src/soc/regfile/sram_wrapper.py

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