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

[soc.git] / src / soc / regfile / sram_wrapper.py

diff --git a/src/soc/regfile/sram_wrapper.py b/src/soc/regfile/sram_wrapper.py
index 89e5ff40c1d6b81698ac246aab688f69b5255574..f5d555e8db49cad7c1533c98d1e045b4057a8182 100644 (file)
--- a/src/soc/regfile/sram_wrapper.py
+++ b/src/soc/regfile/sram_wrapper.py
@@ -243,6 +243,8 @@ class PhasedDualPortRegfile(Elaboratable):
                         accept data
     :param transparent: whether a simultaneous read and write returns the
                         new value (True) or the old value (False)
+
+    .. note:: The debug read port is meant only to assist in formal proofs!
     """
 
     def __init__(self, addr_width, data_width, we_width, write_phase,
@@ -264,6 +266,12 @@ class PhasedDualPortRegfile(Elaboratable):
         """read port data"""
         self.phase = Signal()
         """even/odd cycle indicator"""
+        self.dbg_a = Signal(addr_width)
+        """debug read port address"""
+        self.dbg_q1 = Signal(data_width)
+        """debug read port data (first memory)"""
+        self.dbg_q2 = Signal(data_width)
+        """debug read port data (second memory)"""
 
     def elaborate(self, _):
         m = Module()
@@ -315,6 +323,13 @@ class PhasedDualPortRegfile(Elaboratable):
                 # always output the read data from the second memory,
                 # if not transparent
                 m.d.comb += self.rd_data_o.eq(mem2.q)
+        # our debug port allow the formal engine to inspect the content of
+        # a fixed, arbitrary address, on our memory blocks.
+        # wire it to their debug ports.
+        m.d.comb += mem1.dbg_a.eq(self.dbg_a)
+        m.d.comb += mem2.dbg_a.eq(self.dbg_a)
+        m.d.comb += self.dbg_q1.eq(mem1.dbg_q)
+        m.d.comb += self.dbg_q2.eq(mem2.dbg_q)
 
         return m
 
@@ -433,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)
@@ -474,7 +490,37 @@ class PhasedDualPortRegfileTestCase(FHDLTestCase):
                     m.d.sync += Assert(
                         d_reg == dut.rd_data_o[i * gran:i * gran + gran])
 
-        self.assertFormal(m, mode="bmc", depth=10)
+        # the following is needed for induction, where an unreachable state
+        # (memory and holding register differ) is turned into an illegal one
+        # first, get the values stored in our memory location, using its
+        # debug port
+        stored1 = Signal(dut.data_width)
+        stored2 = Signal(dut.data_width)
+        m.d.comb += dut.dbg_a.eq(a_const)
+        m.d.comb += stored1.eq(dut.dbg_q1)
+        m.d.comb += stored2.eq(dut.dbg_q2)
+        # now, ensure that the value stored in the first memory is always
+        # in sync with the holding register
+        with m.If(wrote):
+            for i in range(dut.we_width):
+                with m.If(we_mask[i]):
+                    m.d.comb += Assert(
+                        d_reg == stored1[i * gran:i * gran + gran])
+        # same for the second memory, but one cycle later
+        with m.If(Past(wrote)):
+            for i in range(dut.we_width):
+                with m.If(we_mask[i]):
+                    m.d.comb += Assert(
+                        Past(d_reg) == stored2[i * gran:i * gran + gran])
+
+        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__":