From 21135f80de4667546c953a562ca91fa20fecf50b Mon Sep 17 00:00:00 2001 From: Cesar Strauss Date: Sun, 3 Apr 2022 15:50:43 -0300 Subject: [PATCH] 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. --- src/soc/regfile/sram_wrapper.py | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/src/soc/regfile/sram_wrapper.py b/src/soc/regfile/sram_wrapper.py index 89e5ff40..8410be34 100644 --- 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 -- 2.30.2