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