d47453a0f9dd7a555fe6a5e5c00c3083b9bd0b35
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 nmigen
.test
.utils
import FHDLTestCase
8 from nmigen
.cli
import rtlil
12 from soc
.regfile
.regfile
import RegFile
15 class Driver(RegFile
):
17 super().__init
__(width
=8, depth
=4)
18 for i
in range(1): # just do one for now
22 def elaborate(self
, platform
):
23 m
= super().elaborate(platform
)
29 lg2depth
= int(math
.ceil(math
.log2(depth
)))
30 _rdports
= self
._rdports
31 _wrports
= self
._wrports
33 comb
+= _wrports
[0].data_i
.eq(AnySeq(8))
35 comb
+= _wrports
[0].wen
.eq(AnySeq(1))
36 comb
+= _wrports
[0].waddr
.eq(AnySeq(lg2depth
))
37 comb
+= _rdports
[0].ren
.eq(AnySeq(1))
38 comb
+= _rdports
[0].raddr
.eq(AnySeq(lg2depth
))
44 # Most likely incorrect 4-way truth table
46 # rp.ren wp.wen rp.data_o reg
47 # 0 0 zero should be previous value
49 # 1 0 reg should be previous value
50 # 1 1 wp.data_i wp.data_i
52 # Holds the value written to the register when a write happens
53 register_data
= Array([Signal(self
.width
, name
=f
"reg_data{i}")
54 for i
in range(depth
)])
55 register_written
= Array([Signal(name
=f
"reg_written{i}")
56 for i
in range(depth
)])
59 comb
+= Assume(rst
== 1)
61 for i
in range(depth
):
62 comb
+= Assume(register_written
[i
] == 0)
65 comb
+= Assume(rst
== 0)
67 with m
.If(_rdports
[0].ren
== 0):
68 comb
+= Assert(_rdports
[0].data_o
== 0)
70 # Read enable is active
72 addr
= _rdports
[0].raddr
73 # Check to see if there's a write on this
74 # cycle. If so, then the output data should be
75 # that of the write port
76 with m
.If(_wrports
[0].wen
& (_wrports
[0].waddr
== addr
)):
77 comb
+= Assert(_rdports
[0].data_o
==
81 # Otherwise the data output should be the
83 with m
.Elif(register_written
[addr
]):
84 comb
+= Assert(_rdports
[0].data_o
==
88 # If there's a write to a given register, store that
89 # data in a copy of the register, and mark it as
91 with m
.If(_wrports
[0].wen
):
92 addr
= _wrports
[0].waddr
93 sync
+= register_data
[addr
].eq(_wrports
[0].data_i
)
94 sync
+= register_written
[addr
].eq(1)
101 class TestCase(FHDLTestCase
):
102 def test_formal(self
):
104 self
.assertFormal(module
, mode
="bmc", depth
=10)
105 self
.assertFormal(module
, mode
="cover", depth
=10)
107 def test_ilang(self
):
109 vl
= rtlil
.convert(dut
, ports
=[])
110 with
open("regfile_binary.il", "w") as f
:
114 if __name__
== '__main__':