From a25051acee0ee21566cd6957e3f5382317f0ef80 Mon Sep 17 00:00:00 2001 From: Cesar Strauss Date: Sun, 3 Apr 2022 16:31:13 -0300 Subject: [PATCH] Run formal proof on both types (even/odd) of phased SRAMs --- src/soc/regfile/sram_wrapper.py | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/src/soc/regfile/sram_wrapper.py b/src/soc/regfile/sram_wrapper.py index 38104e86..f5d555e8 100644 --- 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) - 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 - 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) @@ -514,6 +515,13 @@ class PhasedDualPortRegfileTestCase(FHDLTestCase): 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() -- 2.30.2