src/soc/regfile/sram_wrapper.py

   1 # SPDX-License-Identifier: LGPLv3+
   2 # Copyright (C) 2022 Cesar Strauss <cestrauss@gmail.com>
   3 # Sponsored by NLnet and NGI POINTER under EU Grants 871528 and 957073
   4 # Part of the Libre-SOC Project.
   5
   6 """
   7 Wrapper around a single port (1R or 1W) SRAM, to make a multi-port regfile.
   8
   9 This SRAM primitive has one cycle delay for reads, and, after a write,
  10 it reads the value just written. The goal is to use it to make at least an
  11 1W2R regfile.
  12
  13 See https://bugs.libre-soc.org/show_bug.cgi?id=781 and
  14 https://bugs.libre-soc.org/show_bug.cgi?id=502
  15 """
  16
  17 import unittest
  18
  19 from nmigen import Elaboratable, Module, Memory, Signal, Repl, Mux
  20 from nmigen.back import rtlil
  21 from nmigen.sim import Simulator
  22 from nmigen.asserts import Assert, Assume, Past, AnyConst
  23
  24 from nmutil.formaltest import FHDLTestCase
  25 from nmutil.gtkw import write_gtkw
  26
  27
  28 class SinglePortSRAM(Elaboratable):
  29     """
  30     Model of a single port SRAM, which can be simulated, verified and/or
  31     synthesized to an FPGA.
  32
  33     :param addr_width: width of the address bus
  34     :param data_width: width of the data bus
  35     :param we_width: number of write enable lines
  36
  37     .. note:: The debug read port is meant only to assist in formal proofs!
  38     """
  39     def __init__(self, addr_width, data_width, we_width):
  40         self.addr_width = addr_width
  41         self.data_width = data_width
  42         self.we_width = we_width
  43         # interface signals
  44         self.d = Signal(data_width); """ write data"""
  45         self.q = Signal(data_width); """read data"""
  46         self.a = Signal(addr_width); """ read/write address"""
  47         self.we = Signal(we_width); """write enable"""
  48         # debug signals, only used in formal proofs
  49         self.dbg_addr = Signal(addr_width); """debug: address under test"""
  50         lanes = range(we_width)
  51         self.dbg_lane = Signal(lanes); """debug: write lane under test"""
  52         gran = self.data_width // self.we_width
  53         self.dbg_data = Signal(gran); """debug: data to keep in sync"""
  54         self.dbg_wrote = Signal(); """debug: data is valid"""
  55
  56     def elaborate(self, platform):
  57         m = Module()
  58         # backing memory
  59         depth = 1 << self.addr_width
  60         gran = self.data_width // self.we_width
  61         mem = Memory(width=self.data_width, depth=depth)
  62         # create read and write ports
  63         # By connecting the same address to both ports, they behave, in fact,
  64         # as a single, "half-duplex" port.
  65         # The transparent attribute means that, on a write, we read the new
  66         # value, on the next cycle
  67         # Note that nmigen memories have a one cycle delay, for reads,
  68         # by default
  69         m.submodules.rdport = rdport = mem.read_port(transparent=True)
  70         m.submodules.wrport = wrport = mem.write_port(granularity=gran)
  71         # duplicate the address to both ports
  72         m.d.comb += wrport.addr.eq(self.a)
  73         m.d.comb += rdport.addr.eq(self.a)
  74         # write enable
  75         m.d.comb += wrport.en.eq(self.we)
  76         # read and write data
  77         m.d.comb += wrport.data.eq(self.d)
  78         m.d.comb += self.q.eq(rdport.data)
  79
  80         # the following is needed for induction, where an unreachable state
  81         # (memory and holding register differ) is turned into an illegal one
  82         if platform == "formal":
  83             # the debug port is an asynchronous read port, allowing direct
  84             # access to a given memory location by the formal engine
  85             m.submodules.dbgport = dbgport = mem.read_port(domain="comb")
  86             # first, get the value stored in our memory location,
  87             # using its debug port
  88             stored = Signal(self.data_width)
  89             m.d.comb += dbgport.addr.eq(self.dbg_addr)
  90             m.d.comb += stored.eq(dbgport.data)
  91             # now, ensure that the value stored in memory is always in sync
  92             # with the holding register
  93             with m.If(self.dbg_wrote):
  94                 m.d.sync += Assert(self.dbg_data ==
  95                                    stored.word_select(self.dbg_lane, gran))
  96
  97         return m
  98
  99     def ports(self):
 100         return [
 101             self.d,
 102             self.a,
 103             self.we,
 104             self.q
 105         ]
 106
 107
 108 def create_ilang(dut, ports, test_name):
 109     vl = rtlil.convert(dut, name=test_name, ports=ports)
 110     with open("%s.il" % test_name, "w") as f:
 111         f.write(vl)
 112
 113
 114 class SinglePortSRAMTestCase(FHDLTestCase):
 115     @staticmethod
 116     def test_simple_rtlil():
 117         """
 118         Generate a simple SRAM. Try ``read_rtlil mem_simple.il; proc; show``
 119         from a yosys prompt, to see the memory primitives, and
 120         ``read_rtlil mem_simple.il; synth; show`` to see it implemented as
 121         flip-flop RAM
 122         """
 123         dut = SinglePortSRAM(2, 4, 2)
 124         create_ilang(dut, dut.ports(), "mem_simple")
 125
 126     @staticmethod
 127     def test_blkram_rtlil():
 128         """
 129         Generates a bigger SRAM.
 130         Try ``read_rtlil mem_blkram.il; synth_ecp5; show`` from a yosys
 131         prompt, to see it implemented as block RAM
 132         """
 133         dut = SinglePortSRAM(10, 16, 2)
 134         create_ilang(dut, dut.ports(), "mem_blkram")
 135
 136     def test_sram_model(self):
 137         """
 138         Simulate some read/write/modify operations on the SRAM model
 139         """
 140         dut = SinglePortSRAM(7, 32, 4)
 141         sim = Simulator(dut)
 142         sim.add_clock(1e-6)
 143
 144         def process():
 145             # 1) write 0x12_34_56_78 to address 0
 146             yield dut.a.eq(0)
 147             yield dut.d.eq(0x12_34_56_78)
 148             yield dut.we.eq(0b1111)
 149             yield
 150             # 2) write 0x9A_BC_DE_F0 to address 1
 151             yield dut.a.eq(1)
 152             yield dut.d.eq(0x9A_BC_DE_F0)
 153             yield dut.we.eq(0b1111)
 154             yield
 155             # ... and read value just written to address 0
 156             self.assertEqual((yield dut.q), 0x12_34_56_78)
 157             # 3) prepare to read from address 0
 158             yield dut.d.eq(0)
 159             yield dut.we.eq(0b0000)
 160             yield dut.a.eq(0)
 161             yield
 162             # ... and read value just written to address 1
 163             self.assertEqual((yield dut.q), 0x9A_BC_DE_F0)
 164             # 4) prepare to read from address 1
 165             yield dut.a.eq(1)
 166             yield
 167             # ... and read value from address 0
 168             self.assertEqual((yield dut.q), 0x12_34_56_78)
 169             # 5) write 0x9A and 0xDE to bytes 1 and 3, leaving
 170             # bytes 0 and 2 unchanged
 171             yield dut.a.eq(0)
 172             yield dut.d.eq(0x9A_FF_DE_FF)
 173             yield dut.we.eq(0b1010)
 174             yield
 175             # ... and read value from address 1
 176             self.assertEqual((yield dut.q), 0x9A_BC_DE_F0)
 177             # 6) nothing more to do
 178             yield dut.d.eq(0)
 179             yield dut.we.eq(0)
 180             yield
 181             # ... other than confirm that bytes 1 and 3 were modified
 182             # correctly
 183             self.assertEqual((yield dut.q), 0x9A_34_DE_78)
 184
 185         sim.add_sync_process(process)
 186         traces = ['rdport.clk', 'a[6:0]', 'we[3:0]', 'd[31:0]', 'q[31:0]']
 187         write_gtkw('test_sram_model.gtkw', 'test_sram_model.vcd',
 188                    traces, module='top')
 189         sim_writer = sim.write_vcd('test_sram_model.vcd')
 190         with sim_writer:
 191             sim.run()
 192
 193     def test_model_sram_proof(self):
 194         """
 195         Formal proof of the single port SRAM model
 196         """
 197         m = Module()
 198         # 128 x 32-bit, 8-bit granularity
 199         m.submodules.dut = dut = SinglePortSRAM(7, 32, 4)
 200         gran = len(dut.d) // len(dut.we)  # granularity
 201         # choose a single random memory location to test
 202         a_const = AnyConst(dut.a.shape())
 203         # choose a single byte lane to test
 204         lane = AnyConst(range(dut.we_width))
 205         # holding data register
 206         d_reg = Signal(gran)
 207         # for some reason, simulated formal memory is not zeroed at reset
 208         # ... so, remember whether we wrote it, at least once.
 209         wrote = Signal()
 210         # if our memory location and byte lane is being written
 211         # ... capture the data in our holding register
 212         with m.If((dut.a == a_const) & dut.we.bit_select(lane, 1)):
 213             m.d.sync += d_reg.eq(dut.d.word_select(lane, gran))
 214             m.d.sync += wrote.eq(1)
 215         # if our memory location is being read
 216         # ... and the holding register has valid data
 217         # ... then its value must match the memory output, on the given lane
 218         with m.If((Past(dut.a) == a_const) & wrote):
 219             m.d.sync += Assert(d_reg == dut.q.word_select(lane, gran))
 220
 221         # pass our state to the device under test, so it can ensure that
 222         # its state is in sync with ours, for induction
 223         m.d.comb += [
 224             dut.dbg_addr.eq(a_const),
 225             dut.dbg_lane.eq(lane),
 226             dut.dbg_data.eq(d_reg),
 227             dut.dbg_wrote.eq(wrote),
 228         ]
 229
 230         self.assertFormal(m, mode="prove", depth=2)
 231
 232
 233 class PhasedDualPortRegfile(Elaboratable):
 234     """
 235     Builds, from a pair of 1RW blocks, a pseudo 1W/1R RAM, where the
 236     read port works every cycle, but the write port is only available on
 237     either even (1eW/1R) or odd (1oW/1R) cycles.
 238
 239     :param addr_width: width of the address bus
 240     :param data_width: width of the data bus
 241     :param we_width: number of write enable lines
 242     :param write_phase: indicates on which phase the write port will
 243                         accept data
 244     :param transparent: whether a simultaneous read and write returns the
 245                         new value (True) or the old value (False)
 246
 247     .. note:: The debug read port is meant only to assist in formal proofs!
 248     """
 249
 250     def __init__(self, addr_width, data_width, we_width, write_phase,
 251                  transparent=False):
 252         self.addr_width = addr_width
 253         self.data_width = data_width
 254         self.we_width = we_width
 255         self.write_phase = write_phase
 256         self.transparent = transparent
 257         # interface signals
 258         self.wr_addr_i = Signal(addr_width); """write port address"""
 259         self.wr_data_i = Signal(data_width); """write port data"""
 260         self.wr_we_i = Signal(we_width); """write port enable"""
 261         self.rd_addr_i = Signal(addr_width); """read port address"""
 262         self.rd_data_o = Signal(data_width); """read port data"""
 263         self.phase = Signal(); """even/odd cycle indicator"""
 264         # debug signals, only used in formal proofs
 265         self.dbg_addr = Signal(addr_width); """debug: address under test"""
 266         lanes = range(we_width)
 267         self.dbg_lane = Signal(lanes); """debug: write lane under test"""
 268         gran = self.data_width // self.we_width
 269         self.dbg_data = Signal(gran); """debug: data to keep in sync"""
 270         self.dbg_wrote = Signal(); """debug: data is valid"""
 271
 272     def elaborate(self, platform):
 273         m = Module()
 274         # granularity
 275         # instantiate the two 1RW memory blocks
 276         mem1 = SinglePortSRAM(self.addr_width, self.data_width, self.we_width)
 277         mem2 = SinglePortSRAM(self.addr_width, self.data_width, self.we_width)
 278         m.submodules.mem1 = mem1
 279         m.submodules.mem2 = mem2
 280         # wire write port to first memory, and its output to the second
 281         m.d.comb += mem1.d.eq(self.wr_data_i)
 282         m.d.comb += mem2.d.eq(mem1.q)
 283         # holding registers for the write port of the second memory
 284         last_wr_addr = Signal(self.addr_width)
 285         last_wr_we = Signal(self.we_width)
 286         # do the read and write address coincide?
 287         same_read_write = Signal()
 288         with m.If(self.phase == self.write_phase):
 289             # write phase, start a write on the first memory
 290             m.d.comb += mem1.a.eq(self.wr_addr_i)
 291             m.d.comb += mem1.we.eq(self.wr_we_i)
 292             # save write address and write select for repeating the write
 293             # on the second memory, later
 294             m.d.sync += last_wr_we.eq(self.wr_we_i)
 295             m.d.sync += last_wr_addr.eq(self.wr_addr_i)
 296             # start a read on the second memory
 297             m.d.comb += mem2.a.eq(self.rd_addr_i)
 298             # output previously read data from the first memory
 299             m.d.comb += self.rd_data_o.eq(mem1.q)
 300             if self.transparent:
 301                 # remember whether we are reading from the same location we are
 302                 # writing
 303                 m.d.sync += same_read_write.eq(self.rd_addr_i == self.wr_addr_i)
 304         with m.Else():
 305             # read phase, write last written data on second memory
 306             m.d.comb += mem2.a.eq(last_wr_addr)
 307             m.d.comb += mem2.we.eq(last_wr_we)
 308             # start a read on the first memory
 309             m.d.comb += mem1.a.eq(self.rd_addr_i)
 310             if self.transparent:
 311                 with m.If(same_read_write):
 312                     # when transparent, and read and write addresses coincide,
 313                     # output the data just written
 314                     m.d.comb += self.rd_data_o.eq(mem1.q)
 315                 with m.Else():
 316                     # otherwise, output previously read data
 317                     # from the second memory
 318                     m.d.comb += self.rd_data_o.eq(mem2.q)
 319             else:
 320                 # always output the read data from the second memory,
 321                 # if not transparent
 322                 m.d.comb += self.rd_data_o.eq(mem2.q)
 323
 324         if platform == "formal":
 325             # pass our state to the device under test, so it can ensure that
 326             # its state is in sync with ours, for induction
 327             m.d.comb += [
 328                 # pass the address and write lane under test to both memories
 329                 mem1.dbg_addr.eq(self.dbg_addr),
 330                 mem2.dbg_addr.eq(self.dbg_addr),
 331                 mem1.dbg_lane.eq(self.dbg_lane),
 332                 mem2.dbg_lane.eq(self.dbg_lane),
 333                 # the second memory copies its state from the first memory,
 334                 # after a cycle, so it has a one cycle delay
 335                 mem1.dbg_data.eq(self.dbg_data),
 336                 mem2.dbg_data.eq(Past(self.dbg_data)),
 337                 mem1.dbg_wrote.eq(self.dbg_wrote),
 338                 mem2.dbg_wrote.eq(Past(self.dbg_wrote)),
 339             ]
 340
 341         return m
 342
 343
 344 class PhasedDualPortRegfileTestCase(FHDLTestCase):
 345
 346     def do_test_phased_dual_port_regfile(self, write_phase, transparent):
 347         """
 348         Simulate some read/write/modify operations on the phased write memory
 349         """
 350         dut = PhasedDualPortRegfile(7, 32, 4, write_phase, transparent)
 351         sim = Simulator(dut)
 352         sim.add_clock(1e-6)
 353
 354         # compare read data with previously written data
 355         # and start a new read
 356         def read(rd_addr_i, expected=None):
 357             if expected is not None:
 358                 self.assertEqual((yield dut.rd_data_o), expected)
 359             yield dut.rd_addr_i.eq(rd_addr_i)
 360
 361         # start a write, and set write phase
 362         def write(wr_addr_i, wr_we_i, wr_data_i):
 363             yield dut.wr_addr_i.eq(wr_addr_i)
 364             yield dut.wr_we_i.eq(wr_we_i)
 365             yield dut.wr_data_i.eq(wr_data_i)
 366             yield dut.phase.eq(write_phase)
 367
 368         # disable writes, and start read phase
 369         def skip_write():
 370             yield dut.wr_addr_i.eq(0)
 371             yield dut.wr_we_i.eq(0)
 372             yield dut.wr_data_i.eq(0)
 373             yield dut.phase.eq(~write_phase)
 374
 375         # writes a few values on the write port, and read them back
 376         # ... reads can happen every cycle
 377         # ... writes, only every two cycles.
 378         # since reads have a one cycle delay, the expected value on
 379         # each read refers to the last read performed, not the
 380         # current one, which is in progress.
 381         def process():
 382             yield from read(0)
 383             yield from write(0x42, 0b1111, 0x12345678)
 384             yield
 385             yield from read(0x42)
 386             yield from skip_write()
 387             yield
 388             yield from read(0x42)
 389             yield from write(0x43, 0b1111, 0x9ABCDEF0)
 390             yield
 391             yield from read(0x43, 0x12345678)
 392             yield from skip_write()
 393             yield
 394             yield from read(0x42, 0x12345678)
 395             yield from write(0x43, 0b1001, 0xF0FFFF9A)
 396             yield
 397             yield from read(0x43, 0x9ABCDEF0)
 398             yield from skip_write()
 399             yield
 400             yield from read(0x43, 0x12345678)
 401             yield from write(0x42, 0b0110, 0xFF5634FF)
 402             yield
 403             yield from read(0x42, 0xF0BCDE9A)
 404             yield from skip_write()
 405             yield
 406             yield from read(0, 0xF0BCDE9A)
 407             yield from write(0, 0, 0)
 408             yield
 409             yield from read(0, 0x12563478)
 410             yield from skip_write()
 411             yield
 412             # try reading and writing to the same location, simultaneously
 413             yield from read(0x42)
 414             yield from write(0x42, 0b1111, 0x55AA9966)
 415             yield
 416             # ... and read again
 417             yield from read(0x42)
 418             yield from skip_write()
 419             yield
 420             if transparent:
 421                 # returns the value just written
 422                 yield from read(0, 0x55AA9966)
 423             else:
 424                 # returns the old value
 425                 yield from read(0, 0x12563478)
 426             yield from write(0, 0, 0)
 427             yield
 428             # after a cycle, always returns the new value
 429             yield from read(0, 0x55AA9966)
 430             yield from skip_write()
 431
 432         sim.add_sync_process(process)
 433         debug_file = f'test_phased_dual_port_{write_phase}'
 434         if transparent:
 435             debug_file += '_transparent'
 436         traces = ['clk', 'phase',
 437                   'wr_addr_i[6:0]', 'wr_we_i[3:0]', 'wr_data_i[31:0]',
 438                   'rd_addr_i[6:0]', 'rd_data_o[31:0]']
 439         write_gtkw(debug_file + '.gtkw',
 440                    debug_file + '.vcd',
 441                    traces, module='top', zoom=-22)
 442         sim_writer = sim.write_vcd(debug_file + '.vcd')
 443         with sim_writer:
 444             sim.run()
 445
 446     def test_phased_dual_port_regfile(self):
 447         """test both types (odd and even write ports) of phased write memory"""
 448         with self.subTest("writes happen on phase 0"):
 449             self.do_test_phased_dual_port_regfile(0, False)
 450         with self.subTest("writes happen on phase 1"):
 451             self.do_test_phased_dual_port_regfile(1, False)
 452         """test again, with a transparent read port"""
 453         with self.subTest("writes happen on phase 0 (transparent reads)"):
 454             self.do_test_phased_dual_port_regfile(0, True)
 455         with self.subTest("writes happen on phase 1 (transparent reads)"):
 456             self.do_test_phased_dual_port_regfile(1, True)
 457
 458     def do_test_phased_dual_port_regfile_proof(self, write_phase, transparent):
 459         """
 460         Formal proof of the pseudo 1W/1R regfile
 461         """
 462         m = Module()
 463         # 128 x 32-bit, 8-bit granularity
 464         dut = PhasedDualPortRegfile(7, 32, 4, write_phase, transparent)
 465         m.submodules.dut = dut
 466         gran = dut.data_width // dut.we_width  # granularity
 467         # choose a single random memory location to test
 468         a_const = AnyConst(dut.addr_width)
 469         # choose a single byte lane to test
 470         lane = AnyConst(range(dut.we_width))
 471         # drive alternating phases
 472         m.d.comb += Assume(dut.phase != Past(dut.phase))
 473         # holding data register
 474         d_reg = Signal(gran)
 475         # for some reason, simulated formal memory is not zeroed at reset
 476         # ... so, remember whether we wrote it, at least once.
 477         wrote = Signal()
 478         # if our memory location and byte lane is being written,
 479         # capture the data in our holding register
 480         with m.If((dut.wr_addr_i == a_const)
 481                   & dut.wr_we_i.bit_select(lane, 1)
 482                   & (dut.phase == dut.write_phase)):
 483             m.d.sync += d_reg.eq(dut.wr_data_i.word_select(lane, gran))
 484             m.d.sync += wrote.eq(1)
 485         # if our memory location is being read,
 486         # and the holding register has valid data,
 487         # then its value must match the memory output, on the given lane
 488         with m.If(Past(dut.rd_addr_i) == a_const):
 489             if transparent:
 490                 with m.If(wrote):
 491                     rd_lane = dut.rd_data_o.word_select(lane, gran)
 492                     m.d.sync += Assert(d_reg == rd_lane)
 493             else:
 494                 # with a non-transparent read port, the read value depends
 495                 # on whether there is a simultaneous write, or not
 496                 with m.If((Past(dut.wr_addr_i) == a_const)
 497                           & Past(dut.phase) == dut.write_phase):
 498                     # simultaneous write -> check against last written value
 499                     with m.If(Past(wrote)):
 500                         rd_lane = dut.rd_data_o.word_select(lane, gran)
 501                         m.d.sync += Assert(Past(d_reg) == rd_lane)
 502                 with m.Else():
 503                     # otherwise, check against current written value
 504                     with m.If(wrote):
 505                         rd_lane = dut.rd_data_o.word_select(lane, gran)
 506                         m.d.sync += Assert(d_reg == rd_lane)
 507
 508         # pass our state to the device under test, so it can ensure that
 509         # its state is in sync with ours, for induction
 510         m.d.comb += [
 511             # address and mask under test
 512             dut.dbg_addr.eq(a_const),
 513             dut.dbg_lane.eq(lane),
 514             # state of our holding register
 515             dut.dbg_data.eq(d_reg),
 516             dut.dbg_wrote.eq(wrote),
 517         ]
 518
 519         self.assertFormal(m, mode="prove", depth=3)
 520
 521     def test_phased_dual_port_regfile_proof(self):
 522         """test both types (odd and even write ports) of phased write memory"""
 523         with self.subTest("writes happen on phase 0"):
 524             self.do_test_phased_dual_port_regfile_proof(0, False)
 525         with self.subTest("writes happen on phase 1"):
 526             self.do_test_phased_dual_port_regfile_proof(1, False)
 527         # test again, with transparent read ports
 528         with self.subTest("writes happen on phase 0 (transparent reads)"):
 529             self.do_test_phased_dual_port_regfile_proof(0, True)
 530         with self.subTest("writes happen on phase 1 (transparent reads)"):
 531             self.do_test_phased_dual_port_regfile_proof(1, True)
 532
 533
 534 class DualPortRegfile(Elaboratable):
 535     """
 536     Builds, from a pair of phased 1W/1R blocks, a true 1W/1R RAM, where both
 537     read and write ports work every cycle.
 538     It employs a Last Value Table, that tracks to which memory each address was
 539     last written.
 540
 541     :param addr_width: width of the address bus
 542     :param data_width: width of the data bus
 543     :param we_width: number of write enable lines
 544     :param transparent: whether a simultaneous read and write returns the
 545                         new value (True) or the old value (False)
 546     """
 547
 548     def __init__(self, addr_width, data_width, we_width, transparent=True):
 549         self.addr_width = addr_width
 550         self.data_width = data_width
 551         self.we_width = we_width
 552         self.transparent = transparent
 553         # interface signals
 554         self.wr_addr_i = Signal(addr_width); """write port address"""
 555         self.wr_data_i = Signal(data_width); """write port data"""
 556         self.wr_we_i = Signal(we_width); """write port enable"""
 557         self.rd_addr_i = Signal(addr_width); """read port address"""
 558         self.rd_data_o = Signal(data_width); """read port data"""
 559         # debug signals, only used in formal proofs
 560         # address and write lane under test
 561         self.dbg_addr = Signal(addr_width); """debug: address under test"""
 562         lanes = range(we_width)
 563         self.dbg_lane = Signal(lanes); """debug: write lane under test"""
 564         # upstream state, to keep in sync with ours
 565         gran = self.data_width // self.we_width
 566         self.dbg_data = Signal(gran); """debug: data to keep in sync"""
 567         self.dbg_wrote = Signal(); """debug: data is valid"""
 568         self.dbg_wrote_phase = Signal(); """debug: the phase data was written"""
 569         self.dbg_phase = Signal(); """debug: current phase"""
 570
 571     def elaborate(self, platform):
 572         m = Module()
 573         # depth and granularity
 574         depth = 1 << self.addr_width
 575         gran = self.data_width // self.we_width
 576         # instantiate the two phased 1R/1W memory blocks
 577         mem0 = PhasedDualPortRegfile(
 578             self.addr_width, self.data_width, self.we_width, 0,
 579             self.transparent)
 580         mem1 = PhasedDualPortRegfile(
 581             self.addr_width, self.data_width, self.we_width, 1,
 582             self.transparent)
 583         m.submodules.mem0 = mem0
 584         m.submodules.mem1 = mem1
 585         # instantiate the backing memory (FFRAM or LUTRAM)
 586         # for the Last Value Table
 587         # it should have the same number and port types of the desired
 588         # memory, but just one bit per write lane
 589         lvt_mem = Memory(width=self.we_width, depth=depth)
 590         lvt_wr = lvt_mem.write_port(granularity=1)
 591         lvt_rd = lvt_mem.read_port(transparent=self.transparent)
 592         m.submodules.lvt_wr = lvt_wr
 593         m.submodules.lvt_rd = lvt_rd
 594         # generate and wire the phases for the phased memories
 595         phase = Signal()
 596         m.d.sync += phase.eq(~phase)
 597         m.d.comb += [
 598             mem0.phase.eq(phase),
 599             mem1.phase.eq(phase),
 600         ]
 601         m.d.comb += [
 602             # wire the write ports, directly
 603             mem0.wr_addr_i.eq(self.wr_addr_i),
 604             mem1.wr_addr_i.eq(self.wr_addr_i),
 605             mem0.wr_we_i.eq(self.wr_we_i),
 606             mem1.wr_we_i.eq(self.wr_we_i),
 607             mem0.wr_data_i.eq(self.wr_data_i),
 608             mem1.wr_data_i.eq(self.wr_data_i),
 609             # also wire the read addresses
 610             mem0.rd_addr_i.eq(self.rd_addr_i),
 611             mem1.rd_addr_i.eq(self.rd_addr_i),
 612             # wire read and write ports to the LVT
 613             lvt_wr.addr.eq(self.wr_addr_i),
 614             lvt_wr.en.eq(self.wr_we_i),
 615             lvt_rd.addr.eq(self.rd_addr_i),
 616             # the data for the LVT is the phase on which the value was
 617             # written
 618             lvt_wr.data.eq(Repl(phase, self.we_width)),
 619         ]
 620         for i in range(self.we_width):
 621             # select the right memory to assign to the output read port,
 622             # in this byte lane, according to the LVT contents
 623             m.d.comb += self.rd_data_o.word_select(i, gran).eq(
 624                 Mux(
 625                     lvt_rd.data[i],
 626                     mem1.rd_data_o.word_select(i, gran),
 627                     mem0.rd_data_o.word_select(i, gran)))
 628
 629         if platform == "formal":
 630             # pass upstream state to the memories, so they can ensure that
 631             # their state are in sync with upstream, for induction
 632             m.d.comb += [
 633                 # address and write lane under test
 634                 mem0.dbg_addr.eq(self.dbg_addr),
 635                 mem1.dbg_addr.eq(self.dbg_addr),
 636                 mem0.dbg_lane.eq(self.dbg_lane),
 637                 mem1.dbg_lane.eq(self.dbg_lane),
 638                 # upstream state
 639                 mem0.dbg_data.eq(self.dbg_data),
 640                 mem1.dbg_data.eq(self.dbg_data),
 641                 # the memory, on which the write ends up, depends on which
 642                 # phase it was written
 643                 mem0.dbg_wrote.eq(self.dbg_wrote & ~self.dbg_wrote_phase),
 644                 mem1.dbg_wrote.eq(self.dbg_wrote & self.dbg_wrote_phase),
 645             ]
 646             # sync phase to upstream
 647             m.d.comb += Assert(self.dbg_phase == phase)
 648             # this debug port for the LVT is an asynchronous read port,
 649             # allowing direct access to a given memory location
 650             # by the formal engine
 651             m.submodules.dbgport = dbgport = lvt_mem.read_port(domain='comb')
 652             # first, get the value stored in our memory location,
 653             stored = Signal(self.we_width)
 654             m.d.comb += dbgport.addr.eq(self.dbg_addr)
 655             m.d.comb += stored.eq(dbgport.data)
 656             # now, ensure that the value stored in memory is always in sync
 657             # with the expected value (which memory the value was written to)
 658             with m.If(self.dbg_wrote):
 659                 m.d.comb += Assert(stored.bit_select(self.dbg_lane, 1)
 660                                    == self.dbg_wrote_phase)
 661         return m
 662
 663
 664 class DualPortRegfileTestCase(FHDLTestCase):
 665
 666     def do_test_dual_port_regfile(self, transparent):
 667         """
 668         Simulate some read/write/modify operations on the dual port register
 669         file
 670         """
 671         dut = DualPortRegfile(7, 32, 4, transparent)
 672         sim = Simulator(dut)
 673         sim.add_clock(1e-6)
 674
 675         expected = None
 676         last_expected = None
 677
 678         # compare read data with previously written data
 679         # and start a new read
 680         def read(rd_addr_i, next_expected=None):
 681             nonlocal expected, last_expected
 682             if expected is not None:
 683                 self.assertEqual((yield dut.rd_data_o), expected)
 684             yield dut.rd_addr_i.eq(rd_addr_i)
 685             # account for the read latency
 686             expected = last_expected
 687             last_expected = next_expected
 688
 689         # start a write
 690         def write(wr_addr_i, wr_we_i, wr_data_i):
 691             yield dut.wr_addr_i.eq(wr_addr_i)
 692             yield dut.wr_we_i.eq(wr_we_i)
 693             yield dut.wr_data_i.eq(wr_data_i)
 694
 695         def process():
 696             # write a pair of values, one for each memory
 697             yield from read(0)
 698             yield from write(0x42, 0b1111, 0x87654321)
 699             yield
 700             yield from read(0x42, 0x87654321)
 701             yield from write(0x43, 0b1111, 0x0FEDCBA9)
 702             yield
 703             # skip a beat
 704             yield from read(0x43, 0x0FEDCBA9)
 705             yield from write(0, 0, 0)
 706             yield
 707             # write again, but now they switch memories
 708             yield from read(0)
 709             yield from write(0x42, 0b1111, 0x12345678)
 710             yield
 711             yield from read(0x42, 0x12345678)
 712             yield from write(0x43, 0b1111, 0x9ABCDEF0)
 713             yield
 714             yield from read(0x43, 0x9ABCDEF0)
 715             yield from write(0, 0, 0)
 716             yield
 717             # test partial writes
 718             yield from read(0)
 719             yield from write(0x42, 0b1001, 0x78FFFF12)
 720             yield
 721             yield from read(0)
 722             yield from write(0x43, 0b0110, 0xFFDEABFF)
 723             yield
 724             yield from read(0x42, 0x78345612)
 725             yield from write(0, 0, 0)
 726             yield
 727             yield from read(0x43, 0x9ADEABF0)
 728             yield from write(0, 0, 0)
 729             yield
 730             yield from read(0)
 731             yield from write(0, 0, 0)
 732             yield
 733             if transparent:
 734                 # returns the value just written
 735                 yield from read(0x42, 0x55AA9966)
 736             else:
 737                 # returns the old value
 738                 yield from read(0x42, 0x78345612)
 739             yield from write(0x42, 0b1111, 0x55AA9966)
 740             yield
 741             # after a cycle, always returns the new value
 742             yield from read(0x42, 0x55AA9966)
 743             yield from write(0, 0, 0)
 744             yield
 745             yield from read(0)
 746             yield from write(0, 0, 0)
 747             yield
 748             yield from read(0)
 749             yield from write(0, 0, 0)
 750
 751         sim.add_sync_process(process)
 752         debug_file = 'test_dual_port_regfile'
 753         if transparent:
 754             debug_file += '_transparent'
 755         traces = ['clk', 'phase',
 756                   {'comment': 'write port'},
 757                   'wr_addr_i[6:0]', 'wr_we_i[3:0]', 'wr_data_i[31:0]',
 758                   {'comment': 'read port'},
 759                   'rd_addr_i[6:0]', 'rd_data_o[31:0]',
 760                   {'comment': 'LVT write port'},
 761                   'phase', 'lvt_mem_w_addr[6:0]', 'lvt_mem_w_en[3:0]',
 762                   'lvt_mem_w_data[3:0]',
 763                   {'comment': 'LVT read port'},
 764                   'lvt_mem_r_addr[6:0]', 'lvt_mem_r_data[3:0]',
 765                   {'comment': 'backing memory'},
 766                   'mem0.rd_data_o[31:0]',
 767                   'mem1.rd_data_o[31:0]',
 768                   ]
 769         write_gtkw(debug_file + '.gtkw',
 770                    debug_file + '.vcd',
 771                    traces, module='top', zoom=-22)
 772         sim_writer = sim.write_vcd(debug_file + '.vcd')
 773         with sim_writer:
 774             sim.run()
 775
 776     def test_dual_port_regfile(self):
 777         with self.subTest("non-transparent reads"):
 778             self.do_test_dual_port_regfile(False)
 779         with self.subTest("transparent reads"):
 780             self.do_test_dual_port_regfile(True)
 781
 782     def test_dual_port_regfile_proof(self):
 783         """
 784         Formal proof of the 1W/1R regfile
 785         """
 786         m = Module()
 787         # 128 x 32-bit, 8-bit granularity
 788         dut = DualPortRegfile(7, 32, 4, True)
 789         m.submodules.dut = dut
 790         gran = dut.data_width // dut.we_width  # granularity
 791         # choose a single random memory location to test
 792         a_const = AnyConst(dut.addr_width)
 793         # choose a single byte lane to test
 794         lane = AnyConst(range(dut.we_width))
 795         # holding data register
 796         d_reg = Signal(gran)
 797         # keep track of the phase, so we can remember which memory
 798         # we wrote to
 799         phase = Signal()
 800         m.d.sync += phase.eq(~phase)
 801         # for some reason, simulated formal memory is not zeroed at reset
 802         # ... so, remember whether we wrote it, at least once.
 803         wrote = Signal()
 804         # ... and on which phase it was written
 805         wrote_phase = Signal()
 806         # if our memory location and byte lane is being written,
 807         # capture the data in our holding register
 808         with m.If((dut.wr_addr_i == a_const)
 809                   & dut.wr_we_i.bit_select(lane, 1)):
 810             m.d.sync += d_reg.eq(dut.wr_data_i.word_select(lane, gran))
 811             m.d.sync += wrote.eq(1)
 812             m.d.sync += wrote_phase.eq(phase)
 813         # if our memory location is being read,
 814         # and the holding register has valid data,
 815         # then its value must match the memory output, on the given lane
 816         with m.If(Past(dut.rd_addr_i) == a_const):
 817             with m.If(wrote):
 818                 rd_lane = dut.rd_data_o.word_select(lane, gran)
 819                 m.d.sync += Assert(d_reg == rd_lane)
 820
 821         m.d.comb += [
 822             dut.dbg_addr.eq(a_const),
 823             dut.dbg_lane.eq(lane),
 824             dut.dbg_data.eq(d_reg),
 825             dut.dbg_wrote.eq(wrote),
 826             dut.dbg_wrote_phase.eq(wrote_phase),
 827             dut.dbg_phase.eq(phase),
 828         ]
 829
 830         self.assertFormal(m, mode="prove", depth=3)
 831
 832
 833 if __name__ == "__main__":
 834     unittest.main()