From: Cesar Strauss <cestrauss@gmail.com>
Date: Sun, 27 Mar 2022 17:23:39 +0000 (-0300)
Subject: Finish the SRAM formal proof by implementing induction
X-Git-Url: https://git.libre-soc.org/?p=soc.git;a=commitdiff_plain;h=ec40b7ea2b43a9874db3aa1400545ab469844779

Finish the SRAM formal proof by implementing induction

Add a combinatorial (no delay) debug read port to the SRAM model,
for turning an unreacheable state (memory and holding register differ)
into an illegal state.
Just two clock cycles are needed for a working proof.
---

diff --git a/src/soc/regfile/sram_wrapper.py b/src/soc/regfile/sram_wrapper.py
index 447b6ca9..6dc092da 100644
--- a/src/soc/regfile/sram_wrapper.py
+++ b/src/soc/regfile/sram_wrapper.py
@@ -33,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
@@ -46,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()
@@ -70,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):
@@ -202,7 +213,21 @@ class SinglePortSRAMTestCase(FHDLTestCase):
                 with m.If(we_mask[i]):
                     m.d.sync += Assert(d_reg == dut.q[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 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__":