projects
/
soc.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
472abdb
)
Run formal proof on both types (even/odd) of phased SRAMs
author
Cesar Strauss
<cestrauss@gmail.com>
Sun, 3 Apr 2022 19:31:13 +0000
(16:31 -0300)
committer
Cesar Strauss
<cestrauss@gmail.com>
Sun, 3 Apr 2022 19:31:13 +0000
(16:31 -0300)
src/soc/regfile/sram_wrapper.py
patch
|
blob
|
history
diff --git
a/src/soc/regfile/sram_wrapper.py
b/src/soc/regfile/sram_wrapper.py
index 38104e86bd7b17d7f52fdb15c61612ab5a8e247d..f5d555e8db49cad7c1533c98d1e045b4057a8182 100644
(file)
--- a/
src/soc/regfile/sram_wrapper.py
+++ b/
src/soc/regfile/sram_wrapper.py
@@
-448,13
+448,14
@@
class PhasedDualPortRegfileTestCase(FHDLTestCase):
with self.subTest("writes happen on phase 1 (transparent reads)"):
self.do_test_phased_dual_port_regfile(1, True)
with self.subTest("writes happen on phase 1 (transparent reads)"):
self.do_test_phased_dual_port_regfile(1, True)
- def
test_phased_dual_port_regfile_proof(self
):
+ def
do_test_phased_dual_port_regfile_proof(self, write_phase
):
"""
Formal proof of the pseudo 1W/1R regfile
"""
m = Module()
# 128 x 32-bit, 8-bit granularity
"""
Formal proof of the pseudo 1W/1R regfile
"""
m = Module()
# 128 x 32-bit, 8-bit granularity
- m.submodules.dut = dut = PhasedDualPortRegfile(7, 32, 4, 0, True)
+ dut = PhasedDualPortRegfile(7, 32, 4, write_phase, True)
+ m.submodules.dut = dut
gran = dut.data_width // dut.we_width # granularity
# choose a single random memory location to test
a_const = AnyConst(dut.addr_width)
gran = dut.data_width // dut.we_width # granularity
# choose a single random memory location to test
a_const = AnyConst(dut.addr_width)
@@
-514,6
+515,13
@@
class PhasedDualPortRegfileTestCase(FHDLTestCase):
self.assertFormal(m, mode="prove", depth=2)
self.assertFormal(m, mode="prove", depth=2)
+ def test_phased_dual_port_regfile_proof(self):
+ """test both types (odd and even write ports) of phased write memory"""
+ with self.subTest("writes happen on phase 0"):
+ self.do_test_phased_dual_port_regfile_proof(0)
+ with self.subTest("writes happen on phase 1"):
+ self.do_test_phased_dual_port_regfile_proof(1)
+
if __name__ == "__main__":
unittest.main()
if __name__ == "__main__":
unittest.main()