Implement a debug port on the pseudo 1W/1R SRAM

Exposes the debug ports of the underlying memories.
This is needed to assist the induction proof.

diff --git a/src/soc/regfile/sram_wrapper.py b/src/soc/regfile/sram_wrapper.py
index 89e5ff40c1d6b81698ac246aab688f69b5255574..8410be34530fae9f4bbf72b5462fbe4c25cad7aa 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