From 1d27edf8d48492302a8119fde51cae35e5e64b48 Mon Sep 17 00:00:00 2001 From: Cesar Strauss Date: Sat, 16 Apr 2022 11:33:08 -0300 Subject: [PATCH] Synchronize LVT state, completing the induction proof --- src/soc/regfile/sram_wrapper.py | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/src/soc/regfile/sram_wrapper.py b/src/soc/regfile/sram_wrapper.py index e1891daa..affb5ee7 100644 --- a/src/soc/regfile/sram_wrapper.py +++ b/src/soc/regfile/sram_wrapper.py @@ -664,6 +664,20 @@ class DualPortRegfile(Elaboratable): ] # sync phase to upstream m.d.comb += Assert(self.dbg_phase == phase) + # this debug port for the LVT is an asynchronous read port, + # allowing direct access to a given memory location + # by the formal engine + m.submodules.dbgport = dbgport = lvt_mem.read_port(domain='comb') + # first, get the value stored in our memory location, + stored = Signal(self.we_width) + m.d.comb += dbgport.addr.eq(self.dbg_addr) + m.d.comb += stored.eq(dbgport.data) + # now, ensure that the value stored in memory is always in sync + # with the expected value (which memory the value was written to) + with m.If(self.dbg_wrote): + for i in range(self.we_width): + with m.If(self.dbg_we_mask[i]): + m.d.comb += Assert(stored[i] == self.dbg_wrote_phase) return m @@ -840,7 +854,7 @@ class DualPortRegfileTestCase(FHDLTestCase): dut.dbg_phase.eq(phase), ] - self.assertFormal(m, mode="bmc", depth=10) + self.assertFormal(m, mode="prove", depth=3) if __name__ == "__main__": -- 2.30.2