:param we_width: number of write enable lines
:param write_phase: indicates on which phase the write port will
accept data
+ :param transparent: whether a simultaneous read and write returns the
+ new value (True) or the old value (False) on the full
+ read port
+
+ .. note:: The debug read port is meant only to assist in formal proofs!
"""
- def __init__(self, addr_width, data_width, we_width, write_phase):
+ def __init__(self, addr_width, data_width, we_width, write_phase,
+ transparent=True):
self.addr_width = addr_width
self.data_width = data_width
self.we_width = we_width
self.write_phase = write_phase
+ self.transparent = transparent
# interface signals
self.wr_addr_i = Signal(addr_width); """phased write port address"""
self.wr_data_i = Signal(data_width); """phased write port data"""
self.rdp_addr_i = Signal(addr_width); """phased read port address"""
self.rdp_data_o = Signal(data_width); """phased read port data"""
self.phase = Signal(); """even/odd cycle indicator"""
+ # debug signals, only used in formal proofs
+ self.dbg_addr = Signal(addr_width); """debug: address under test"""
+ lanes = range(we_width)
+ self.dbg_lane = Signal(lanes); """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, platform):
m = Module()
# holding registers for the write port of the other memories
last_wr_addr = Signal(self.addr_width)
last_wr_we = Signal(self.we_width)
- # do the phased read and write addresses coincide?
+ # do read and write addresses coincide?
+ same_read_write = Signal()
same_phased_read_write = Signal()
with m.If(self.phase == self.write_phase):
# write phase, start a write on the first memory
# output previously read data from the first memory
m.d.comb += self.rd_data_o.eq(mem1.q)
# remember whether we are reading from the same location as we
- # are writing, on the phased read port
+ # are writing
m.d.sync += same_phased_read_write.eq(
self.rdp_addr_i == self.wr_addr_i)
+ if self.transparent:
+ m.d.sync += same_read_write.eq(self.rd_addr_i == self.wr_addr_i)
with m.Else():
# read phase, write last written data on the other memories
m.d.comb += [
# start a read on the first memory
m.d.comb += mem1.a.eq(self.rd_addr_i)
# output the read data from the second memory
- m.d.comb += self.rd_data_o.eq(mem2.q)
+ if self.transparent:
+ with m.If(same_read_write):
+ # when transparent, and read and write addresses coincide,
+ # output the data just written
+ m.d.comb += self.rd_data_o.eq(mem1.q)
+ with m.Else():
+ # otherwise, output previously read data
+ # from the second memory
+ m.d.comb += self.rd_data_o.eq(mem2.q)
+ else:
+ # always output the read data from the second memory,
+ # if not transparent
+ m.d.comb += self.rd_data_o.eq(mem2.q)
with m.If(same_phased_read_write):
# if read and write addresses coincide,
# output the data just written
# from the third memory
m.d.comb += self.rdp_data_o.eq(mem3.q)
+ if platform == "formal":
+ # 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 += [
+ # pass the address and write lane under test to both memories
+ mem1.dbg_addr.eq(self.dbg_addr),
+ mem2.dbg_addr.eq(self.dbg_addr),
+ mem3.dbg_addr.eq(self.dbg_addr),
+ mem1.dbg_lane.eq(self.dbg_lane),
+ mem2.dbg_lane.eq(self.dbg_lane),
+ mem3.dbg_lane.eq(self.dbg_lane),
+ # the other memories copy their state from the first memory,
+ # after a cycle, so they have a one cycle delay
+ mem1.dbg_data.eq(self.dbg_data),
+ mem2.dbg_data.eq(Past(self.dbg_data)),
+ mem3.dbg_data.eq(Past(self.dbg_data)),
+ mem1.dbg_wrote.eq(self.dbg_wrote),
+ mem2.dbg_wrote.eq(Past(self.dbg_wrote)),
+ mem3.dbg_wrote.eq(Past(self.dbg_wrote)),
+ ]
+
return m
class PhasedReadPhasedWriteFullReadSRAMTestCase(FHDLTestCase):
- def do_test_case(self, write_phase):
+ def do_test_case(self, write_phase, transparent):
"""
Simulate some read/write/modify operations
"""
- dut = PhasedReadPhasedWriteFullReadSRAM(7, 32, 4, write_phase)
+ dut = PhasedReadPhasedWriteFullReadSRAM(7, 32, 4, write_phase,
+ transparent)
sim = Simulator(dut)
sim.add_clock(1e-6)
yield from skip_write()
yield
# try reading and writing at the same time
- yield from read(0x42, 0x12563478)
- # transparent port, should return the value just written
+ if transparent:
+ # transparent port, return the value just written
+ yield from read(0x42, 0x55AA9966)
+ else:
+ # ... otherwise, return the old value
+ yield from read(0x42, 0x12563478)
+ # transparent port, always return the value just written
yield from phased_read(0x42, 0x55AA9966)
yield from write(0x42, 0b1111, 0x55AA9966)
yield
- # after a cycle, returns the new value
+ # after a cycle, always returns the new value
yield from read(0x42, 0x55AA9966)
yield from skip_write()
yield
sim.add_sync_process(process)
debug_file = 'test_phased_read_write_sram_' + str(write_phase)
+ if transparent:
+ debug_file += '_transparent'
traces = ['clk', 'phase',
{'comment': 'phased write port'},
'wr_addr_i[6:0]', 'wr_we_i[3:0]', 'wr_data_i[31:0]',
def test_case(self):
"""test both types (odd and even write ports) of phased memory"""
with self.subTest("writes happen on phase 0"):
- self.do_test_case(0)
+ self.do_test_case(0, True)
with self.subTest("writes happen on phase 1"):
- self.do_test_case(1)
+ self.do_test_case(1, True)
+ with self.subTest("writes happen on phase 0 (non-transparent reads)"):
+ self.do_test_case(0, False)
+ with self.subTest("writes happen on phase 1 (non-transparent reads)"):
+ self.do_test_case(1, False)
+
+ def do_test_formal(self, write_phase, transparent):
+ """
+ Formal proof of the pseudo 1W/2R regfile
+ """
+ m = Module()
+ # 128 x 32-bit, 8-bit granularity
+ dut = PhasedReadPhasedWriteFullReadSRAM(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
+ lane = AnyConst(range(dut.we_width))
+ # 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.wr_we_i.bit_select(lane, 1)
+ & (dut.phase == dut.write_phase)):
+ m.d.sync += d_reg.eq(dut.wr_data_i.word_select(lane, 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):
+ 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)
+ & Past(dut.phase) == dut.write_phase):
+ # simultaneous write -> check against last written value
+ with m.If(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)
+ # same for the phased read port, except it's always transparent
+ # and the port works only on the write phase
+ with m.If((Past(dut.rdp_addr_i) == a_const) & wrote
+ & (Past(dut.phase) == dut.write_phase)):
+ rdp_lane = dut.rdp_data_o.word_select(lane, gran)
+ m.d.sync += Assert(d_reg == rdp_lane)
+
+ # 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_lane.eq(lane),
+ # state of our holding register
+ dut.dbg_data.eq(d_reg),
+ dut.dbg_wrote.eq(wrote),
+ ]
+
+ self.assertFormal(m, mode="prove", depth=3)
+
+ def test_formal(self):
+ """test both types (odd and even write ports) of phased write memory"""
+ with self.subTest("writes happen on phase 0"):
+ self.do_test_formal(0, False)
+ with self.subTest("writes happen on phase 1"):
+ self.do_test_formal(1, False)
+ # test again, with transparent read ports
+ with self.subTest("writes happen on phase 0 (transparent reads)"):
+ self.do_test_formal(0, True)
+ with self.subTest("writes happen on phase 1 (transparent reads)"):
+ self.do_test_formal(1, True)
if __name__ == "__main__":
projects / soc.git / blobdiff