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         if not self.transparent:
 603             # for some reason, formal proofs don't recognize the default
 604             # reset value for this signal
 605             m.d.comb += lvt_rd.en.eq(1)
 606         m.submodules.lvt_wr = lvt_wr
 607         m.submodules.lvt_rd = lvt_rd
 608         # generate and wire the phases for the phased memories
 609         phase = Signal()
 610         m.d.sync += phase.eq(~phase)
 611         m.d.comb += [
 612             mem0.phase.eq(phase),
 613             mem1.phase.eq(phase),
 614         ]
 615         m.d.comb += [
 616             # wire the write ports, directly
 617             mem0.wr_addr_i.eq(self.wr_addr_i),
 618             mem1.wr_addr_i.eq(self.wr_addr_i),
 619             mem0.wr_we_i.eq(self.wr_we_i),
 620             mem1.wr_we_i.eq(self.wr_we_i),
 621             mem0.wr_data_i.eq(self.wr_data_i),
 622             mem1.wr_data_i.eq(self.wr_data_i),
 623             # also wire the read addresses
 624             mem0.rd_addr_i.eq(self.rd_addr_i),
 625             mem1.rd_addr_i.eq(self.rd_addr_i),
 626             # wire read and write ports to the LVT
 627             lvt_wr.addr.eq(self.wr_addr_i),
 628             lvt_wr.en.eq(self.wr_we_i),
 629             lvt_rd.addr.eq(self.rd_addr_i),
 630             # the data for the LVT is the phase on which the value was
 631             # written
 632             lvt_wr.data.eq(Repl(phase, self.we_width)),
 633         ]
 634         for i in range(self.we_width):
 635             # select the right memory to assign to the output read port,
 636             # in this byte lane, according to the LVT contents
 637             m.d.comb += self.rd_data_o.word_select(i, gran).eq(
 638                 Mux(
 639                     lvt_rd.data[i],
 640                     mem1.rd_data_o.word_select(i, gran),
 641                     mem0.rd_data_o.word_select(i, gran)))
 642
 643         if platform == "formal":
 644             # pass upstream state to the memories, so they can ensure that
 645             # their state are in sync with upstream, for induction
 646             m.d.comb += [
 647                 # address and write lane under test
 648                 mem0.dbg_addr.eq(self.dbg_addr),
 649                 mem1.dbg_addr.eq(self.dbg_addr),
 650                 mem0.dbg_lane.eq(self.dbg_lane),
 651                 mem1.dbg_lane.eq(self.dbg_lane),
 652                 # upstream state
 653                 mem0.dbg_data.eq(self.dbg_data),
 654                 mem1.dbg_data.eq(self.dbg_data),
 655                 # the memory, on which the write ends up, depends on which
 656                 # phase it was written
 657                 mem0.dbg_wrote.eq(self.dbg_wrote & ~self.dbg_wrote_phase),
 658                 mem1.dbg_wrote.eq(self.dbg_wrote & self.dbg_wrote_phase),
 659             ]
 660             # sync phase to upstream
 661             m.d.comb += Assert(self.dbg_phase == phase)
 662             # this debug port for the LVT is an asynchronous read port,
 663             # allowing direct access to a given memory location
 664             # by the formal engine
 665             m.submodules.dbgport = dbgport = lvt_mem.read_port(domain='comb')
 666             # first, get the value stored in our memory location,
 667             stored = Signal(self.we_width)
 668             m.d.comb += dbgport.addr.eq(self.dbg_addr)
 669             m.d.comb += stored.eq(dbgport.data)
 670             # now, ensure that the value stored in memory is always in sync
 671             # with the expected value (which memory the value was written to)
 672             with m.If(self.dbg_wrote):
 673                 m.d.comb += Assert(stored.bit_select(self.dbg_lane, 1)
 674                                    == self.dbg_wrote_phase)
 675         return m
 676
 677     def ports(self):
 678         return [
 679             self.wr_addr_i,
 680             self.wr_data_i,
 681             self.wr_we_i,
 682             self.rd_addr_i,
 683             self.rd_data_o
 684         ]
 685
 686
 687 class DualPortRegfileTestCase(FHDLTestCase):
 688
 689     def do_test_dual_port_regfile(self, transparent):
 690         """
 691         Simulate some read/write/modify operations on the dual port register
 692         file
 693         """
 694         dut = DualPortRegfile(7, 32, 4, transparent)
 695         sim = Simulator(dut)
 696         sim.add_clock(1e-6)
 697
 698         expected = None
 699         last_expected = None
 700
 701         # compare read data with previously written data
 702         # and start a new read
 703         def read(rd_addr_i, next_expected=None):
 704             nonlocal expected, last_expected
 705             if expected is not None:
 706                 self.assertEqual((yield dut.rd_data_o), expected)
 707             yield dut.rd_addr_i.eq(rd_addr_i)
 708             # account for the read latency
 709             expected = last_expected
 710             last_expected = next_expected
 711
 712         # start a write
 713         def write(wr_addr_i, wr_we_i, wr_data_i):
 714             yield dut.wr_addr_i.eq(wr_addr_i)
 715             yield dut.wr_we_i.eq(wr_we_i)
 716             yield dut.wr_data_i.eq(wr_data_i)
 717
 718         def process():
 719             # write a pair of values, one for each memory
 720             yield from read(0)
 721             yield from write(0x42, 0b1111, 0x87654321)
 722             yield
 723             yield from read(0x42, 0x87654321)
 724             yield from write(0x43, 0b1111, 0x0FEDCBA9)
 725             yield
 726             # skip a beat
 727             yield from read(0x43, 0x0FEDCBA9)
 728             yield from write(0, 0, 0)
 729             yield
 730             # write again, but now they switch memories
 731             yield from read(0)
 732             yield from write(0x42, 0b1111, 0x12345678)
 733             yield
 734             yield from read(0x42, 0x12345678)
 735             yield from write(0x43, 0b1111, 0x9ABCDEF0)
 736             yield
 737             yield from read(0x43, 0x9ABCDEF0)
 738             yield from write(0, 0, 0)
 739             yield
 740             # test partial writes
 741             yield from read(0)
 742             yield from write(0x42, 0b1001, 0x78FFFF12)
 743             yield
 744             yield from read(0)
 745             yield from write(0x43, 0b0110, 0xFFDEABFF)
 746             yield
 747             yield from read(0x42, 0x78345612)
 748             yield from write(0, 0, 0)
 749             yield
 750             yield from read(0x43, 0x9ADEABF0)
 751             yield from write(0, 0, 0)
 752             yield
 753             yield from read(0)
 754             yield from write(0, 0, 0)
 755             yield
 756             if transparent:
 757                 # returns the value just written
 758                 yield from read(0x42, 0x55AA9966)
 759             else:
 760                 # returns the old value
 761                 yield from read(0x42, 0x78345612)
 762             yield from write(0x42, 0b1111, 0x55AA9966)
 763             yield
 764             # after a cycle, always returns the new value
 765             yield from read(0x42, 0x55AA9966)
 766             yield from write(0, 0, 0)
 767             yield
 768             yield from read(0)
 769             yield from write(0, 0, 0)
 770             yield
 771             yield from read(0)
 772             yield from write(0, 0, 0)
 773
 774         sim.add_sync_process(process)
 775         debug_file = 'test_dual_port_regfile'
 776         if transparent:
 777             debug_file += '_transparent'
 778         traces = ['clk', 'phase',
 779                   {'comment': 'write port'},
 780                   'wr_addr_i[6:0]', 'wr_we_i[3:0]', 'wr_data_i[31:0]',
 781                   {'comment': 'read port'},
 782                   'rd_addr_i[6:0]', 'rd_data_o[31:0]',
 783                   {'comment': 'LVT write port'},
 784                   'phase', 'lvt_mem_w_addr[6:0]', 'lvt_mem_w_en[3:0]',
 785                   'lvt_mem_w_data[3:0]',
 786                   {'comment': 'LVT read port'},
 787                   'lvt_mem_r_addr[6:0]', 'lvt_mem_r_data[3:0]',
 788                   {'comment': 'backing memory'},
 789                   'mem0.rd_data_o[31:0]',
 790                   'mem1.rd_data_o[31:0]',
 791                   ]
 792         write_gtkw(debug_file + '.gtkw',
 793                    debug_file + '.vcd',
 794                    traces, module='top', zoom=-22)
 795         sim_writer = sim.write_vcd(debug_file + '.vcd')
 796         with sim_writer:
 797             sim.run()
 798
 799     def test_dual_port_regfile(self):
 800         with self.subTest("non-transparent reads"):
 801             self.do_test_dual_port_regfile(False)
 802         with self.subTest("transparent reads"):
 803             self.do_test_dual_port_regfile(True)
 804
 805     def do_test_dual_port_regfile_proof(self, transparent=True):
 806         """
 807         Formal proof of the 1W/1R regfile
 808         """
 809         m = Module()
 810         # 128 x 32-bit, 8-bit granularity
 811         dut = DualPortRegfile(7, 32, 4, transparent)
 812         m.submodules.dut = dut
 813         gran = dut.data_width // dut.we_width  # granularity
 814         # choose a single random memory location to test
 815         a_const = AnyConst(dut.addr_width)
 816         # choose a single byte lane to test
 817         lane = AnyConst(range(dut.we_width))
 818         # holding data register
 819         d_reg = Signal(gran)
 820         # keep track of the phase, so we can remember which memory
 821         # we wrote to
 822         phase = Signal()
 823         m.d.sync += phase.eq(~phase)
 824         # for some reason, simulated formal memory is not zeroed at reset
 825         # ... so, remember whether we wrote it, at least once.
 826         wrote = Signal()
 827         # ... and on which phase it was written
 828         wrote_phase = Signal()
 829         # if our memory location and byte lane is being written,
 830         # capture the data in our holding register
 831         with m.If((dut.wr_addr_i == a_const)
 832                   & dut.wr_we_i.bit_select(lane, 1)):
 833             m.d.sync += d_reg.eq(dut.wr_data_i.word_select(lane, gran))
 834             m.d.sync += wrote.eq(1)
 835             m.d.sync += wrote_phase.eq(phase)
 836         # if our memory location is being read,
 837         # and the holding register has valid data,
 838         # then its value must match the memory output, on the given lane
 839         with m.If(Past(dut.rd_addr_i) == a_const):
 840             if transparent:
 841                 with m.If(wrote):
 842                     rd_lane = dut.rd_data_o.word_select(lane, gran)
 843                     m.d.sync += Assert(d_reg == rd_lane)
 844             else:
 845                 # with a non-transparent read port, the read value depends
 846                 # on whether there is a simultaneous write, or not
 847                 with m.If(Past(dut.wr_addr_i) == a_const):
 848                     # simultaneous write -> check against last written value
 849                     with m.If(wrote & Past(wrote)):
 850                         rd_lane = dut.rd_data_o.word_select(lane, gran)
 851                         m.d.sync += Assert(Past(d_reg) == rd_lane)
 852                 with m.Else():
 853                     # otherwise, check against current written value
 854                     with m.If(wrote):
 855                         rd_lane = dut.rd_data_o.word_select(lane, gran)
 856                         m.d.sync += Assert(d_reg == rd_lane)
 857
 858         m.d.comb += [
 859             dut.dbg_addr.eq(a_const),
 860             dut.dbg_lane.eq(lane),
 861             dut.dbg_data.eq(d_reg),
 862             dut.dbg_wrote.eq(wrote),
 863             dut.dbg_wrote_phase.eq(wrote_phase),
 864             dut.dbg_phase.eq(phase),
 865         ]
 866
 867         self.assertFormal(m, mode="prove", depth=3)
 868
 869     def test_dual_port_regfile_proof(self):
 870         """
 871         Formal check of 1W/1R regfile (transparent and not)
 872         """
 873         with self.subTest("transparent reads"):
 874             self.do_test_dual_port_regfile_proof(True)
 875         with self.subTest("non-transparent reads"):
 876             self.do_test_dual_port_regfile_proof(False)
 877
 878
 879 class PhasedReadPhasedWriteFullReadSRAM(Elaboratable):
 880     """
 881     Builds, from three 1RW blocks, a pseudo 1W/2R SRAM, with:
 882
 883     * one full read port, which works every cycle,
 884     * one write port, which is only available on either even or odd cycles,
 885     * an extra transparent read port, available only on the same cycles as the
 886       write port
 887
 888     This type of SRAM is useful for a XOR-based 6x1RW implementation of
 889     a 1R/1W register file.
 890
 891     :param addr_width: width of the address bus
 892     :param data_width: width of the data bus
 893     :param we_width: number of write enable lines
 894     :param write_phase: indicates on which phase the write port will
 895                         accept data
 896     :param transparent: whether a simultaneous read and write returns the
 897                         new value (True) or the old value (False) on the full
 898                         read port
 899     """
 900
 901     def __init__(self, addr_width, data_width, we_width, write_phase,
 902                  transparent=True):
 903         self.addr_width = addr_width
 904         self.data_width = data_width
 905         self.we_width = we_width
 906         self.write_phase = write_phase
 907         self.transparent = transparent
 908         # interface signals
 909         self.wr_addr_i = Signal(addr_width); """phased write port address"""
 910         self.wr_data_i = Signal(data_width); """phased write port data"""
 911         self.wr_we_i = Signal(we_width); """phased write port enable"""
 912         self.rd_addr_i = Signal(addr_width); """full read port address"""
 913         self.rd_data_o = Signal(data_width); """full read port data"""
 914         self.rdp_addr_i = Signal(addr_width); """phased read port address"""
 915         self.rdp_data_o = Signal(data_width); """phased read port data"""
 916         self.phase = Signal(); """even/odd cycle indicator"""
 917
 918     def elaborate(self, platform):
 919         m = Module()
 920         # instantiate the 1RW memory blocks
 921         mem1 = SinglePortSRAM(self.addr_width, self.data_width, self.we_width)
 922         mem2 = SinglePortSRAM(self.addr_width, self.data_width, self.we_width)
 923         mem3 = SinglePortSRAM(self.addr_width, self.data_width, self.we_width)
 924         m.submodules.mem1 = mem1
 925         m.submodules.mem2 = mem2
 926         m.submodules.mem3 = mem3
 927         # wire input write data to first memory, and its output to the others
 928         m.d.comb += [
 929             mem1.d.eq(self.wr_data_i),
 930             mem2.d.eq(mem1.q),
 931             mem3.d.eq(mem1.q)
 932         ]
 933         # holding registers for the write port of the other memories
 934         last_wr_addr = Signal(self.addr_width)
 935         last_wr_we = Signal(self.we_width)
 936         # do read and write addresses coincide?
 937         same_read_write = Signal()
 938         same_phased_read_write = Signal()
 939         with m.If(self.phase == self.write_phase):
 940             # write phase, start a write on the first memory
 941             m.d.comb += mem1.a.eq(self.wr_addr_i)
 942             m.d.comb += mem1.we.eq(self.wr_we_i)
 943             # save write address and write select for repeating the write
 944             # on the other memories, one cycle later
 945             m.d.sync += last_wr_we.eq(self.wr_we_i)
 946             m.d.sync += last_wr_addr.eq(self.wr_addr_i)
 947             # start a read on the other memories
 948             m.d.comb += mem2.a.eq(self.rd_addr_i)
 949             m.d.comb += mem3.a.eq(self.rdp_addr_i)
 950             # output previously read data from the first memory
 951             m.d.comb += self.rd_data_o.eq(mem1.q)
 952             # remember whether we are reading from the same location as we
 953             # are writing
 954             m.d.sync += same_phased_read_write.eq(
 955                 self.rdp_addr_i == self.wr_addr_i)
 956             if self.transparent:
 957                 m.d.sync += same_read_write.eq(self.rd_addr_i == self.wr_addr_i)
 958         with m.Else():
 959             # read phase, write last written data on the other memories
 960             m.d.comb += [
 961                 mem2.a.eq(last_wr_addr),
 962                 mem2.we.eq(last_wr_we),
 963                 mem3.a.eq(last_wr_addr),
 964                 mem3.we.eq(last_wr_we),
 965             ]
 966             # start a read on the first memory
 967             m.d.comb += mem1.a.eq(self.rd_addr_i)
 968             # output the read data from the second memory
 969             if self.transparent:
 970                 with m.If(same_read_write):
 971                     # when transparent, and read and write addresses coincide,
 972                     # output the data just written
 973                     m.d.comb += self.rd_data_o.eq(mem1.q)
 974                 with m.Else():
 975                     # otherwise, output previously read data
 976                     # from the second memory
 977                     m.d.comb += self.rd_data_o.eq(mem2.q)
 978             else:
 979                 # always output the read data from the second memory,
 980                 # if not transparent
 981                 m.d.comb += self.rd_data_o.eq(mem2.q)
 982             with m.If(same_phased_read_write):
 983                 # if read and write addresses coincide,
 984                 # output the data just written
 985                 m.d.comb += self.rdp_data_o.eq(mem1.q)
 986             with m.Else():
 987                 # otherwise, output previously read data
 988                 # from the third memory
 989                 m.d.comb += self.rdp_data_o.eq(mem3.q)
 990
 991         return m
 992
 993
 994 class PhasedReadPhasedWriteFullReadSRAMTestCase(FHDLTestCase):
 995
 996     def do_test_case(self, write_phase, transparent):
 997         """
 998         Simulate some read/write/modify operations
 999         """
