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