1 # This is the proof for Regfile class from regfile/regfile.py
3 from nmigen
import (Module
, Signal
, Elaboratable
, Mux
, Cat
, Repl
,
4 signed
, ResetSignal
, Array
)
5 from nmigen
.asserts
import (Assert
, AnySeq
, Assume
, Cover
, Initial
,
6 Rose
, Fell
, Stable
, Past
)
7 from nmutil
.formaltest
import FHDLTestCase
8 from nmigen
.cli
import rtlil
11 from soc
.regfile
.regfile
import RegFileArray
14 class Driver(RegFileArray
):
16 super().__init
__(width
=8, depth
=4)
17 for i
in range(1): # just do one for now
18 self
.read_port(f
"rd{i}")
19 self
.write_port(f
"wr{i}")
21 def elaborate(self
, platform
):
22 m
= super().elaborate(platform
)
28 _rdports
= self
._rdports
29 _wrports
= self
._wrports
31 comb
+= _wrports
[0][1].data_i
.eq(AnySeq(8))
32 comb
+= _wrports
[0][1].wen
.eq(AnySeq(depth
))
33 comb
+= _rdports
[0][1].ren
.eq(AnySeq(depth
))
39 # Most likely incorrect 4-way truth table
41 # rp.ren wp.wen rp.data_o reg
42 # 0 0 zero should be previous value
44 # 1 0 reg should be previous value
45 # 1 1 wp.data_i wp.data_i
47 # Holds the value written to the register when a write happens
48 register_data
= Array([Signal(self
.width
, name
=f
"reg_data{i}")
49 for i
in range(depth
)])
50 register_written
= Array([Signal(name
=f
"reg_written{i}")
51 for i
in range(depth
)])
52 comb
+= Cover(_rdports
[0][1].ren
== 0b0001)
55 comb
+= Assume(rst
== 1)
57 for i
in range(depth
):
58 comb
+= Assume(register_written
[i
] == 0)
61 comb
+= Assume(rst
== 0)
64 # Assume that rd_en is onehot
66 for i
in range(depth
):
67 bitsum
= bitsum
+ _rdports
[0][1].ren
[i
]
68 comb
+= Assume(bitsum
<= 1)
72 # If there is no read, then data_o should be 0
73 with m
.If(_rdports
[0][1].ren
== 0):
74 comb
+= Assert(_rdports
[0][1].data_o
== 0)
76 # One of the rd_enable requests must be active
78 for i
in range(depth
):
79 # If there's a read on this register
80 with m
.If(_rdports
[0][1].ren
[i
]):
81 # Check to see if there's a write on this
82 # cycle. If so, then the output data should be
83 # that of the write port
84 with m
.If(_wrports
[0][1].wen
[i
]):
85 comb
+= Assert(_rdports
[0][1].data_o
==
86 _wrports
[0][1].data_i
)
89 # Otherwise the data output should be the
91 with m
.Elif(register_written
[i
]):
92 comb
+= Assert(_rdports
[0][1].data_o
==
96 for i
in range(depth
):
97 # If there's a write to a given register, store that
98 # data in a copy of the register, and mark it as
100 with m
.If(_wrports
[0][1].wen
[i
]):
101 sync
+= register_data
[i
].eq(_wrports
[0][1].data_i
)
102 sync
+= register_written
[i
].eq(1)
109 class TestCase(FHDLTestCase
):
110 def test_formal(self
):
112 self
.assertFormal(module
, mode
="bmc", depth
=10)
113 self
.assertFormal(module
, mode
="cover", depth
=10)
115 def test_ilang(self
):
117 vl
= rtlil
.convert(dut
, ports
=[])
118 with
open("regfile_array.il", "w") as f
:
122 if __name__
== '__main__':