projects
/
nmutil.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
0044c0b
)
modify PLRU to allow access to internals by formal proof
author
Jacob Lifshay
<programmerjake@gmail.com>
Thu, 18 Aug 2022 06:22:38 +0000
(23:22 -0700)
committer
Jacob Lifshay
<programmerjake@gmail.com>
Thu, 18 Aug 2022 06:22:38 +0000
(23:22 -0700)
src/nmutil/plru.py
patch
|
blob
|
history
diff --git
a/src/nmutil/plru.py
b/src/nmutil/plru.py
index 80c67571d42adcc48925181116acf23e445c1548..379709990ad7c2619e02a558f8f366cd329b4959 100644
(file)
--- a/
src/nmutil/plru.py
+++ b/
src/nmutil/plru.py
@@
-27,12
+27,17
@@
class PLRU(Elaboratable):
self.acc_en = Signal()
self.lru_o = Signal(BITS)
self.acc_en = Signal()
self.lru_o = Signal(BITS)
+ self._plru_tree = Signal(self.TLBSZ)
+ """ exposed only for testing """
+
+ @property
+ def TLBSZ(self):
+ return 2 * (self.BITS - 1)
+
def elaborate(self, platform=None):
m = Module()
# Tree (bit per entry)
def elaborate(self, platform=None):
m = Module()
# Tree (bit per entry)
- TLBSZ = 2*(self.BITS-1)
- plru_tree = Signal(TLBSZ)
# Just predefine which nodes will be set/cleared
# E.g. for a TLB with 8 entries, the for-loop is semantically
# Just predefine which nodes will be set/cleared
# E.g. for a TLB with 8 entries, the for-loop is semantically
@@
-65,7
+70,7
@@
class PLRU(Elaboratable):
plru_idx = idx_base + (i >> shift)
# print("plru", i, lvl, hex(idx_base),
# plru_idx, shift, new_idx)
plru_idx = idx_base + (i >> shift)
# print("plru", i, lvl, hex(idx_base),
# plru_idx, shift, new_idx)
- m.d.sync += plru_tree[plru_idx].eq(new_idx)
+ m.d.sync +=
self._
plru_tree[plru_idx].eq(new_idx)
# Decode tree to write enable signals
# Next for-loop basically creates the following logic for e.g.
# Decode tree to write enable signals
# Next for-loop basically creates the following logic for e.g.
@@
-93,7
+98,7
@@
class PLRU(Elaboratable):
plru = Signal(reset_less=True,
name="plru-%d-%d-%d-%d" %
(i, lvl, plru_idx, new_idx))
plru = Signal(reset_less=True,
name="plru-%d-%d-%d-%d" %
(i, lvl, plru_idx, new_idx))
- m.d.comb += plru.eq(plru_tree[plru_idx])
+ m.d.comb += plru.eq(
self._
plru_tree[plru_idx])
if new_idx:
en.append(~plru) # yes inverted (using bool() below)
else:
if new_idx:
en.append(~plru) # yes inverted (using bool() below)
else: