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
  20 from nmigen.back import rtlil
  21 from nmigen.sim import Simulator
  22 from nmigen.asserts import Assert, Assume, Past, AnyConst
  23
  24 from nmutil.formaltest import FHDLTestCase
  25 from nmutil.gtkw import write_gtkw
  26
  27
  28 class SinglePortSRAM(Elaboratable):
  29     """
  30     Model of a single port SRAM, which can be simulated, verified and/or
  31     synthesized to an FPGA.
  32
  33     :param addr_width: width of the address bus
  34     :param data_width: width of the data bus
  35     :param we_width: number of write enable lines
  36
  37     .. note:: The debug read port is meant only to assist in formal proofs!
  38     """
  39     def __init__(self, addr_width, data_width, we_width):
  40         self.addr_width = addr_width
  41         self.data_width = data_width
  42         self.we_width = we_width
  43         self.d = Signal(data_width)
  44         """ write data"""
  45         self.q = Signal(data_width)
  46         """read data"""
  47         self.a = Signal(addr_width)
  48         """ read/write address"""
  49         self.we = Signal(we_width)
  50         """write enable"""
  51         self.dbg_a = Signal(addr_width)
  52         """debug read port address"""
  53         self.dbg_q = Signal(data_width)
  54         """debug read port data"""
  55
  56     def elaborate(self, _):
  57         m = Module()
  58         # backing memory
  59         depth = 1 << self.addr_width
  60         granularity = 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=granularity)
  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         # the debug port is an asynchronous read port, allowing direct access
  80         # to a given memory location by the formal engine
  81         m.submodules.dbgport = dbgport = mem.read_port(domain="comb")
  82         m.d.comb += dbgport.addr.eq(self.dbg_a)
  83         m.d.comb += self.dbg_q.eq(dbgport.data)
  84         return m
  85
  86     def ports(self):
  87         return [
  88             self.d,
  89             self.a,
  90             self.we,
  91             self.q
  92         ]
  93
  94
  95 def create_ilang(dut, ports, test_name):
  96     vl = rtlil.convert(dut, name=test_name, ports=ports)
  97     with open("%s.il" % test_name, "w") as f:
  98         f.write(vl)
  99
 100
 101 class SinglePortSRAMTestCase(FHDLTestCase):
 102     @staticmethod
 103     def test_simple_rtlil():
 104         """
 105         Generate a simple SRAM. Try ``read_rtlil mem_simple.il; proc; show``
 106         from a yosys prompt, to see the memory primitives, and
 107         ``read_rtlil mem_simple.il; synth; show`` to see it implemented as
 108         flip-flop RAM
 109         """
 110         dut = SinglePortSRAM(2, 4, 2)
 111         create_ilang(dut, dut.ports(), "mem_simple")
 112
 113     @staticmethod
 114     def test_blkram_rtlil():
 115         """
 116         Generates a bigger SRAM.
 117         Try ``read_rtlil mem_blkram.il; synth_ecp5; show`` from a yosys
 118         prompt, to see it implemented as block RAM
 119         """
 120         dut = SinglePortSRAM(10, 16, 2)
 121         create_ilang(dut, dut.ports(), "mem_blkram")
 122
 123     def test_sram_model(self):
 124         """
 125         Simulate some read/write/modify operations on the SRAM model
 126         """
 127         dut = SinglePortSRAM(7, 32, 4)
 128         sim = Simulator(dut)
 129         sim.add_clock(1e-6)
 130
 131         def process():
 132             # 1) write 0x12_34_56_78 to address 0
 133             yield dut.a.eq(0)
 134             yield dut.d.eq(0x12_34_56_78)
 135             yield dut.we.eq(0b1111)
 136             yield
 137             # 2) write 0x9A_BC_DE_F0 to address 1
 138             yield dut.a.eq(1)
 139             yield dut.d.eq(0x9A_BC_DE_F0)
 140             yield dut.we.eq(0b1111)
 141             yield
 142             # ... and read value just written to address 0
 143             self.assertEqual((yield dut.q), 0x12_34_56_78)
 144             # 3) prepare to read from address 0
 145             yield dut.d.eq(0)
 146             yield dut.we.eq(0b0000)
 147             yield dut.a.eq(0)
 148             yield
 149             # ... and read value just written to address 1
 150             self.assertEqual((yield dut.q), 0x9A_BC_DE_F0)
 151             # 4) prepare to read from address 1
 152             yield dut.a.eq(1)
 153             yield
 154             # ... and read value from address 0
 155             self.assertEqual((yield dut.q), 0x12_34_56_78)
 156             # 5) write 0x9A and 0xDE to bytes 1 and 3, leaving
 157             # bytes 0 and 2 unchanged
 158             yield dut.a.eq(0)
 159             yield dut.d.eq(0x9A_FF_DE_FF)
 160             yield dut.we.eq(0b1010)
 161             yield
 162             # ... and read value from address 1
 163             self.assertEqual((yield dut.q), 0x9A_BC_DE_F0)
 164             # 6) nothing more to do
 165             yield dut.d.eq(0)
 166             yield dut.we.eq(0)
 167             yield
 168             # ... other than confirm that bytes 1 and 3 were modified
 169             # correctly
 170             self.assertEqual((yield dut.q), 0x9A_34_DE_78)
 171
 172         sim.add_sync_process(process)
 173         traces = ['rdport.clk', 'a[6:0]', 'we[3:0]', 'd[31:0]', 'q[31:0]']
 174         write_gtkw('test_sram_model.gtkw', 'test_sram_model.vcd',
 175                    traces, module='top')
 176         sim_writer = sim.write_vcd('test_sram_model.vcd')
 177         with sim_writer:
 178             sim.run()
 179
 180     def test_model_sram_proof(self):
 181         """
 182         Formal proof of the single port SRAM model
 183         """
 184         m = Module()
 185         # 128 x 32-bit, 8-bit granularity
 186         m.submodules.dut = dut = SinglePortSRAM(7, 32, 4)
 187         gran = len(dut.d) // len(dut.we)  # granularity
 188         # choose a single random memory location to test
 189         a_const = AnyConst(dut.a.shape())
 190         # choose a single byte lane to test (one-hot encoding)
 191         we_mask = Signal.like(dut.we)
 192         # ... by first creating a random bit pattern
 193         we_const = AnyConst(dut.we.shape())
 194         # ... and zeroing all but the first non-zero bit
 195         m.d.comb += we_mask.eq(we_const & (-we_const))
 196         # holding data register
 197         d_reg = Signal(gran)
 198         # for some reason, simulated formal memory is not zeroed at reset
 199         # ... so, remember whether we wrote it, at least once.
 200         wrote = Signal()
 201         # if our memory location and byte lane is being written
 202         # ... capture the data in our holding register
 203         with m.If(dut.a == a_const):
 204             for i in range(len(dut.we)):
 205                 with m.If(we_mask[i] & dut.we[i]):
 206                     m.d.sync += d_reg.eq(dut.d[i*gran:i*gran+gran])
 207                     m.d.sync += wrote.eq(1)
 208         # if our memory location is being read
 209         # ... and the holding register has valid data
 210         # ... then its value must match the memory output, on the given lane
 211         with m.If((Past(dut.a) == a_const) & wrote):
 212             for i in range(len(dut.we)):
 213                 with m.If(we_mask[i]):
 214                     m.d.sync += Assert(d_reg == dut.q[i*gran:i*gran+gran])
 215
 216         # the following is needed for induction, where an unreachable state
 217         # (memory and holding register differ) is turned into an illegal one
 218         # first, get the value stored in our memory location, using its debug
 219         # port
 220         stored = Signal.like(dut.q)
 221         m.d.comb += dut.dbg_a.eq(a_const)
 222         m.d.comb += stored.eq(dut.dbg_q)
 223         # now, ensure that the value stored in memory is always in sync
 224         # with the holding register
 225         with m.If(wrote):
 226             for i in range(len(dut.we)):
 227                 with m.If(we_mask[i]):
 228                     m.d.sync += Assert(d_reg == stored[i*gran:i*gran+gran])
 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         self.wr_addr_i = Signal(addr_width)
 258         """write port address"""
 259         self.wr_data_i = Signal(data_width)
 260         """write port data"""
 261         self.wr_we_i = Signal(we_width)
 262         """write port enable"""
 263         self.rd_addr_i = Signal(addr_width)
 264         """read port address"""
 265         self.rd_data_o = Signal(data_width)
 266         """read port data"""
 267         self.phase = Signal()
 268         """even/odd cycle indicator"""
 269         self.dbg_a = Signal(addr_width)
 270         """debug read port address"""
 271         self.dbg_q1 = Signal(data_width)
 272         """debug read port data (first memory)"""
 273         self.dbg_q2 = Signal(data_width)
 274         """debug read port data (second memory)"""
 275
 276     def elaborate(self, _):
 277         m = Module()
 278         # instantiate the two 1RW memory blocks
 279         mem1 = SinglePortSRAM(self.addr_width, self.data_width, self.we_width)
 280         mem2 = SinglePortSRAM(self.addr_width, self.data_width, self.we_width)
 281         m.submodules.mem1 = mem1
 282         m.submodules.mem2 = mem2
 283         # wire write port to first memory, and its output to the second
 284         m.d.comb += mem1.d.eq(self.wr_data_i)
 285         m.d.comb += mem2.d.eq(mem1.q)
 286         # holding registers for the write port of the second memory
 287         last_wr_addr = Signal(self.addr_width)
 288         last_wr_we = Signal(self.we_width)
 289         # do the read and write address coincide?
 290         same_read_write = Signal()
 291         with m.If(self.phase == self.write_phase):
 292             # write phase, start a write on the first memory
 293             m.d.comb += mem1.a.eq(self.wr_addr_i)
 294             m.d.comb += mem1.we.eq(self.wr_we_i)
 295             # save write address and write select for repeating the write
 296             # on the second memory, later
 297             m.d.sync += last_wr_we.eq(self.wr_we_i)
 298             m.d.sync += last_wr_addr.eq(self.wr_addr_i)
 299             # start a read on the second memory
 300             m.d.comb += mem2.a.eq(self.rd_addr_i)
 301             # output previously read data from the first memory
 302             m.d.comb += self.rd_data_o.eq(mem1.q)
 303             if self.transparent:
 304                 # remember whether we are reading from the same location we are
 305                 # writing
 306                 m.d.sync += same_read_write.eq(self.rd_addr_i == self.wr_addr_i)
 307         with m.Else():
 308             # read phase, write last written data on second memory
 309             m.d.comb += mem2.a.eq(last_wr_addr)
 310             m.d.comb += mem2.we.eq(last_wr_we)
 311             # start a read on the first memory
 312             m.d.comb += mem1.a.eq(self.rd_addr_i)
 313             if self.transparent:
 314                 with m.If(same_read_write):
 315                     # when transparent, and read and write addresses coincide,
 316                     # output the data just written
 317                     m.d.comb += self.rd_data_o.eq(mem1.q)
 318                 with m.Else():
 319                     # otherwise, output previously read data
 320                     # from the second memory
 321                     m.d.comb += self.rd_data_o.eq(mem2.q)
 322             else:
 323                 # always output the read data from the second memory,
 324                 # if not transparent
 325                 m.d.comb += self.rd_data_o.eq(mem2.q)
 326         # our debug port allow the formal engine to inspect the content of
 327         # a fixed, arbitrary address, on our memory blocks.
 328         # wire it to their debug ports.
 329         m.d.comb += mem1.dbg_a.eq(self.dbg_a)
 330         m.d.comb += mem2.dbg_a.eq(self.dbg_a)
 331         m.d.comb += self.dbg_q1.eq(mem1.dbg_q)
 332         m.d.comb += self.dbg_q2.eq(mem2.dbg_q)
 333
 334         return m
 335
 336
 337 class PhasedDualPortRegfileTestCase(FHDLTestCase):
 338
 339     def do_test_phased_dual_port_regfile(self, write_phase, transparent):
 340         """
 341         Simulate some read/write/modify operations on the phased write memory
 342         """
 343         dut = PhasedDualPortRegfile(7, 32, 4, write_phase, transparent)
 344         sim = Simulator(dut)
 345         sim.add_clock(1e-6)
 346
 347         # compare read data with previously written data
 348         # and start a new read
 349         def read(rd_addr_i, expected=None):
 350             if expected is not None:
 351                 self.assertEqual((yield dut.rd_data_o), expected)
 352             yield dut.rd_addr_i.eq(rd_addr_i)
 353
 354         # start a write, and set write phase
 355         def write(wr_addr_i, wr_we_i, wr_data_i):
 356             yield dut.wr_addr_i.eq(wr_addr_i)
 357             yield dut.wr_we_i.eq(wr_we_i)
 358             yield dut.wr_data_i.eq(wr_data_i)
 359             yield dut.phase.eq(write_phase)
 360
 361         # disable writes, and start read phase
 362         def skip_write():
 363             yield dut.wr_addr_i.eq(0)
 364             yield dut.wr_we_i.eq(0)
 365             yield dut.wr_data_i.eq(0)
 366             yield dut.phase.eq(~write_phase)
 367
 368         # writes a few values on the write port, and read them back
 369         # ... reads can happen every cycle
 370         # ... writes, only every two cycles.
 371         # since reads have a one cycle delay, the expected value on
 372         # each read refers to the last read performed, not the
 373         # current one, which is in progress.
 374         def process():
 375             yield from read(0)
 376             yield from write(0x42, 0b1111, 0x12345678)
 377             yield
 378             yield from read(0x42)
 379             yield from skip_write()
 380             yield
 381             yield from read(0x42)
 382             yield from write(0x43, 0b1111, 0x9ABCDEF0)
 383             yield
 384             yield from read(0x43, 0x12345678)
 385             yield from skip_write()
 386             yield
 387             yield from read(0x42, 0x12345678)
 388             yield from write(0x43, 0b1001, 0xF0FFFF9A)
 389             yield
 390             yield from read(0x43, 0x9ABCDEF0)
 391             yield from skip_write()
 392             yield
 393             yield from read(0x43, 0x12345678)
 394             yield from write(0x42, 0b0110, 0xFF5634FF)
 395             yield
 396             yield from read(0x42, 0xF0BCDE9A)
 397             yield from skip_write()
 398             yield
 399             yield from read(0, 0xF0BCDE9A)
 400             yield from write(0, 0, 0)
 401             yield
 402             yield from read(0, 0x12563478)
 403             yield from skip_write()
 404             yield
 405             # try reading and writing to the same location, simultaneously
 406             yield from read(0x42)
 407             yield from write(0x42, 0b1111, 0x55AA9966)
 408             yield
 409             # ... and read again
 410             yield from read(0x42)
 411             yield from skip_write()
 412             yield
 413             if transparent:
 414                 # returns the value just written
 415                 yield from read(0, 0x55AA9966)
 416             else:
 417                 # returns the old value
 418                 yield from read(0, 0x12563478)
 419             yield from write(0, 0, 0)
 420             yield
 421             # after a cycle, always returns the new value
 422             yield from read(0, 0x55AA9966)
 423             yield from skip_write()
 424
 425         sim.add_sync_process(process)
 426         debug_file = f'test_phased_dual_port_{write_phase}'
 427         if transparent:
 428             debug_file += '_transparent'
 429         traces = ['clk', 'phase',
 430                   'wr_addr_i[6:0]', 'wr_we_i[3:0]', 'wr_data_i[31:0]',
 431                   'rd_addr_i[6:0]', 'rd_data_o[31:0]']
 432         write_gtkw(debug_file + '.gtkw',
 433                    debug_file + '.vcd',
 434                    traces, module='top', zoom=-22)
 435         sim_writer = sim.write_vcd(debug_file + '.vcd')
 436         with sim_writer:
 437             sim.run()
 438
 439     def test_phased_dual_port_regfile(self):
 440         """test both types (odd and even write ports) of phased write memory"""
 441         with self.subTest("writes happen on phase 0"):
 442             self.do_test_phased_dual_port_regfile(0, False)
 443         with self.subTest("writes happen on phase 1"):
 444             self.do_test_phased_dual_port_regfile(1, False)
 445         """test again, with a transparent read port"""
 446         with self.subTest("writes happen on phase 0 (transparent reads)"):
 447             self.do_test_phased_dual_port_regfile(0, True)
 448         with self.subTest("writes happen on phase 1 (transparent reads)"):
 449             self.do_test_phased_dual_port_regfile(1, True)
 450
 451     def test_phased_dual_port_regfile_proof(self):
 452         """
 453         Formal proof of the pseudo 1W/1R regfile
 454         """
 455         m = Module()
 456         # 128 x 32-bit, 8-bit granularity
 457         m.submodules.dut = dut = PhasedDualPortRegfile(7, 32, 4, 0, True)
 458         gran = dut.data_width // dut.we_width  # granularity
 459         # choose a single random memory location to test
 460         a_const = AnyConst(dut.addr_width)
 461         # choose a single byte lane to test (one-hot encoding)
 462         we_mask = Signal(dut.we_width)
 463         # ... by first creating a random bit pattern
 464         we_const = AnyConst(dut.we_width)
 465         # ... and zeroing all but the first non-zero bit
 466         m.d.comb += we_mask.eq(we_const & (-we_const))
 467         # drive alternating phases
 468         m.d.comb += Assume(dut.phase != Past(dut.phase))
 469         # holding data register
 470         d_reg = Signal(gran)
 471         # for some reason, simulated formal memory is not zeroed at reset
 472         # ... so, remember whether we wrote it, at least once.
 473         wrote = Signal()
 474         # if our memory location and byte lane is being written,
 475         # capture the data in our holding register
 476         with m.If((dut.wr_addr_i == a_const)
 477                   & (dut.phase == dut.write_phase)):
 478             for i in range(dut.we_width):
 479                 with m.If(we_mask[i] & dut.wr_we_i[i]):
 480                     m.d.sync += d_reg.eq(
 481                         dut.wr_data_i[i * gran:i * gran + gran])
 482                     m.d.sync += wrote.eq(1)
 483         # if our memory location is being read,
 484         # and the holding register has valid data,
 485         # then its value must match the memory output, on the given lane
 486         with m.If((Past(dut.rd_addr_i) == a_const) & wrote):
 487             for i in range(dut.we_width):
 488                 with m.If(we_mask[i]):
 489                     m.d.sync += Assert(
 490                         d_reg == dut.rd_data_o[i * gran:i * gran + gran])
 491
 492         # the following is needed for induction, where an unreachable state
 493         # (memory and holding register differ) is turned into an illegal one
 494         # first, get the values stored in our memory location, using its
 495         # debug port
 496         stored1 = Signal(dut.data_width)
 497         stored2 = Signal(dut.data_width)
 498         m.d.comb += dut.dbg_a.eq(a_const)
 499         m.d.comb += stored1.eq(dut.dbg_q1)
 500         m.d.comb += stored2.eq(dut.dbg_q2)
 501         # now, ensure that the value stored in the first memory is always
 502         # in sync with the holding register
 503         with m.If(wrote):
 504             for i in range(dut.we_width):
 505                 with m.If(we_mask[i]):
 506                     m.d.comb += Assert(
 507                         d_reg == stored1[i * gran:i * gran + gran])
 508         # same for the second memory, but one cycle later
 509         with m.If(Past(wrote)):
 510             for i in range(dut.we_width):
 511                 with m.If(we_mask[i]):
 512                     m.d.comb += Assert(
 513                         Past(d_reg) == stored2[i * gran:i * gran + gran])
 514
 515         self.assertFormal(m, mode="prove", depth=2)
 516
 517
 518 if __name__ == "__main__":
 519     unittest.main()