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 nmigen.asserts import Assert, Assume, Past, AnyConst
from nmutil.formaltest import FHDLTestCase
from nmutil.gtkw import write_gtkw
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,
"""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()
# 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
with self.subTest("writes happen on phase 1 (transparent reads)"):
self.do_test_phased_dual_port_regfile(1, True)
+ def do_test_phased_dual_port_regfile_proof(self, write_phase, transparent):
+ """
+ Formal proof of the pseudo 1W/1R regfile
+ """
+ m = Module()
+ # 128 x 32-bit, 8-bit granularity
+ dut = PhasedDualPortRegfile(7, 32, 4, write_phase, transparent)
+ m.submodules.dut = dut
+ gran = dut.data_width // dut.we_width # granularity
+ # choose a single random memory location to test
+ a_const = AnyConst(dut.addr_width)
+ # choose a single byte lane to test (one-hot encoding)
+ we_mask = Signal(dut.we_width)
+ # ... by first creating a random bit pattern
+ we_const = AnyConst(dut.we_width)
+ # ... and zeroing all but the first non-zero bit
+ m.d.comb += we_mask.eq(we_const & (-we_const))
+ # drive alternating phases
+ m.d.comb += Assume(dut.phase != Past(dut.phase))
+ # 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.wr_addr_i == a_const)
+ & (dut.phase == dut.write_phase)):
+ for i in range(dut.we_width):
+ with m.If(we_mask[i] & dut.wr_we_i[i]):
+ m.d.sync += d_reg.eq(
+ dut.wr_data_i[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.rd_addr_i) == a_const):
+ if transparent:
+ with m.If(wrote):
+ for i in range(dut.we_width):
+ rd_lane = dut.rd_data_o.word_select(i, gran)
+ with m.If(we_mask[i]):
+ 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)
+ & Past(dut.phase) == dut.write_phase):
+ # simultaneous write -> check against last written value
+ with m.If(Past(wrote)):
+ for i in range(dut.we_width):
+ rd_lane = dut.rd_data_o.word_select(i, gran)
+ with m.If(we_mask[i]):
+ m.d.sync += Assert(Past(d_reg) == rd_lane)
+ with m.Else():
+ # otherwise, check against current written value
+ with m.If(wrote):
+ for i in range(dut.we_width):
+ rd_lane = dut.rd_data_o.word_select(i, gran)
+ with m.If(we_mask[i]):
+ m.d.sync += Assert(d_reg == rd_lane)
+
+ # the following is needed for induction, where an unreachable state
+ # (memory and holding register differ) is turned into an illegal one
+ # first, get the values stored in our memory location, using its
+ # debug port
+ stored1 = Signal(dut.data_width)
+ stored2 = Signal(dut.data_width)
+ m.d.comb += dut.dbg_a.eq(a_const)
+ m.d.comb += stored1.eq(dut.dbg_q1)
+ m.d.comb += stored2.eq(dut.dbg_q2)
+ # now, ensure that the value stored in the first memory is always
+ # in sync with the holding register
+ with m.If(wrote):
+ for i in range(dut.we_width):
+ with m.If(we_mask[i]):
+ m.d.comb += Assert(
+ d_reg == stored1[i * gran:i * gran + gran])
+ # same for the second memory, but one cycle later
+ with m.If(Past(wrote)):
+ for i in range(dut.we_width):
+ with m.If(we_mask[i]):
+ m.d.comb += Assert(
+ Past(d_reg) == stored2[i * gran:i * gran + gran])
+
+ self.assertFormal(m, mode="prove", depth=2)
+
+ def test_phased_dual_port_regfile_proof(self):
+ """test both types (odd and even write ports) of phased write memory"""
+ with self.subTest("writes happen on phase 0"):
+ self.do_test_phased_dual_port_regfile_proof(0, False)
+ with self.subTest("writes happen on phase 1"):
+ self.do_test_phased_dual_port_regfile_proof(1, False)
+ # test again, with transparent read ports
+ with self.subTest("writes happen on phase 0 (transparent reads)"):
+ self.do_test_phased_dual_port_regfile_proof(0, True)
+ with self.subTest("writes happen on phase 1 (transparent reads)"):
+ self.do_test_phased_dual_port_regfile_proof(1, True)
+
if __name__ == "__main__":
unittest.main()
projects / soc.git / blobdiff