From: Cesar Strauss <cestrauss@gmail.com>
Date: Sun, 3 Apr 2022 19:31:13 +0000 (-0300)
Subject: Run formal proof on both types (even/odd) of phased SRAMs
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a25051acee0ee21566cd6957e3f5382317f0ef80;p=soc.git

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