447b6ca9e020e3a1257b62916904ed56047ccb2b
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.
7 Wrapper around a single port (1R or 1W) SRAM, to make a multi-port regfile.
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
13 See https://bugs.libre-soc.org/show_bug.cgi?id=781 and
14 https://bugs.libre-soc.org/show_bug.cgi?id=502
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
24 from nmutil
.formaltest
import FHDLTestCase
25 from nmutil
.gtkw
import write_gtkw
28 class SinglePortSRAM(Elaboratable
):
30 Model of a single port SRAM, which can be simulated, verified and/or
31 synthesized to an FPGA.
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
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
)
43 self
.q
= Signal(data_width
)
45 self
.a
= Signal(addr_width
)
46 """ read/write address"""
47 self
.we
= Signal(we_width
)
50 def elaborate(self
, _
):
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,
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
)
69 m
.d
.comb
+= wrport
.en
.eq(self
.we
)
71 m
.d
.comb
+= wrport
.data
.eq(self
.d
)
72 m
.d
.comb
+= self
.q
.eq(rdport
.data
)
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
:
90 class SinglePortSRAMTestCase(FHDLTestCase
):
92 def test_simple_rtlil():
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
99 dut
= SinglePortSRAM(2, 4, 2)
100 create_ilang(dut
, dut
.ports(), "mem_simple")
103 def test_blkram_rtlil():
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
109 dut
= SinglePortSRAM(10, 16, 2)
110 create_ilang(dut
, dut
.ports(), "mem_blkram")
112 def test_sram_model(self
):
114 Simulate some read/write/modify operations on the SRAM model
116 dut
= SinglePortSRAM(7, 32, 4)
121 # 1) write 0x12_34_56_78 to address 0
123 yield dut
.d
.eq(0x12_34_56_78)
124 yield dut
.we
.eq(0b1111)
126 # 2) write 0x9A_BC_DE_F0 to address 1
128 yield dut
.d
.eq(0x9A_BC_DE_F0)
129 yield dut
.we
.eq(0b1111)
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
135 yield dut
.we
.eq(0b0000)
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
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
148 yield dut
.d
.eq(0x9A_FF_DE_FF)
149 yield dut
.we
.eq(0b1010)
151 # ... and read value from address 1
152 self
.assertEqual((yield dut
.q
), 0x9A_BC_DE_F0)
153 # 6) nothing more to do
157 # ... other than confirm that bytes 1 and 3 were modified
159 self
.assertEqual((yield dut
.q
), 0x9A_34_DE_78)
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')
169 def test_model_sram_proof(self
):
171 Formal proof of the single port SRAM model
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
187 # for some reason, simulated formal memory is not zeroed at reset
188 # ... so, remember whether we wrote it, at least once.
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
])
205 self
.assertFormal(m
, mode
="bmc", depth
=10)
208 if __name__
== "__main__":