From: Cesar Strauss Date: Sat, 26 Mar 2022 21:09:12 +0000 (-0300) Subject: Add formal verification of the single port memory block X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7df58b30dcefe51c547db4102db41a58e5124922;p=soc.git Add formal verification of the single port memory block We test a single, random memory location. If any memory location, chosen at random, passes, then the whole memory is correct. Note that an induction proof is still missing, since it requires additional assertions to avoid illegal states. --- diff --git a/src/soc/regfile/sram_wrapper.py b/src/soc/regfile/sram_wrapper.py index c2096cc8..447b6ca9 100644 --- a/src/soc/regfile/sram_wrapper.py +++ b/src/soc/regfile/sram_wrapper.py @@ -19,6 +19,7 @@ import unittest from nmigen import Elaboratable, Module, Memory, Signal from nmigen.back import rtlil from nmigen.sim import Simulator +from nmigen.asserts import Assert, Past, AnyConst from nmutil.formaltest import FHDLTestCase from nmutil.gtkw import write_gtkw @@ -165,6 +166,44 @@ class SinglePortSRAMTestCase(FHDLTestCase): with sim_writer: sim.run() + def test_model_sram_proof(self): + """ + Formal proof of the single port SRAM model + """ + m = Module() + # 128 x 32-bit, 8-bit granularity + m.submodules.dut = dut = SinglePortSRAM(7, 32, 4) + gran = len(dut.d) // len(dut.we) # granularity + # choose a single random memory location to test + a_const = AnyConst(dut.a.shape()) + # choose a single byte lane to test (one-hot encoding) + we_mask = Signal.like(dut.we) + # ... by first creating a random bit pattern + we_const = AnyConst(dut.we.shape()) + # ... and zeroing all but the first non-zero bit + m.d.comb += we_mask.eq(we_const & (-we_const)) + # holding data register + d_reg = Signal(gran) + # for some reason, simulated formal memory is not zeroed at reset + # ... so, remember whether we wrote it, at least once. + wrote = Signal() + # if our memory location and byte lane is being written + # ... capture the data in our holding register + with m.If(dut.a == a_const): + for i in range(len(dut.we)): + with m.If(we_mask[i] & dut.we[i]): + m.d.sync += d_reg.eq(dut.d[i*gran:i*gran+gran]) + m.d.sync += wrote.eq(1) + # if our memory location is being read + # ... and the holding register has valid data + # ... then its value must match the memory output, on the given lane + with m.If((Past(dut.a) == a_const) & wrote): + for i in range(len(dut.we)): + 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) + if __name__ == "__main__": unittest.main()