From 695108b7e98dc23073cf952825e18b6dce10e6d8 Mon Sep 17 00:00:00 2001 From: Cesar Strauss Date: Sat, 16 Apr 2022 17:44:30 -0300 Subject: [PATCH] Check non-transparent 1W/1R SRAM wrapper Add special case for the non-transparent case, where a simultaneous write returns the old value of the holding register. This completes the proof for this 1W/1R SRAM wrapper --- src/soc/regfile/sram_wrapper.py | 33 ++++++++++++++++++++++++++++----- 1 file changed, 28 insertions(+), 5 deletions(-) diff --git a/src/soc/regfile/sram_wrapper.py b/src/soc/regfile/sram_wrapper.py index cba1ec21..bc29cff5 100644 --- a/src/soc/regfile/sram_wrapper.py +++ b/src/soc/regfile/sram_wrapper.py @@ -802,13 +802,13 @@ class DualPortRegfileTestCase(FHDLTestCase): with self.subTest("transparent reads"): self.do_test_dual_port_regfile(True) - def test_dual_port_regfile_proof(self): + def do_test_dual_port_regfile_proof(self, transparent=True): """ Formal proof of the 1W/1R regfile """ m = Module() # 128 x 32-bit, 8-bit granularity - dut = DualPortRegfile(7, 32, 4, True) + dut = DualPortRegfile(7, 32, 4, transparent) m.submodules.dut = dut gran = dut.data_width // dut.we_width # granularity # choose a single random memory location to test @@ -837,9 +837,23 @@ class DualPortRegfileTestCase(FHDLTestCase): # and the holding register has valid data, # then its value must match the memory output, on the given lane with m.If(Past(dut.rd_addr_i) == a_const): - with m.If(wrote): - rd_lane = dut.rd_data_o.word_select(lane, gran) - m.d.sync += Assert(d_reg == rd_lane) + if transparent: + with m.If(wrote): + rd_lane = dut.rd_data_o.word_select(lane, gran) + m.d.sync += Assert(d_reg == rd_lane) + else: + # with a non-transparent read port, the read value depends + # on whether there is a simultaneous write, or not + with m.If(Past(dut.wr_addr_i) == a_const): + # simultaneous write -> check against last written value + with m.If(wrote & Past(wrote)): + rd_lane = dut.rd_data_o.word_select(lane, gran) + m.d.sync += Assert(Past(d_reg) == rd_lane) + with m.Else(): + # otherwise, check against current written value + with m.If(wrote): + rd_lane = dut.rd_data_o.word_select(lane, gran) + m.d.sync += Assert(d_reg == rd_lane) m.d.comb += [ dut.dbg_addr.eq(a_const), @@ -852,6 +866,15 @@ class DualPortRegfileTestCase(FHDLTestCase): self.assertFormal(m, mode="prove", depth=3) + def test_dual_port_regfile_proof(self): + """ + Formal check of 1W/1R regfile (transparent and not) + """ + with self.subTest("transparent reads"): + self.do_test_dual_port_regfile_proof(True) + with self.subTest("non-transparent reads"): + self.do_test_dual_port_regfile_proof(False) + if __name__ == "__main__": unittest.main() -- 2.30.2