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
, Assume
, 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 .. note:: The debug read port is meant only to assist in formal proofs!
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
)
45 self
.q
= Signal(data_width
)
47 self
.a
= Signal(addr_width
)
48 """ read/write address"""
49 self
.we
= Signal(we_width
)
51 self
.dbg_a
= Signal(addr_width
)
52 """debug read port address"""
53 self
.dbg_q
= Signal(data_width
)
54 """debug read port data"""
56 def elaborate(self
, _
):
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,
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
)
75 m
.d
.comb
+= wrport
.en
.eq(self
.we
)
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
)
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
:
101 class SinglePortSRAMTestCase(FHDLTestCase
):
103 def test_simple_rtlil():
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
110 dut
= SinglePortSRAM(2, 4, 2)
111 create_ilang(dut
, dut
.ports(), "mem_simple")
114 def test_blkram_rtlil():
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
120 dut
= SinglePortSRAM(10, 16, 2)
121 create_ilang(dut
, dut
.ports(), "mem_blkram")
123 def test_sram_model(self
):
125 Simulate some read/write/modify operations on the SRAM model
127 dut
= SinglePortSRAM(7, 32, 4)
132 # 1) write 0x12_34_56_78 to address 0
134 yield dut
.d
.eq(0x12_34_56_78)
135 yield dut
.we
.eq(0b1111)
137 # 2) write 0x9A_BC_DE_F0 to address 1
139 yield dut
.d
.eq(0x9A_BC_DE_F0)
140 yield dut
.we
.eq(0b1111)
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
146 yield dut
.we
.eq(0b0000)
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
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
159 yield dut
.d
.eq(0x9A_FF_DE_FF)
160 yield dut
.we
.eq(0b1010)
162 # ... and read value from address 1
163 self
.assertEqual((yield dut
.q
), 0x9A_BC_DE_F0)
164 # 6) nothing more to do
168 # ... other than confirm that bytes 1 and 3 were modified
170 self
.assertEqual((yield dut
.q
), 0x9A_34_DE_78)
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')
180 def test_model_sram_proof(self
):
182 Formal proof of the single port SRAM model
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
198 # for some reason, simulated formal memory is not zeroed at reset
199 # ... so, remember whether we wrote it, at least once.
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
])
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
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
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
])
230 self
.assertFormal(m
, mode
="prove", depth
=2)
233 class PhasedDualPortRegfile(Elaboratable
):
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.
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
244 :param transparent: whether a simultaneous read and write returns the
245 new value (True) or the old value (False)
248 def __init__(self
, addr_width
, data_width
, we_width
, write_phase
,
250 self
.addr_width
= addr_width
251 self
.data_width
= data_width
252 self
.we_width
= we_width
253 self
.write_phase
= write_phase
254 self
.transparent
= transparent
255 self
.wr_addr_i
= Signal(addr_width
)
256 """write port address"""
257 self
.wr_data_i
= Signal(data_width
)
258 """write port data"""
259 self
.wr_we_i
= Signal(we_width
)
260 """write port enable"""
261 self
.rd_addr_i
= Signal(addr_width
)
262 """read port address"""
263 self
.rd_data_o
= Signal(data_width
)
265 self
.phase
= Signal()
266 """even/odd cycle indicator"""
268 def elaborate(self
, _
):
270 # instantiate the two 1RW memory blocks
271 mem1
= SinglePortSRAM(self
.addr_width
, self
.data_width
, self
.we_width
)
272 mem2
= SinglePortSRAM(self
.addr_width
, self
.data_width
, self
.we_width
)
273 m
.submodules
.mem1
= mem1
274 m
.submodules
.mem2
= mem2
275 # wire write port to first memory, and its output to the second
276 m
.d
.comb
+= mem1
.d
.eq(self
.wr_data_i
)
277 m
.d
.comb
+= mem2
.d
.eq(mem1
.q
)
278 # holding registers for the write port of the second memory
279 last_wr_addr
= Signal(self
.addr_width
)
280 last_wr_we
= Signal(self
.we_width
)
281 # do the read and write address coincide?
282 same_read_write
= Signal()
283 with m
.If(self
.phase
== self
.write_phase
):
284 # write phase, start a write on the first memory
285 m
.d
.comb
+= mem1
.a
.eq(self
.wr_addr_i
)
286 m
.d
.comb
+= mem1
.we
.eq(self
.wr_we_i
)
287 # save write address and write select for repeating the write
288 # on the second memory, later
289 m
.d
.sync
+= last_wr_we
.eq(self
.wr_we_i
)
290 m
.d
.sync
+= last_wr_addr
.eq(self
.wr_addr_i
)
291 # start a read on the second memory
292 m
.d
.comb
+= mem2
.a
.eq(self
.rd_addr_i
)
293 # output previously read data from the first memory
294 m
.d
.comb
+= self
.rd_data_o
.eq(mem1
.q
)
296 # remember whether we are reading from the same location we are
298 m
.d
.sync
+= same_read_write
.eq(self
.rd_addr_i
== self
.wr_addr_i
)
300 # read phase, write last written data on second memory
301 m
.d
.comb
+= mem2
.a
.eq(last_wr_addr
)
302 m
.d
.comb
+= mem2
.we
.eq(last_wr_we
)
303 # start a read on the first memory
304 m
.d
.comb
+= mem1
.a
.eq(self
.rd_addr_i
)
306 with m
.If(same_read_write
):
307 # when transparent, and read and write addresses coincide,
308 # output the data just written
309 m
.d
.comb
+= self
.rd_data_o
.eq(mem1
.q
)
311 # otherwise, output previously read data
312 # from the second memory
313 m
.d
.comb
+= self
.rd_data_o
.eq(mem2
.q
)
315 # always output the read data from the second memory,
317 m
.d
.comb
+= self
.rd_data_o
.eq(mem2
.q
)
322 class PhasedDualPortRegfileTestCase(FHDLTestCase
):
324 def do_test_phased_dual_port_regfile(self
, write_phase
, transparent
):
326 Simulate some read/write/modify operations on the phased write memory
328 dut
= PhasedDualPortRegfile(7, 32, 4, write_phase
, transparent
)
332 # compare read data with previously written data
333 # and start a new read
334 def read(rd_addr_i
, expected
=None):
335 if expected
is not None:
336 self
.assertEqual((yield dut
.rd_data_o
), expected
)
337 yield dut
.rd_addr_i
.eq(rd_addr_i
)
339 # start a write, and set write phase
340 def write(wr_addr_i
, wr_we_i
, wr_data_i
):
341 yield dut
.wr_addr_i
.eq(wr_addr_i
)
342 yield dut
.wr_we_i
.eq(wr_we_i
)
343 yield dut
.wr_data_i
.eq(wr_data_i
)
344 yield dut
.phase
.eq(write_phase
)
346 # disable writes, and start read phase
348 yield dut
.wr_addr_i
.eq(0)
349 yield dut
.wr_we_i
.eq(0)
350 yield dut
.wr_data_i
.eq(0)
351 yield dut
.phase
.eq(~write_phase
)
353 # writes a few values on the write port, and read them back
354 # ... reads can happen every cycle
355 # ... writes, only every two cycles.
356 # since reads have a one cycle delay, the expected value on
357 # each read refers to the last read performed, not the
358 # current one, which is in progress.
361 yield from write(0x42, 0b1111, 0x12345678)
363 yield from read(0x42)
364 yield from skip_write()
366 yield from read(0x42)
367 yield from write(0x43, 0b1111, 0x9ABCDEF0)
369 yield from read(0x43, 0x12345678)
370 yield from skip_write()
372 yield from read(0x42, 0x12345678)
373 yield from write(0x43, 0b1001, 0xF0FFFF9A)
375 yield from read(0x43, 0x9ABCDEF0)
376 yield from skip_write()
378 yield from read(0x43, 0x12345678)
379 yield from write(0x42, 0b0110, 0xFF5634FF)
381 yield from read(0x42, 0xF0BCDE9A)
382 yield from skip_write()
384 yield from read(0, 0xF0BCDE9A)
385 yield from write(0, 0, 0)
387 yield from read(0, 0x12563478)
388 yield from skip_write()
390 # try reading and writing to the same location, simultaneously
391 yield from read(0x42)
392 yield from write(0x42, 0b1111, 0x55AA9966)
395 yield from read(0x42)
396 yield from skip_write()
399 # returns the value just written
400 yield from read(0, 0x55AA9966)
402 # returns the old value
403 yield from read(0, 0x12563478)
404 yield from write(0, 0, 0)
406 # after a cycle, always returns the new value
407 yield from read(0, 0x55AA9966)
408 yield from skip_write()
410 sim
.add_sync_process(process
)
411 debug_file
= f
'test_phased_dual_port_{write_phase}'
413 debug_file
+= '_transparent'
414 traces
= ['clk', 'phase',
415 'wr_addr_i[6:0]', 'wr_we_i[3:0]', 'wr_data_i[31:0]',
416 'rd_addr_i[6:0]', 'rd_data_o[31:0]']
417 write_gtkw(debug_file
+ '.gtkw',
419 traces
, module
='top', zoom
=-22)
420 sim_writer
= sim
.write_vcd(debug_file
+ '.vcd')
424 def test_phased_dual_port_regfile(self
):
425 """test both types (odd and even write ports) of phased write memory"""
426 with self
.subTest("writes happen on phase 0"):
427 self
.do_test_phased_dual_port_regfile(0, False)
428 with self
.subTest("writes happen on phase 1"):
429 self
.do_test_phased_dual_port_regfile(1, False)
430 """test again, with a transparent read port"""
431 with self
.subTest("writes happen on phase 0 (transparent reads)"):
432 self
.do_test_phased_dual_port_regfile(0, True)
433 with self
.subTest("writes happen on phase 1 (transparent reads)"):
434 self
.do_test_phased_dual_port_regfile(1, True)
436 def test_phased_dual_port_regfile_proof(self
):
438 Formal proof of the pseudo 1W/1R regfile
441 # 128 x 32-bit, 8-bit granularity
442 m
.submodules
.dut
= dut
= PhasedDualPortRegfile(7, 32, 4, 0, True)
443 gran
= dut
.data_width
// dut
.we_width
# granularity
444 # choose a single random memory location to test
445 a_const
= AnyConst(dut
.addr_width
)
446 # choose a single byte lane to test (one-hot encoding)
447 we_mask
= Signal(dut
.we_width
)
448 # ... by first creating a random bit pattern
449 we_const
= AnyConst(dut
.we_width
)
450 # ... and zeroing all but the first non-zero bit
451 m
.d
.comb
+= we_mask
.eq(we_const
& (-we_const
))
452 # drive alternating phases
453 m
.d
.comb
+= Assume(dut
.phase
!= Past(dut
.phase
))
454 # holding data register
456 # for some reason, simulated formal memory is not zeroed at reset
457 # ... so, remember whether we wrote it, at least once.
459 # if our memory location and byte lane is being written,
460 # capture the data in our holding register
461 with m
.If((dut
.wr_addr_i
== a_const
)
462 & (dut
.phase
== dut
.write_phase
)):
463 for i
in range(dut
.we_width
):
464 with m
.If(we_mask
[i
] & dut
.wr_we_i
[i
]):
465 m
.d
.sync
+= d_reg
.eq(
466 dut
.wr_data_i
[i
* gran
:i
* gran
+ gran
])
467 m
.d
.sync
+= wrote
.eq(1)
468 # if our memory location is being read,
469 # and the holding register has valid data,
470 # then its value must match the memory output, on the given lane
471 with m
.If((Past(dut
.rd_addr_i
) == a_const
) & wrote
):
472 for i
in range(dut
.we_width
):
473 with m
.If(we_mask
[i
]):
475 d_reg
== dut
.rd_data_o
[i
* gran
:i
* gran
+ gran
])
477 self
.assertFormal(m
, mode
="bmc", depth
=10)
480 if __name__
== "__main__":