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
class SinglePortSRAM(Elaboratable):
:param addr_width: width of the address bus
:param data_width: width of the data bus
:param we_width: number of write enable lines
+
+ .. note:: The debug read port is meant only to assist in formal proofs!
"""
def __init__(self, addr_width, data_width, we_width):
self.addr_width = addr_width
""" read/write address"""
self.we = Signal(we_width)
"""write enable"""
+ self.dbg_a = Signal(addr_width)
+ """debug read port address"""
+ self.dbg_q = Signal(data_width)
+ """debug read port data"""
def elaborate(self, _):
m = Module()
# read and write data
m.d.comb += wrport.data.eq(self.d)
m.d.comb += self.q.eq(rdport.data)
+ # the debug port is an asynchronous read port, allowing direct access
+ # to a given memory location by the formal engine
+ m.submodules.dbgport = dbgport = mem.read_port(domain="comb")
+ m.d.comb += dbgport.addr.eq(self.dbg_a)
+ m.d.comb += self.dbg_q.eq(dbgport.data)
return m
def ports(self):
dut = SinglePortSRAM(10, 16, 2)
create_ilang(dut, dut.ports(), "mem_blkram")
+ def test_sram_model(self):
+ """
+ Simulate some read/write/modify operations on the SRAM model
+ """
+ dut = SinglePortSRAM(7, 32, 4)
+ sim = Simulator(dut)
+ sim.add_clock(1e-6)
+
+ def process():
+ # 1) write 0x12_34_56_78 to address 0
+ yield dut.a.eq(0)
+ yield dut.d.eq(0x12_34_56_78)
+ yield dut.we.eq(0b1111)
+ yield
+ # 2) write 0x9A_BC_DE_F0 to address 1
+ yield dut.a.eq(1)
+ yield dut.d.eq(0x9A_BC_DE_F0)
+ yield dut.we.eq(0b1111)
+ yield
+ # ... and read value just written to address 0
+ self.assertEqual((yield dut.q), 0x12_34_56_78)
+ # 3) prepare to read from address 0
+ yield dut.d.eq(0)
+ yield dut.we.eq(0b0000)
+ yield dut.a.eq(0)
+ yield
+ # ... and read value just written to address 1
+ self.assertEqual((yield dut.q), 0x9A_BC_DE_F0)
+ # 4) prepare to read from address 1
+ yield dut.a.eq(1)
+ yield
+ # ... and read value from address 0
+ self.assertEqual((yield dut.q), 0x12_34_56_78)
+ # 5) write 0x9A and 0xDE to bytes 1 and 3, leaving
+ # bytes 0 and 2 unchanged
+ yield dut.a.eq(0)
+ yield dut.d.eq(0x9A_FF_DE_FF)
+ yield dut.we.eq(0b1010)
+ yield
+ # ... and read value from address 1
+ self.assertEqual((yield dut.q), 0x9A_BC_DE_F0)
+ # 6) nothing more to do
+ yield dut.d.eq(0)
+ yield dut.we.eq(0)
+ yield
+ # ... other than confirm that bytes 1 and 3 were modified
+ # correctly
+ self.assertEqual((yield dut.q), 0x9A_34_DE_78)
+
+ sim.add_sync_process(process)
+ traces = ['rdport.clk', 'a[6:0]', 'we[3:0]', 'd[31:0]', 'q[31:0]']
+ write_gtkw('test_sram_model.gtkw', 'test_sram_model.vcd',
+ traces, module='top')
+ sim_writer = sim.write_vcd('test_sram_model.vcd')
+ 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])
+
+ # the following is needed for induction, where an unreachable state
+ # (memory and holding register differ) is turned into an illegal one
+ # first, get the value stored in our memory location, using its debug
+ # port
+ stored = Signal.like(dut.q)
+ m.d.comb += dut.dbg_a.eq(a_const)
+ m.d.comb += stored.eq(dut.dbg_q)
+ # now, ensure that the value stored in memory is always in sync
+ # with the holding register
+ with m.If(wrote):
+ for i in range(len(dut.we)):
+ with m.If(we_mask[i]):
+ m.d.sync += Assert(d_reg == stored[i*gran:i*gran+gran])
+
+ self.assertFormal(m, mode="prove", depth=2)
+
if __name__ == "__main__":
unittest.main()
projects / soc.git / blobdiff