self.we_width = we_width
self.write_phase = write_phase
self.transparent = transparent
+ # interface signals
self.wr_addr_i = Signal(addr_width); """write port address"""
self.wr_data_i = Signal(data_width); """write port data"""
self.wr_we_i = Signal(we_width); """write port enable"""
self.rd_addr_i = Signal(addr_width); """read port address"""
self.rd_data_o = Signal(data_width); """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 (1st mem)"""
- self.dbg_q2 = Signal(data_width); """debug read port data (2nd mem)"""
+ # debug signals, only used in formal proofs
+ self.dbg_addr = Signal(addr_width); """debug: address under test"""
+ self.dbg_we_mask = Signal(we_width); """debug: write lane under test"""
+ gran = self.data_width // self.we_width
+ self.dbg_data = Signal(gran); """debug: data to keep in sync"""
+ self.dbg_wrote = Signal(); """debug: data is valid"""
- def elaborate(self, _):
+ def elaborate(self, platform):
m = Module()
+ # granularity
+ gran = self.data_width // self.we_width
# instantiate the two 1RW memory blocks
mem1 = SinglePortSRAM(self.addr_width, self.data_width, self.we_width)
mem2 = SinglePortSRAM(self.addr_width, self.data_width, self.we_width)
# 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)
+
+ if platform == "formal":
+ # 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
+ m.d.comb += mem1.dbg_a.eq(self.dbg_addr)
+ m.d.comb += mem2.dbg_a.eq(self.dbg_addr)
+ stored1 = Signal(self.data_width)
+ stored2 = Signal(self.data_width)
+ m.d.comb += stored1.eq(mem1.dbg_q)
+ m.d.comb += stored2.eq(mem2.dbg_q)
+ # now, ensure that the value stored in the first memory is always
+ # in sync with the holding register
+ 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(
+ self.dbg_data == stored1.word_select(i, gran))
+ # same for the second memory, but one cycle later
+ with m.If(Past(self.dbg_wrote)):
+ for i in range(self.we_width):
+ with m.If(self.dbg_we_mask[i]):
+ m.d.comb += Assert(
+ Past(self.dbg_data) == stored2.word_select(i, gran))
return m
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])
+ # pass our state to the device under test, so it can ensure that
+ # its state is in sync with ours, for induction
+ m.d.comb += [
+ # address and mask under test
+ dut.dbg_addr.eq(a_const),
+ dut.dbg_we_mask.eq(we_mask),
+ # state of our holding register
+ dut.dbg_data.eq(d_reg),
+ dut.dbg_wrote.eq(wrote),
+ ]
self.assertFormal(m, mode="prove", depth=2)
:param addr_width: width of the address bus
:param data_width: width of the data bus
:param we_width: number of write enable lines
+ :param transparent: whether a simultaneous read and write returns the
+ new value (True) or the old value (False)
"""
- def __init__(self, addr_width, data_width, we_width):
+ def __init__(self, addr_width, data_width, we_width, transparent=True):
self.addr_width = addr_width
self.data_width = data_width
self.we_width = we_width
+ self.transparent = transparent
self.wr_addr_i = Signal(addr_width); """write port address"""
self.wr_data_i = Signal(data_width); """write port data"""
self.wr_we_i = Signal(we_width); """write port enable"""
gran = self.data_width // self.we_width
# instantiate the two phased 1R/1W memory blocks
mem0 = PhasedDualPortRegfile(
- self.addr_width, self.data_width, self.we_width, 0, False)
+ self.addr_width, self.data_width, self.we_width, 0,
+ self.transparent)
mem1 = PhasedDualPortRegfile(
- self.addr_width, self.data_width, self.we_width, 1, False)
+ self.addr_width, self.data_width, self.we_width, 1,
+ self.transparent)
m.submodules.mem0 = mem0
m.submodules.mem1 = mem1
# instantiate the backing memory (FFRAM or LUTRAM)
# memory, but just one bit per write lane
lvt_mem = Memory(width=self.we_width, depth=depth)
lvt_wr = lvt_mem.write_port(granularity=1)
- lvt_rd = lvt_mem.read_port(transparent=False)
+ lvt_rd = lvt_mem.read_port(transparent=self.transparent)
m.submodules.lvt_wr = lvt_wr
m.submodules.lvt_rd = lvt_rd
# generate and wire the phases for the phased memories
lvt_rd.data[i],
mem1.rd_data_o.word_select(i, gran),
mem0.rd_data_o.word_select(i, gran)))
+ # TODO create debug port and pass state downstream
+ m.d.comb += [
+ mem0.dbg_wrote.eq(0),
+ mem1.dbg_wrote.eq(0),
+ ]
return m
class DualPortRegfileTestCase(FHDLTestCase):
- def test_dual_port_regfile(self):
+ def do_test_dual_port_regfile(self, transparent):
"""
Simulate some read/write/modify operations on the dual port register
file
"""
- dut = DualPortRegfile(7, 32, 4)
+ dut = DualPortRegfile(7, 32, 4, transparent)
sim = Simulator(dut)
sim.add_clock(1e-6)
yield from read(0)
yield from write(0, 0, 0)
yield
- # test non-transparent reads
- yield from read(0x42, 0x78345612)
+ if transparent:
+ # returns the value just written
+ yield from read(0x42, 0x55AA9966)
+ else:
+ # returns the old value
+ yield from read(0x42, 0x78345612)
yield from write(0x42, 0b1111, 0x55AA9966)
yield
+ # after a cycle, always returns the new value
yield from read(0x42, 0x55AA9966)
yield from write(0, 0, 0)
yield
sim.add_sync_process(process)
debug_file = 'test_dual_port_regfile'
+ if transparent:
+ debug_file += '_transparent'
traces = ['clk', 'phase',
{'comment': 'write port'},
'wr_addr_i[6:0]', 'wr_we_i[3:0]', 'wr_data_i[31:0]',
with sim_writer:
sim.run()
+ def test_dual_port_regfile(self):
+ with self.subTest("non-transparent reads"):
+ self.do_test_dual_port_regfile(False)
+ with self.subTest("transparent reads"):
+ self.do_test_dual_port_regfile(True)
+
+ def test_dual_port_regfile_proof(self):
+ """
+ Formal proof of the 1W/1R regfile
+ """
+ m = Module()
+ # 128 x 32-bit, 8-bit granularity
+ dut = DualPortRegfile(7, 32, 4, True)
+ 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))
+ # 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)):
+ 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):
+ 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)
+
+ self.assertFormal(m, mode="bmc", depth=10)
+
if __name__ == "__main__":
unittest.main()
projects / soc.git / blobdiff