Complete the formal proof of the pseudo dual port SRAM

Have to ensure that the holding register is in sync with the memory
contents, to avoid false positives due to unreachable states.

Since we are adding assertions, we can only strengthen the proof, even
if it does become more complex.

diff --git a/src/soc/regfile/sram_wrapper.py b/src/soc/regfile/sram_wrapper.py
index 8410be34530fae9f4bbf72b5462fbe4c25cad7aa..38104e86bd7b17d7f52fdb15c61612ab5a8e247d 100644 (file)
--- a/src/soc/regfile/sram_wrapper.py
+++ b/src/soc/regfile/sram_wrapper.py
@@ -489,7 +489,30 @@ 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)
 
 
 if __name__ == "__main__":