Finish the SRAM formal proof by implementing induction

[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 c2096cc89f31eb860f68608e1435bda59a8547ac..6dc092dab3547af0967d08251f2b243cb5408e2a 100644 (file)
--- a/src/soc/regfile/sram_wrapper.py
+++ b/src/soc/regfile/sram_wrapper.py
@@ -19,6 +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 nmutil.formaltest import FHDLTestCase
 from nmutil.gtkw import write_gtkw
@@ -32,6 +33,8 @@ class SinglePortSRAM(Elaboratable):
     :param addr_width: width of the address bus
     :param data_width: width of the data bus
     :param we_width: number of write enable lines
+
+    .. note:: The debug read port is meant only to assist in formal proofs!
     """
     def __init__(self, addr_width, data_width, we_width):
         self.addr_width = addr_width
@@ -45,6 +48,10 @@ class SinglePortSRAM(Elaboratable):
         """ read/write address"""
         self.we = Signal(we_width)
         """write enable"""
+        self.dbg_a = Signal(addr_width)
+        """debug read port address"""
+        self.dbg_q = Signal(data_width)
+        """debug read port data"""
 
     def elaborate(self, _):
         m = Module()
@@ -69,6 +76,11 @@ class SinglePortSRAM(Elaboratable):
         # read and write data
         m.d.comb += wrport.data.eq(self.d)
         m.d.comb += self.q.eq(rdport.data)
+        # the debug port is an asynchronous read port, allowing direct access
+        # to a given memory location by the formal engine
+        m.submodules.dbgport = dbgport = mem.read_port(domain="comb")
+        m.d.comb += dbgport.addr.eq(self.dbg_a)
+        m.d.comb += self.dbg_q.eq(dbgport.data)
         return m
 
     def ports(self):
@@ -165,6 +177,58 @@ class SinglePortSRAMTestCase(FHDLTestCase):
         with sim_writer:
             sim.run()
 
+    def test_model_sram_proof(self):
+        """
+        Formal proof of the single port SRAM model
+        """
+        m = Module()
+        # 128 x 32-bit, 8-bit granularity
+        m.submodules.dut = dut = SinglePortSRAM(7, 32, 4)
+        gran = len(dut.d) // len(dut.we)  # granularity
+        # choose a single random memory location to test
+        a_const = AnyConst(dut.a.shape())
+        # choose a single byte lane to test (one-hot encoding)
+        we_mask = Signal.like(dut.we)
+        # ... by first creating a random bit pattern
+        we_const = AnyConst(dut.we.shape())
+        # ... and zeroing all but the first non-zero bit
+        m.d.comb += we_mask.eq(we_const & (-we_const))
+        # 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.a == a_const):
+            for i in range(len(dut.we)):
+                with m.If(we_mask[i] & dut.we[i]):
+                    m.d.sync += d_reg.eq(dut.d[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.a) == a_const) & wrote):
+            for i in range(len(dut.we)):
+                with m.If(we_mask[i]):
+                    m.d.sync += Assert(d_reg == dut.q[i*gran:i*gran+gran])
+
+        # the following is needed for induction, where an unreachable state
+        # (memory and holding register differ) is turned into an illegal one
+        # first, get the value stored in our memory location, using its debug
+        # port
+        stored = Signal.like(dut.q)
+        m.d.comb += dut.dbg_a.eq(a_const)
+        m.d.comb += stored.eq(dut.dbg_q)
+        # now, ensure that the value stored in memory is always in sync
+        # with the holding register
+        with m.If(wrote):
+            for i in range(len(dut.we)):
+                with m.If(we_mask[i]):
+                    m.d.sync += Assert(d_reg == stored[i*gran:i*gran+gran])
+
+        self.assertFormal(m, mode="prove", depth=2)
+
 
 if __name__ == "__main__":
     unittest.main()