Run formal proof on both types (even/odd) of phased SRAMs

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)
 
-    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()