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         # interface signals
 574         self.wr_addr_i = Signal(addr_width); """write port address"""
 575         self.wr_data_i = Signal(data_width); """write port data"""
 576         self.wr_we_i = Signal(we_width); """write port enable"""
 577         self.rd_addr_i = Signal(addr_width); """read port address"""
 578         self.rd_data_o = Signal(data_width); """read port data"""
 579         # debug signals, only used in formal proofs
 580         # address and write lane under test
 581         self.dbg_addr = Signal(addr_width); """debug: address under test"""
 582         self.dbg_we_mask = Signal(we_width); """debug: write lane under test"""
 583         # upstream state, to keep in sync with ours
 584         gran = self.data_width // self.we_width
 585         self.dbg_data = Signal(gran); """debug: data to keep in sync"""
 586         self.dbg_wrote = Signal(); """debug: data is valid"""
 587         self.dbg_wrote_phase = Signal(); """debug: the phase data was written"""
 588         self.dbg_phase = Signal(); """debug: current phase"""
 589
 590     def elaborate(self, platform):
 591         m = Module()
 592         # depth and granularity
 593         depth = 1 << self.addr_width
 594         gran = self.data_width // self.we_width
 595         # instantiate the two phased 1R/1W memory blocks
 596         mem0 = PhasedDualPortRegfile(
 597             self.addr_width, self.data_width, self.we_width, 0,
 598             self.transparent)
 599         mem1 = PhasedDualPortRegfile(
 600             self.addr_width, self.data_width, self.we_width, 1,
 601             self.transparent)
 602         m.submodules.mem0 = mem0
 603         m.submodules.mem1 = mem1
 604         # instantiate the backing memory (FFRAM or LUTRAM)
 605         # for the Last Value Table
 606         # it should have the same number and port types of the desired
 607         # memory, but just one bit per write lane
 608         lvt_mem = Memory(width=self.we_width, depth=depth)
 609         lvt_wr = lvt_mem.write_port(granularity=1)
 610         lvt_rd = lvt_mem.read_port(transparent=self.transparent)
 611         m.submodules.lvt_wr = lvt_wr
 612         m.submodules.lvt_rd = lvt_rd
 613         # generate and wire the phases for the phased memories
 614         phase = Signal()
 615         m.d.sync += phase.eq(~phase)
 616         m.d.comb += [
 617             mem0.phase.eq(phase),
 618             mem1.phase.eq(phase),
 619         ]
 620         m.d.comb += [
 621             # wire the write ports, directly
 622             mem0.wr_addr_i.eq(self.wr_addr_i),
 623             mem1.wr_addr_i.eq(self.wr_addr_i),
 624             mem0.wr_we_i.eq(self.wr_we_i),
 625             mem1.wr_we_i.eq(self.wr_we_i),
 626             mem0.wr_data_i.eq(self.wr_data_i),
 627             mem1.wr_data_i.eq(self.wr_data_i),
 628             # also wire the read addresses
 629             mem0.rd_addr_i.eq(self.rd_addr_i),
 630             mem1.rd_addr_i.eq(self.rd_addr_i),
 631             # wire read and write ports to the LVT
 632             lvt_wr.addr.eq(self.wr_addr_i),
 633             lvt_wr.en.eq(self.wr_we_i),
 634             lvt_rd.addr.eq(self.rd_addr_i),
 635             # the data for the LVT is the phase on which the value was
 636             # written
 637             lvt_wr.data.eq(Repl(phase, self.we_width)),
 638         ]
 639         for i in range(self.we_width):
 640             # select the right memory to assign to the output read port,
 641             # in this byte lane, according to the LVT contents
 642             m.d.comb += self.rd_data_o.word_select(i, gran).eq(
 643                 Mux(
 644                     lvt_rd.data[i],
 645                     mem1.rd_data_o.word_select(i, gran),
 646                     mem0.rd_data_o.word_select(i, gran)))
 647
 648         if platform == "formal":
 649             # pass upstream state to the memories, so they can ensure that
 650             # their state are in sync with upstream, for induction
 651             m.d.comb += [
 652                 # address and write lane under test
 653                 mem0.dbg_addr.eq(self.dbg_addr),
 654                 mem1.dbg_addr.eq(self.dbg_addr),
 655                 mem0.dbg_we_mask.eq(self.dbg_we_mask),
 656                 mem1.dbg_we_mask.eq(self.dbg_we_mask),
 657                 # upstream state
 658                 mem0.dbg_data.eq(self.dbg_data),
 659                 mem1.dbg_data.eq(self.dbg_data),
 660                 # the memory, on which the write ends up, depends on which
 661                 # phase it was written
 662                 mem0.dbg_wrote.eq(self.dbg_wrote & ~self.dbg_wrote_phase),
 663                 mem1.dbg_wrote.eq(self.dbg_wrote & self.dbg_wrote_phase),
 664             ]
 665             # sync phase to upstream
 666             m.d.comb += Assert(self.dbg_phase == phase)
 667             # this debug port for the LVT is an asynchronous read port,
 668             # allowing direct access to a given memory location
 669             # by the formal engine
 670             m.submodules.dbgport = dbgport = lvt_mem.read_port(domain='comb')
 671             # first, get the value stored in our memory location,
 672             stored = Signal(self.we_width)
 673             m.d.comb += dbgport.addr.eq(self.dbg_addr)
 674             m.d.comb += stored.eq(dbgport.data)
 675             # now, ensure that the value stored in memory is always in sync
 676             # with the expected value (which memory the value was written to)
 677             with m.If(self.dbg_wrote):
 678                 for i in range(self.we_width):
 679                     with m.If(self.dbg_we_mask[i]):
 680                         m.d.comb += Assert(stored[i] == self.dbg_wrote_phase)
 681         return m
 682
 683
 684 class DualPortRegfileTestCase(FHDLTestCase):
 685
 686     def do_test_dual_port_regfile(self, transparent):
 687         """
 688         Simulate some read/write/modify operations on the dual port register
 689         file
 690         """
 691         dut = DualPortRegfile(7, 32, 4, transparent)
 692         sim = Simulator(dut)
 693         sim.add_clock(1e-6)
 694
 695         expected = None
 696         last_expected = None
 697
 698         # compare read data with previously written data
 699         # and start a new read
 700         def read(rd_addr_i, next_expected=None):
 701             nonlocal expected, last_expected
 702             if expected is not None:
 703                 self.assertEqual((yield dut.rd_data_o), expected)
 704             yield dut.rd_addr_i.eq(rd_addr_i)
 705             # account for the read latency
 706             expected = last_expected
 707             last_expected = next_expected
 708
 709         # start a write
 710         def write(wr_addr_i, wr_we_i, wr_data_i):
 711             yield dut.wr_addr_i.eq(wr_addr_i)
 712             yield dut.wr_we_i.eq(wr_we_i)
 713             yield dut.wr_data_i.eq(wr_data_i)
 714
 715         def process():
 716             # write a pair of values, one for each memory
 717             yield from read(0)
 718             yield from write(0x42, 0b1111, 0x87654321)
 719             yield
 720             yield from read(0x42, 0x87654321)
 721             yield from write(0x43, 0b1111, 0x0FEDCBA9)
 722             yield
 723             # skip a beat
 724             yield from read(0x43, 0x0FEDCBA9)
 725             yield from write(0, 0, 0)
 726             yield
 727             # write again, but now they switch memories
 728             yield from read(0)
 729             yield from write(0x42, 0b1111, 0x12345678)
 730             yield
 731             yield from read(0x42, 0x12345678)
 732             yield from write(0x43, 0b1111, 0x9ABCDEF0)
 733             yield
 734             yield from read(0x43, 0x9ABCDEF0)
 735             yield from write(0, 0, 0)
 736             yield
 737             # test partial writes
 738             yield from read(0)
 739             yield from write(0x42, 0b1001, 0x78FFFF12)
 740             yield
 741             yield from read(0)
 742             yield from write(0x43, 0b0110, 0xFFDEABFF)
 743             yield
 744             yield from read(0x42, 0x78345612)
 745             yield from write(0, 0, 0)
 746             yield
 747             yield from read(0x43, 0x9ADEABF0)
 748             yield from write(0, 0, 0)
 749             yield
 750             yield from read(0)
 751             yield from write(0, 0, 0)
 752             yield
 753             if transparent:
 754                 # returns the value just written
 755                 yield from read(0x42, 0x55AA9966)
 756             else:
 757                 # returns the old value
 758                 yield from read(0x42, 0x78345612)
 759             yield from write(0x42, 0b1111, 0x55AA9966)
 760             yield
 761             # after a cycle, always returns the new value
 762             yield from read(0x42, 0x55AA9966)
 763             yield from write(0, 0, 0)
 764             yield
 765             yield from read(0)
 766             yield from write(0, 0, 0)
 767             yield
 768             yield from read(0)
 769             yield from write(0, 0, 0)
 770
 771         sim.add_sync_process(process)
 772         debug_file = 'test_dual_port_regfile'
 773         if transparent:
 774             debug_file += '_transparent'
 775         traces = ['clk', 'phase',
 776                   {'comment': 'write port'},
 777                   'wr_addr_i[6:0]', 'wr_we_i[3:0]', 'wr_data_i[31:0]',
 778                   {'comment': 'read port'},
 779                   'rd_addr_i[6:0]', 'rd_data_o[31:0]',
 780                   {'comment': 'LVT write port'},
 781                   'phase', 'lvt_mem_w_addr[6:0]', 'lvt_mem_w_en[3:0]',
 782                   'lvt_mem_w_data[3:0]',
 783                   {'comment': 'LVT read port'},
 784                   'lvt_mem_r_addr[6:0]', 'lvt_mem_r_data[3:0]',
 785                   {'comment': 'backing memory'},
 786                   'mem0.rd_data_o[31:0]',
 787                   'mem1.rd_data_o[31:0]',
 788                   ]
 789         write_gtkw(debug_file + '.gtkw',
 790                    debug_file + '.vcd',
 791                    traces, module='top', zoom=-22)
 792         sim_writer = sim.write_vcd(debug_file + '.vcd')
 793         with sim_writer:
 794             sim.run()
 795
 796     def test_dual_port_regfile(self):
 797         with self.subTest("non-transparent reads"):
 798             self.do_test_dual_port_regfile(False)
 799         with self.subTest("transparent reads"):
 800             self.do_test_dual_port_regfile(True)
 801
 802     def test_dual_port_regfile_proof(self):
 803         """
 804         Formal proof of the 1W/1R regfile
 805         """
 806         m = Module()
 807         # 128 x 32-bit, 8-bit granularity
 808         dut = DualPortRegfile(7, 32, 4, True)
 809         m.submodules.dut = dut
 810         gran = dut.data_width // dut.we_width  # granularity
 811         # choose a single random memory location to test
 812         a_const = AnyConst(dut.addr_width)
 813         # choose a single byte lane to test (one-hot encoding)
 814         we_mask = Signal(dut.we_width)
 815         # ... by first creating a random bit pattern
 816         we_const = AnyConst(dut.we_width)
 817         # ... and zeroing all but the first non-zero bit
 818         m.d.comb += we_mask.eq(we_const & (-we_const))
 819         # holding data register
 820         d_reg = Signal(gran)
 821         # keep track of the phase, so we can remember which memory
 822         # we wrote to
 823         phase = Signal()
 824         m.d.sync += phase.eq(~phase)
 825         # for some reason, simulated formal memory is not zeroed at reset
 826         # ... so, remember whether we wrote it, at least once.
 827         wrote = Signal()
 828         # ... and on which phase it was written
 829         wrote_phase = Signal()
 830         # if our memory location and byte lane is being written,
 831         # capture the data in our holding register
 832         with m.If((dut.wr_addr_i == a_const)):
 833             for i in range(dut.we_width):
 834                 with m.If(we_mask[i] & dut.wr_we_i[i]):
 835                     m.d.sync += d_reg.eq(dut.wr_data_i.word_select(i, gran))
 836                     m.d.sync += wrote.eq(1)
 837                     m.d.sync += wrote_phase.eq(phase)
 838         # if our memory location is being read,
 839         # and the holding register has valid data,
 840         # then its value must match the memory output, on the given lane
 841         with m.If(Past(dut.rd_addr_i) == a_const):
 842             with m.If(wrote):
 843                 for i in range(dut.we_width):
 844                     rd_lane = dut.rd_data_o.word_select(i, gran)
 845                     with m.If(we_mask[i]):
 846                         m.d.sync += Assert(d_reg == rd_lane)
 847
 848         m.d.comb += [
 849             dut.dbg_addr.eq(a_const),
 850             dut.dbg_we_mask.eq(we_mask),
 851             dut.dbg_data.eq(d_reg),
 852             dut.dbg_wrote.eq(wrote),
 853             dut.dbg_wrote_phase.eq(wrote_phase),
 854             dut.dbg_phase.eq(phase),
 855         ]
 856
 857         self.assertFormal(m, mode="prove", depth=3)
 858
 859
 860 if __name__ == "__main__":
 861     unittest.main()