From: Cesar Strauss <cestrauss@gmail.com>
Date: Sun, 3 Apr 2022 18:24:16 +0000 (-0300)
Subject: Formal proof of the phased write dual port memory wrapper
X-Git-Url: https://git.libre-soc.org/?p=soc.git;a=commitdiff_plain;h=9764dfc9c5d0fc8dff70c73cc4475d1087b155aa

Formal proof of the phased write dual port memory wrapper

Similar to the proof of the 1RW memory block, but read and writes are
done on dedicated ports.
For now, only transparent regfile is tested.
To complete the formal verification, an induction proof will follow.
---

diff --git a/src/soc/regfile/sram_wrapper.py b/src/soc/regfile/sram_wrapper.py
index f80c4323..89e5ff40 100644
--- a/src/soc/regfile/sram_wrapper.py
+++ b/src/soc/regfile/sram_wrapper.py
@@ -19,7 +19,7 @@ import unittest
 from nmigen import Elaboratable, Module, Memory, Signal
 from nmigen.back import rtlil
 from nmigen.sim import Simulator
-from nmigen.asserts import Assert, Past, AnyConst
+from nmigen.asserts import Assert, Assume, Past, AnyConst
 
 from nmutil.formaltest import FHDLTestCase
 from nmutil.gtkw import write_gtkw
@@ -433,6 +433,49 @@ 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):
+        """
+        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)
+        gran = dut.data_width // dut.we_width  # granularity
+        # choose a single random memory location to test
+        a_const = AnyConst(dut.addr_width)
+        # choose a single byte lane to test (one-hot encoding)
+        we_mask = Signal(dut.we_width)
+        # ... by first creating a random bit pattern
+        we_const = AnyConst(dut.we_width)
+        # ... and zeroing all but the first non-zero bit
+        m.d.comb += we_mask.eq(we_const & (-we_const))
+        # drive alternating phases
+        m.d.comb += Assume(dut.phase != Past(dut.phase))
+        # holding data register
+        d_reg = Signal(gran)
+        # for some reason, simulated formal memory is not zeroed at reset
+        # ... so, remember whether we wrote it, at least once.
+        wrote = Signal()
+        # if our memory location and byte lane is being written,
+        # capture the data in our holding register
+        with m.If((dut.wr_addr_i == a_const)
+                  & (dut.phase == dut.write_phase)):
+            for i in range(dut.we_width):
+                with m.If(we_mask[i] & dut.wr_we_i[i]):
+                    m.d.sync += d_reg.eq(
+                        dut.wr_data_i[i * gran:i * gran + gran])
+                    m.d.sync += wrote.eq(1)
+        # if our memory location is being read,
+        # and the holding register has valid data,
+        # then its value must match the memory output, on the given lane
+        with m.If((Past(dut.rd_addr_i) == a_const) & wrote):
+            for i in range(dut.we_width):
+                with m.If(we_mask[i]):
+                    m.d.sync += Assert(
+                        d_reg == dut.rd_data_o[i * gran:i * gran + gran])
+
+        self.assertFormal(m, mode="bmc", depth=10)
+
 
 if __name__ == "__main__":
     unittest.main()