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         self.dbg_data = Signal(data_width); """debug: data to keep in sync"""
 262         self.dbg_wrote = Signal(addr_width); """debug: data is valid"""
 263
 264     def elaborate(self, platform):
 265         m = Module()
 266         # granularity
 267         gran = self.data_width // self.we_width
 268         # instantiate the two 1RW memory blocks
 269         mem1 = SinglePortSRAM(self.addr_width, self.data_width, self.we_width)
 270         mem2 = SinglePortSRAM(self.addr_width, self.data_width, self.we_width)
 271         m.submodules.mem1 = mem1
 272         m.submodules.mem2 = mem2
 273         # wire write port to first memory, and its output to the second
 274         m.d.comb += mem1.d.eq(self.wr_data_i)
 275         m.d.comb += mem2.d.eq(mem1.q)
 276         # holding registers for the write port of the second memory
 277         last_wr_addr = Signal(self.addr_width)
 278         last_wr_we = Signal(self.we_width)
 279         # do the read and write address coincide?
 280         same_read_write = Signal()
 281         with m.If(self.phase == self.write_phase):
 282             # write phase, start a write on the first memory
 283             m.d.comb += mem1.a.eq(self.wr_addr_i)
 284             m.d.comb += mem1.we.eq(self.wr_we_i)
 285             # save write address and write select for repeating the write
 286             # on the second memory, later
 287             m.d.sync += last_wr_we.eq(self.wr_we_i)
 288             m.d.sync += last_wr_addr.eq(self.wr_addr_i)
 289             # start a read on the second memory
 290             m.d.comb += mem2.a.eq(self.rd_addr_i)
 291             # output previously read data from the first memory
 292             m.d.comb += self.rd_data_o.eq(mem1.q)
 293             if self.transparent:
 294                 # remember whether we are reading from the same location we are
 295                 # writing
 296                 m.d.sync += same_read_write.eq(self.rd_addr_i == self.wr_addr_i)
 297         with m.Else():
 298             # read phase, write last written data on second memory
 299             m.d.comb += mem2.a.eq(last_wr_addr)
 300             m.d.comb += mem2.we.eq(last_wr_we)
 301             # start a read on the first memory
 302             m.d.comb += mem1.a.eq(self.rd_addr_i)
 303             if self.transparent:
 304                 with m.If(same_read_write):
 305                     # when transparent, and read and write addresses coincide,
 306                     # output the data just written
 307                     m.d.comb += self.rd_data_o.eq(mem1.q)
 308                 with m.Else():
 309                     # otherwise, output previously read data
 310                     # from the second memory
 311                     m.d.comb += self.rd_data_o.eq(mem2.q)
 312             else:
 313                 # always output the read data from the second memory,
 314                 # if not transparent
 315                 m.d.comb += self.rd_data_o.eq(mem2.q)
 316
 317         if platform == "formal":
 318             # the following is needed for induction, where an unreachable
 319             # state (memory and holding register differ) is turned into an
 320             # illegal one
 321             # first, get the values stored in our memory location, using its
 322             # debug port
 323             m.d.comb += mem1.dbg_a.eq(self.dbg_addr)
 324             m.d.comb += mem2.dbg_a.eq(self.dbg_addr)
 325             stored1 = Signal(self.data_width)
 326             stored2 = Signal(self.data_width)
 327             m.d.comb += stored1.eq(mem1.dbg_q)
 328             m.d.comb += stored2.eq(mem2.dbg_q)
 329             # now, ensure that the value stored in the first memory is always
 330             # in sync with the holding register
 331             with m.If(self.dbg_wrote):
 332                 for i in range(self.we_width):
 333                     with m.If(self.dbg_we_mask[i]):
 334                         m.d.comb += Assert(
 335                             self.dbg_data == stored1.word_select(i, gran))
 336             # same for the second memory, but one cycle later
 337             with m.If(Past(self.dbg_wrote)):
 338                 for i in range(self.we_width):
 339                     with m.If(self.dbg_we_mask[i]):
 340                         m.d.comb += Assert(
 341                             Past(self.dbg_data) == stored2.word_select(i, gran))
 342
 343         return m
 344
 345
 346 class PhasedDualPortRegfileTestCase(FHDLTestCase):
 347
 348     def do_test_phased_dual_port_regfile(self, write_phase, transparent):
 349         """
 350         Simulate some read/write/modify operations on the phased write memory
 351         """
 352         dut = PhasedDualPortRegfile(7, 32, 4, write_phase, transparent)
 353         sim = Simulator(dut)
 354         sim.add_clock(1e-6)
 355
 356         # compare read data with previously written data
 357         # and start a new read
 358         def read(rd_addr_i, expected=None):
 359             if expected is not None:
 360                 self.assertEqual((yield dut.rd_data_o), expected)
 361             yield dut.rd_addr_i.eq(rd_addr_i)
 362
 363         # start a write, and set write phase
 364         def write(wr_addr_i, wr_we_i, wr_data_i):
 365             yield dut.wr_addr_i.eq(wr_addr_i)
 366             yield dut.wr_we_i.eq(wr_we_i)
 367             yield dut.wr_data_i.eq(wr_data_i)
 368             yield dut.phase.eq(write_phase)
 369
 370         # disable writes, and start read phase
 371         def skip_write():
 372             yield dut.wr_addr_i.eq(0)
 373             yield dut.wr_we_i.eq(0)
 374             yield dut.wr_data_i.eq(0)
 375             yield dut.phase.eq(~write_phase)
 376
 377         # writes a few values on the write port, and read them back
 378         # ... reads can happen every cycle
 379         # ... writes, only every two cycles.
 380         # since reads have a one cycle delay, the expected value on
 381         # each read refers to the last read performed, not the
 382         # current one, which is in progress.
 383         def process():
 384             yield from read(0)
 385             yield from write(0x42, 0b1111, 0x12345678)
 386             yield
 387             yield from read(0x42)
 388             yield from skip_write()
 389             yield
 390             yield from read(0x42)
 391             yield from write(0x43, 0b1111, 0x9ABCDEF0)
 392             yield
 393             yield from read(0x43, 0x12345678)
 394             yield from skip_write()
 395             yield
 396             yield from read(0x42, 0x12345678)
 397             yield from write(0x43, 0b1001, 0xF0FFFF9A)
 398             yield
 399             yield from read(0x43, 0x9ABCDEF0)
 400             yield from skip_write()
 401             yield
 402             yield from read(0x43, 0x12345678)
 403             yield from write(0x42, 0b0110, 0xFF5634FF)
 404             yield
 405             yield from read(0x42, 0xF0BCDE9A)
 406             yield from skip_write()
 407             yield
 408             yield from read(0, 0xF0BCDE9A)
 409             yield from write(0, 0, 0)
 410             yield
 411             yield from read(0, 0x12563478)
 412             yield from skip_write()
 413             yield
 414             # try reading and writing to the same location, simultaneously
 415             yield from read(0x42)
 416             yield from write(0x42, 0b1111, 0x55AA9966)
 417             yield
 418             # ... and read again
 419             yield from read(0x42)
 420             yield from skip_write()
 421             yield
 422             if transparent:
 423                 # returns the value just written
 424                 yield from read(0, 0x55AA9966)
 425             else:
 426                 # returns the old value
 427                 yield from read(0, 0x12563478)
 428             yield from write(0, 0, 0)
 429             yield
 430             # after a cycle, always returns the new value
 431             yield from read(0, 0x55AA9966)
 432             yield from skip_write()
 433
 434         sim.add_sync_process(process)
 435         debug_file = f'test_phased_dual_port_{write_phase}'
 436         if transparent:
 437             debug_file += '_transparent'
 438         traces = ['clk', 'phase',
 439                   'wr_addr_i[6:0]', 'wr_we_i[3:0]', 'wr_data_i[31:0]',
 440                   'rd_addr_i[6:0]', 'rd_data_o[31:0]']
 441         write_gtkw(debug_file + '.gtkw',
 442                    debug_file + '.vcd',
 443                    traces, module='top', zoom=-22)
 444         sim_writer = sim.write_vcd(debug_file + '.vcd')
 445         with sim_writer:
 446             sim.run()
 447
 448     def test_phased_dual_port_regfile(self):
 449         """test both types (odd and even write ports) of phased write memory"""
 450         with self.subTest("writes happen on phase 0"):
 451             self.do_test_phased_dual_port_regfile(0, False)
 452         with self.subTest("writes happen on phase 1"):
 453             self.do_test_phased_dual_port_regfile(1, False)
 454         """test again, with a transparent read port"""
 455         with self.subTest("writes happen on phase 0 (transparent reads)"):
 456             self.do_test_phased_dual_port_regfile(0, True)
 457         with self.subTest("writes happen on phase 1 (transparent reads)"):
 458             self.do_test_phased_dual_port_regfile(1, True)
 459
 460     def do_test_phased_dual_port_regfile_proof(self, write_phase, transparent):
 461         """
 462         Formal proof of the pseudo 1W/1R regfile
 463         """
 464         m = Module()
 465         # 128 x 32-bit, 8-bit granularity
 466         dut = PhasedDualPortRegfile(7, 32, 4, write_phase, transparent)
 467         m.submodules.dut = dut
 468         gran = dut.data_width // dut.we_width  # granularity
 469         # choose a single random memory location to test
 470         a_const = AnyConst(dut.addr_width)
 471         # choose a single byte lane to test (one-hot encoding)
 472         we_mask = Signal(dut.we_width)
 473         # ... by first creating a random bit pattern
 474         we_const = AnyConst(dut.we_width)
 475         # ... and zeroing all but the first non-zero bit
 476         m.d.comb += we_mask.eq(we_const & (-we_const))
 477         # drive alternating phases
 478         m.d.comb += Assume(dut.phase != Past(dut.phase))
 479         # holding data register
 480         d_reg = Signal(gran)
 481         # for some reason, simulated formal memory is not zeroed at reset
 482         # ... so, remember whether we wrote it, at least once.
 483         wrote = Signal()
 484         # if our memory location and byte lane is being written,
 485         # capture the data in our holding register
 486         with m.If((dut.wr_addr_i == a_const)
 487                   & (dut.phase == dut.write_phase)):
 488             for i in range(dut.we_width):
 489                 with m.If(we_mask[i] & dut.wr_we_i[i]):
 490                     m.d.sync += d_reg.eq(
 491                         dut.wr_data_i[i * gran:i * gran + gran])
 492                     m.d.sync += wrote.eq(1)
 493         # if our memory location is being read,
 494         # and the holding register has valid data,
 495         # then its value must match the memory output, on the given lane
 496         with m.If(Past(dut.rd_addr_i) == a_const):
 497             if transparent:
 498                 with m.If(wrote):
 499                     for i in range(dut.we_width):
 500                         rd_lane = dut.rd_data_o.word_select(i, gran)
 501                         with m.If(we_mask[i]):
 502                             m.d.sync += Assert(d_reg == rd_lane)
 503             else:
 504                 # with a non-transparent read port, the read value depends
 505                 # on whether there is a simultaneous write, or not
 506                 with m.If((Past(dut.wr_addr_i) == a_const)
 507                           & Past(dut.phase) == dut.write_phase):
 508                     # simultaneous write -> check against last written value
 509                     with m.If(Past(wrote)):
 510                         for i in range(dut.we_width):
 511                             rd_lane = dut.rd_data_o.word_select(i, gran)
 512                             with m.If(we_mask[i]):
 513                                 m.d.sync += Assert(Past(d_reg) == rd_lane)
 514                 with m.Else():
 515                     # otherwise, check against current written value
 516                     with m.If(wrote):
 517                         for i in range(dut.we_width):
 518                             rd_lane = dut.rd_data_o.word_select(i, gran)
 519                             with m.If(we_mask[i]):
 520                                 m.d.sync += Assert(d_reg == rd_lane)
 521
 522         # pass our state to the device under test, so it can ensure that
 523         # its state is in sync with ours, for induction
 524         m.d.comb += [
 525             # address and mask under test
 526             dut.dbg_addr.eq(a_const),
 527             dut.dbg_we_mask.eq(we_mask),
 528             # state of our holding register
 529             dut.dbg_data.eq(d_reg),
 530             dut.dbg_wrote.eq(wrote),
 531         ]
 532
 533         self.assertFormal(m, mode="prove", depth=2)
 534
 535     def test_phased_dual_port_regfile_proof(self):
 536         """test both types (odd and even write ports) of phased write memory"""
 537         with self.subTest("writes happen on phase 0"):
 538             self.do_test_phased_dual_port_regfile_proof(0, False)
 539         with self.subTest("writes happen on phase 1"):
 540             self.do_test_phased_dual_port_regfile_proof(1, False)
 541         # test again, with transparent read ports
 542         with self.subTest("writes happen on phase 0 (transparent reads)"):
 543             self.do_test_phased_dual_port_regfile_proof(0, True)
 544         with self.subTest("writes happen on phase 1 (transparent reads)"):
 545             self.do_test_phased_dual_port_regfile_proof(1, True)
 546
 547
 548 class DualPortRegfile(Elaboratable):
 549     """
 550     Builds, from a pair of phased 1W/1R blocks, a true 1W/1R RAM, where both
 551     read and write ports work every cycle.
 552     It employs a Last Value Table, that tracks to which memory each address was
 553     last written.
 554
 555     :param addr_width: width of the address bus
 556     :param data_width: width of the data bus
 557     :param we_width: number of write enable lines
 558     :param transparent: whether a simultaneous read and write returns the
 559                         new value (True) or the old value (False)
 560     """
 561
 562     def __init__(self, addr_width, data_width, we_width, transparent=True):
 563         self.addr_width = addr_width
 564         self.data_width = data_width
 565         self.we_width = we_width
 566         self.transparent = transparent
 567         self.wr_addr_i = Signal(addr_width); """write port address"""
 568         self.wr_data_i = Signal(data_width); """write port data"""
 569         self.wr_we_i = Signal(we_width); """write port enable"""
 570         self.rd_addr_i = Signal(addr_width); """read port address"""
 571         self.rd_data_o = Signal(data_width); """read port data"""
 572
 573     def elaborate(self, _):
 574         m = Module()
 575         # depth and granularity
 576         depth = 1 << self.addr_width
 577         gran = self.data_width // self.we_width
 578         # instantiate the two phased 1R/1W memory blocks
 579         mem0 = PhasedDualPortRegfile(
 580             self.addr_width, self.data_width, self.we_width, 0,
 581             self.transparent)
 582         mem1 = PhasedDualPortRegfile(
 583             self.addr_width, self.data_width, self.we_width, 1,
 584             self.transparent)
 585         m.submodules.mem0 = mem0
 586         m.submodules.mem1 = mem1
 587         # instantiate the backing memory (FFRAM or LUTRAM)
 588         # for the Last Value Table
 589         # it should have the same number and port types of the desired
 590         # memory, but just one bit per write lane
 591         lvt_mem = Memory(width=self.we_width, depth=depth)
 592         lvt_wr = lvt_mem.write_port(granularity=1)
 593         lvt_rd = lvt_mem.read_port(transparent=self.transparent)
 594         m.submodules.lvt_wr = lvt_wr
 595         m.submodules.lvt_rd = lvt_rd
 596         # generate and wire the phases for the phased memories
 597         phase = Signal()
 598         m.d.sync += phase.eq(~phase)
 599         m.d.comb += [
 600             mem0.phase.eq(phase),
 601             mem1.phase.eq(phase),
 602         ]
 603         m.d.comb += [
 604             # wire the write ports, directly
 605             mem0.wr_addr_i.eq(self.wr_addr_i),
 606             mem1.wr_addr_i.eq(self.wr_addr_i),
 607             mem0.wr_we_i.eq(self.wr_we_i),
 608             mem1.wr_we_i.eq(self.wr_we_i),
 609             mem0.wr_data_i.eq(self.wr_data_i),
 610             mem1.wr_data_i.eq(self.wr_data_i),
 611             # also wire the read addresses
 612             mem0.rd_addr_i.eq(self.rd_addr_i),
 613             mem1.rd_addr_i.eq(self.rd_addr_i),
 614             # wire read and write ports to the LVT
 615             lvt_wr.addr.eq(self.wr_addr_i),
 616             lvt_wr.en.eq(self.wr_we_i),
 617             lvt_rd.addr.eq(self.rd_addr_i),
 618             # the data for the LVT is the phase on which the value was
 619             # written
 620             lvt_wr.data.eq(Repl(phase, self.we_width)),
 621         ]
 622         for i in range(self.we_width):
 623             # select the right memory to assign to the output read port,
 624             # in this byte lane, according to the LVT contents
 625             m.d.comb += self.rd_data_o.word_select(i, gran).eq(
 626                 Mux(
 627                     lvt_rd.data[i],
 628                     mem1.rd_data_o.word_select(i, gran),
 629                     mem0.rd_data_o.word_select(i, gran)))
 630         # TODO create debug port and pass state downstream
 631         m.d.comb += [
 632             mem0.dbg_wrote.eq(0),
 633             mem1.dbg_wrote.eq(0),
 634         ]
 635         return m
 636
 637
 638 class DualPortRegfileTestCase(FHDLTestCase):
 639
 640     def do_test_dual_port_regfile(self, transparent):
 641         """
 642         Simulate some read/write/modify operations on the dual port register
 643         file
 644         """
 645         dut = DualPortRegfile(7, 32, 4, transparent)
 646         sim = Simulator(dut)
 647         sim.add_clock(1e-6)
 648
 649         expected = None
 650         last_expected = None
 651
 652         # compare read data with previously written data
 653         # and start a new read
 654         def read(rd_addr_i, next_expected=None):
 655             nonlocal expected, last_expected
 656             if expected is not None:
 657                 self.assertEqual((yield dut.rd_data_o), expected)
 658             yield dut.rd_addr_i.eq(rd_addr_i)
 659             # account for the read latency
 660             expected = last_expected
 661             last_expected = next_expected
 662
 663         # start a write
 664         def write(wr_addr_i, wr_we_i, wr_data_i):
 665             yield dut.wr_addr_i.eq(wr_addr_i)
 666             yield dut.wr_we_i.eq(wr_we_i)
 667             yield dut.wr_data_i.eq(wr_data_i)
 668
 669         def process():
 670             # write a pair of values, one for each memory
 671             yield from read(0)
 672             yield from write(0x42, 0b1111, 0x87654321)
 673             yield
 674             yield from read(0x42, 0x87654321)
 675             yield from write(0x43, 0b1111, 0x0FEDCBA9)
 676             yield
 677             # skip a beat
 678             yield from read(0x43, 0x0FEDCBA9)
 679             yield from write(0, 0, 0)
 680             yield
 681             # write again, but now they switch memories
 682             yield from read(0)
 683             yield from write(0x42, 0b1111, 0x12345678)
 684             yield
 685             yield from read(0x42, 0x12345678)
 686             yield from write(0x43, 0b1111, 0x9ABCDEF0)
 687             yield
 688             yield from read(0x43, 0x9ABCDEF0)
 689             yield from write(0, 0, 0)
 690             yield
 691             # test partial writes
 692             yield from read(0)
 693             yield from write(0x42, 0b1001, 0x78FFFF12)
 694             yield
 695             yield from read(0)
 696             yield from write(0x43, 0b0110, 0xFFDEABFF)
 697             yield
 698             yield from read(0x42, 0x78345612)
 699             yield from write(0, 0, 0)
 700             yield
 701             yield from read(0x43, 0x9ADEABF0)
 702             yield from write(0, 0, 0)
 703             yield
 704             yield from read(0)
 705             yield from write(0, 0, 0)
 706             yield
 707             if transparent:
 708                 # returns the value just written
 709                 yield from read(0x42, 0x55AA9966)
 710             else:
 711                 # returns the old value
 712                 yield from read(0x42, 0x78345612)
 713             yield from write(0x42, 0b1111, 0x55AA9966)
 714             yield
 715             # after a cycle, always returns the new value
 716             yield from read(0x42, 0x55AA9966)
 717             yield from write(0, 0, 0)
 718             yield
 719             yield from read(0)
 720             yield from write(0, 0, 0)
 721             yield
 722             yield from read(0)
 723             yield from write(0, 0, 0)
 724
 725         sim.add_sync_process(process)
 726         debug_file = 'test_dual_port_regfile'
 727         if transparent:
 728             debug_file += '_transparent'
 729         traces = ['clk', 'phase',
 730                   {'comment': 'write port'},
 731                   'wr_addr_i[6:0]', 'wr_we_i[3:0]', 'wr_data_i[31:0]',
 732                   {'comment': 'read port'},
 733                   'rd_addr_i[6:0]', 'rd_data_o[31:0]',
 734                   {'comment': 'LVT write port'},
 735                   'phase', 'lvt_mem_w_addr[6:0]', 'lvt_mem_w_en[3:0]',
 736                   'lvt_mem_w_data[3:0]',
 737                   {'comment': 'LVT read port'},
 738                   'lvt_mem_r_addr[6:0]', 'lvt_mem_r_data[3:0]',
 739                   {'comment': 'backing memory'},
 740                   'mem0.rd_data_o[31:0]',
 741                   'mem1.rd_data_o[31:0]',
 742                   ]
 743         write_gtkw(debug_file + '.gtkw',
 744                    debug_file + '.vcd',
 745                    traces, module='top', zoom=-22)
 746         sim_writer = sim.write_vcd(debug_file + '.vcd')
 747         with sim_writer:
 748             sim.run()
 749
 750     def test_dual_port_regfile(self):
 751         with self.subTest("non-transparent reads"):
 752             self.do_test_dual_port_regfile(False)
 753         with self.subTest("transparent reads"):
 754             self.do_test_dual_port_regfile(True)
 755
 756     def test_dual_port_regfile_proof(self):
 757         """
 758         Formal proof of the 1W/1R regfile
 759         """
 760         m = Module()
 761         # 128 x 32-bit, 8-bit granularity
 762         dut = DualPortRegfile(7, 32, 4, True)
 763         m.submodules.dut = dut
 764         gran = dut.data_width // dut.we_width  # granularity
 765         # choose a single random memory location to test
 766         a_const = AnyConst(dut.addr_width)
 767         # choose a single byte lane to test (one-hot encoding)
 768         we_mask = Signal(dut.we_width)
 769         # ... by first creating a random bit pattern
 770         we_const = AnyConst(dut.we_width)
 771         # ... and zeroing all but the first non-zero bit
 772         m.d.comb += we_mask.eq(we_const & (-we_const))
 773         # holding data register
 774         d_reg = Signal(gran)
 775         # for some reason, simulated formal memory is not zeroed at reset
 776         # ... so, remember whether we wrote it, at least once.
 777         wrote = Signal()
 778         # if our memory location and byte lane is being written,
 779         # capture the data in our holding register
 780         with m.If((dut.wr_addr_i == a_const)):
 781             for i in range(dut.we_width):
 782                 with m.If(we_mask[i] & dut.wr_we_i[i]):
 783                     m.d.sync += d_reg.eq(
 784                         dut.wr_data_i[i * gran:i * gran + gran])
 785                     m.d.sync += wrote.eq(1)
 786         # if our memory location is being read,
 787         # and the holding register has valid data,
 788         # then its value must match the memory output, on the given lane
 789         with m.If(Past(dut.rd_addr_i) == a_const):
 790             with m.If(wrote):
 791                 for i in range(dut.we_width):
 792                     rd_lane = dut.rd_data_o.word_select(i, gran)
 793                     with m.If(we_mask[i]):
 794                         m.d.sync += Assert(d_reg == rd_lane)
 795
 796         self.assertFormal(m, mode="bmc", depth=10)
 797
 798
 799 if __name__ == "__main__":
 800     unittest.main()