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, 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     def __init__(self, addr_width, data_width, we_width):
  38         self.addr_width = addr_width
  39         self.data_width = data_width
  40         self.we_width = we_width
  41         self.d = Signal(data_width)
  42         """ write data"""
  43         self.q = Signal(data_width)
  44         """read data"""
  45         self.a = Signal(addr_width)
  46         """ read/write address"""
  47         self.we = Signal(we_width)
  48         """write enable"""
  49
  50     def elaborate(self, _):
  51         m = Module()
  52         # backing memory
  53         depth = 1 << self.addr_width
  54         granularity = self.data_width // self.we_width
  55         mem = Memory(width=self.data_width, depth=depth)
  56         # create read and write ports
  57         # By connecting the same address to both ports, they behave, in fact,
  58         # as a single, "half-duplex" port.
  59         # The transparent attribute means that, on a write, we read the new
  60         # value, on the next cycle
  61         # Note that nmigen memories have a one cycle delay, for reads,
  62         # by default
  63         m.submodules.rdport = rdport = mem.read_port(transparent=True)
  64         m.submodules.wrport = wrport = mem.write_port(granularity=granularity)
  65         # duplicate the address to both ports
  66         m.d.comb += wrport.addr.eq(self.a)
  67         m.d.comb += rdport.addr.eq(self.a)
  68         # write enable
  69         m.d.comb += wrport.en.eq(self.we)
  70         # read and write data
  71         m.d.comb += wrport.data.eq(self.d)
  72         m.d.comb += self.q.eq(rdport.data)
  73         return m
  74
  75     def ports(self):
  76         return [
  77             self.d,
  78             self.a,
  79             self.we,
  80             self.q
  81         ]
  82
  83
  84 def create_ilang(dut, ports, test_name):
  85     vl = rtlil.convert(dut, name=test_name, ports=ports)
  86     with open("%s.il" % test_name, "w") as f:
  87         f.write(vl)
  88
  89
  90 class SinglePortSRAMTestCase(FHDLTestCase):
  91     @staticmethod
  92     def test_simple_rtlil():
  93         """
  94         Generate a simple SRAM. Try ``read_rtlil mem_simple.il; proc; show``
  95         from a yosys prompt, to see the memory primitives, and
  96         ``read_rtlil mem_simple.il; synth; show`` to see it implemented as
  97         flip-flop RAM
  98         """
  99         dut = SinglePortSRAM(2, 4, 2)
 100         create_ilang(dut, dut.ports(), "mem_simple")
 101
 102     @staticmethod
 103     def test_blkram_rtlil():
 104         """
 105         Generates a bigger SRAM.
 106         Try ``read_rtlil mem_blkram.il; synth_ecp5; show`` from a yosys
 107         prompt, to see it implemented as block RAM
 108         """
 109         dut = SinglePortSRAM(10, 16, 2)
 110         create_ilang(dut, dut.ports(), "mem_blkram")
 111
 112     def test_sram_model(self):
 113         """
 114         Simulate some read/write/modify operations on the SRAM model
 115         """
 116         dut = SinglePortSRAM(7, 32, 4)
 117         sim = Simulator(dut)
 118         sim.add_clock(1e-6)
 119
 120         def process():
 121             # 1) write 0x12_34_56_78 to address 0
 122             yield dut.a.eq(0)
 123             yield dut.d.eq(0x12_34_56_78)
 124             yield dut.we.eq(0b1111)
 125             yield
 126             # 2) write 0x9A_BC_DE_F0 to address 1
 127             yield dut.a.eq(1)
 128             yield dut.d.eq(0x9A_BC_DE_F0)
 129             yield dut.we.eq(0b1111)
 130             yield
 131             # ... and read value just written to address 0
 132             self.assertEqual((yield dut.q), 0x12_34_56_78)
 133             # 3) prepare to read from address 0
 134             yield dut.d.eq(0)
 135             yield dut.we.eq(0b0000)
 136             yield dut.a.eq(0)
 137             yield
 138             # ... and read value just written to address 1
 139             self.assertEqual((yield dut.q), 0x9A_BC_DE_F0)
 140             # 4) prepare to read from address 1
 141             yield dut.a.eq(1)
 142             yield
 143             # ... and read value from address 0
 144             self.assertEqual((yield dut.q), 0x12_34_56_78)
 145             # 5) write 0x9A and 0xDE to bytes 1 and 3, leaving
 146             # bytes 0 and 2 unchanged
 147             yield dut.a.eq(0)
 148             yield dut.d.eq(0x9A_FF_DE_FF)
 149             yield dut.we.eq(0b1010)
 150             yield
 151             # ... and read value from address 1
 152             self.assertEqual((yield dut.q), 0x9A_BC_DE_F0)
 153             # 6) nothing more to do
 154             yield dut.d.eq(0)
 155             yield dut.we.eq(0)
 156             yield
 157             # ... other than confirm that bytes 1 and 3 were modified
 158             # correctly
 159             self.assertEqual((yield dut.q), 0x9A_34_DE_78)
 160
 161         sim.add_sync_process(process)
 162         traces = ['rdport.clk', 'a[6:0]', 'we[3:0]', 'd[31:0]', 'q[31:0]']
 163         write_gtkw('test_sram_model.gtkw', 'test_sram_model.vcd',
 164                    traces, module='top')
 165         sim_writer = sim.write_vcd('test_sram_model.vcd')
 166         with sim_writer:
 167             sim.run()
 168
 169     def test_model_sram_proof(self):
 170         """
 171         Formal proof of the single port SRAM model
 172         """
 173         m = Module()
 174         # 128 x 32-bit, 8-bit granularity
 175         m.submodules.dut = dut = SinglePortSRAM(7, 32, 4)
 176         gran = len(dut.d) // len(dut.we)  # granularity
 177         # choose a single random memory location to test
 178         a_const = AnyConst(dut.a.shape())
 179         # choose a single byte lane to test (one-hot encoding)
 180         we_mask = Signal.like(dut.we)
 181         # ... by first creating a random bit pattern
 182         we_const = AnyConst(dut.we.shape())
 183         # ... and zeroing all but the first non-zero bit
 184         m.d.comb += we_mask.eq(we_const & (-we_const))
 185         # holding data register
 186         d_reg = Signal(gran)
 187         # for some reason, simulated formal memory is not zeroed at reset
 188         # ... so, remember whether we wrote it, at least once.
 189         wrote = Signal()
 190         # if our memory location and byte lane is being written
 191         # ... capture the data in our holding register
 192         with m.If(dut.a == a_const):
 193             for i in range(len(dut.we)):
 194                 with m.If(we_mask[i] & dut.we[i]):
 195                     m.d.sync += d_reg.eq(dut.d[i*gran:i*gran+gran])
 196                     m.d.sync += wrote.eq(1)
 197         # if our memory location is being read
 198         # ... and the holding register has valid data
 199         # ... then its value must match the memory output, on the given lane
 200         with m.If((Past(dut.a) == a_const) & wrote):
 201             for i in range(len(dut.we)):
 202                 with m.If(we_mask[i]):
 203                     m.d.sync += Assert(d_reg == dut.q[i*gran:i*gran+gran])
 204
 205         self.assertFormal(m, mode="bmc", depth=10)
 206
 207
 208 if __name__ == "__main__":
 209     unittest.main()