1000         dut = PhasedReadPhasedWriteFullReadSRAM(7, 32, 4, write_phase,
1001                                                 transparent)
1002         sim = Simulator(dut)
1003         sim.add_clock(1e-6)
1004
1005         expected = None
1006         last_expected = None
1007
1008         # compare read data with previously written data
1009         # and start a new read
1010         def read(rd_addr_i, next_expected=None):
1011             nonlocal expected, last_expected
1012             if expected is not None:
1013                 self.assertEqual((yield dut.rd_data_o), expected)
1014             yield dut.rd_addr_i.eq(rd_addr_i)
1015             # account for the read latency
1016             expected = last_expected
1017             last_expected = next_expected
1018
1019         expected2 = None
1020
1021         # same as above, but for the phased read port
1022         def phased_read(rdp_addr_i, next_expected2=None):
1023             nonlocal expected2
1024             if expected2 is not None:
1025                 self.assertEqual((yield dut.rdp_data_o), expected2)
1026             yield dut.rdp_addr_i.eq(rdp_addr_i)
1027             # account for the read latency
1028             expected2 = next_expected2
1029
1030         # start a write
1031         def write(wr_addr_i, wr_we_i, wr_data_i):
1032             yield dut.wr_addr_i.eq(wr_addr_i)
1033             yield dut.wr_we_i.eq(wr_we_i)
1034             yield dut.wr_data_i.eq(wr_data_i)
1035             yield dut.phase.eq(write_phase)
1036
1037         # disable writes, and start read phase
1038         def skip_write():
1039             yield dut.wr_addr_i.eq(0)
1040             yield dut.wr_we_i.eq(0)
1041             yield dut.wr_data_i.eq(0)
1042             yield dut.phase.eq(~write_phase)
1043             # also skip reading from the phased read port
1044             yield dut.rdp_addr_i.eq(0)
1045
1046         # writes a few values on the write port, and read them back
1047         def process():
1048             yield from read(0)
1049             yield from phased_read(0)
1050             yield from write(0x42, 0b1111, 0x12345678)
1051             yield
1052             yield from read(0x42, 0x12345678)
1053             yield from skip_write()
1054             yield
1055             yield from read(0x42, 0x12345678)
1056             yield from phased_read(0x42, 0x12345678)
1057             yield from write(0x43, 0b1111, 0x9ABCDEF0)
1058             yield
1059             yield from read(0x43, 0x9ABCDEF0)
1060             yield from skip_write()
1061             yield
1062             yield from read(0x42, 0x12345678)
1063             yield from phased_read(0x42, 0x12345678)
1064             yield from write(0x43, 0b1001, 0xF0FFFF9A)
1065             yield
1066             yield from read(0x43, 0xF0BCDE9A)
1067             yield from skip_write()
1068             yield
1069             yield from read(0x43, 0xF0BCDE9A)
1070             yield from phased_read(0x43, 0xF0BCDE9A)
1071             yield from write(0x42, 0b0110, 0xFF5634FF)
1072             yield
1073             yield from read(0x42, 0x12563478)
1074             yield from skip_write()
1075             yield
1076             yield from read(0)
1077             yield from phased_read(0)
1078             yield from write(0, 0, 0)
1079             yield
1080             yield from read(0)
1081             yield from skip_write()
1082             yield
1083             # try reading and writing at the same time
1084             if transparent:
1085                 # transparent port, return the value just written
1086                 yield from read(0x42, 0x55AA9966)
1087             else:
1088                 # ... otherwise, return the old value
1089                 yield from read(0x42, 0x12563478)
1090             # transparent port, always return the value just written
1091             yield from phased_read(0x42, 0x55AA9966)
1092             yield from write(0x42, 0b1111, 0x55AA9966)
1093             yield
1094             # after a cycle, always returns the new value
1095             yield from read(0x42, 0x55AA9966)
1096             yield from skip_write()
1097             yield
1098             yield from read(0)
1099             yield from phased_read(0)
1100             yield from write(0, 0, 0)
1101             yield
1102             yield from read(0)
1103             yield from skip_write()
1104
1105         sim.add_sync_process(process)
1106         debug_file = 'test_phased_read_write_sram_' + str(write_phase)
1107         if transparent:
1108             debug_file += '_transparent'
1109         traces = ['clk', 'phase',
1110                   {'comment': 'phased write port'},
1111                   'wr_addr_i[6:0]', 'wr_we_i[3:0]', 'wr_data_i[31:0]',
1112                   {'comment': 'full read port'},
1113                   'rd_addr_i[6:0]', 'rd_data_o[31:0]',
1114                   {'comment': 'phased read port'},
1115                   'rdp_addr_i[6:0]', 'rdp_data_o[31:0]']
1116         write_gtkw(debug_file + '.gtkw',
1117                    debug_file + '.vcd',
1118                    traces, module='top', zoom=-22)
1119         sim_writer = sim.write_vcd(debug_file + '.vcd')
1120         with sim_writer:
1121             sim.run()
1122
1123     def test_case(self):
1124         """test both types (odd and even write ports) of phased memory"""
1125         with self.subTest("writes happen on phase 0"):
1126             self.do_test_case(0, True)
1127         with self.subTest("writes happen on phase 1"):
1128             self.do_test_case(1, True)
1129         with self.subTest("writes happen on phase 0 (non-transparent reads)"):
1130             self.do_test_case(0, False)
1131         with self.subTest("writes happen on phase 1 (non-transparent reads)"):
1132             self.do_test_case(1, False)
1133
1134
1135 if __name__ == "__main__":
1136     unittest.main()