ce58793fbf5c50e9551e7cbac8f0cef577763bcd
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
); """ write data"""
44 self
.q
= Signal(data_width
); """read data"""
45 self
.a
= Signal(addr_width
); """ read/write address"""
46 self
.we
= Signal(we_width
); """write enable"""
47 self
.dbg_a
= Signal(addr_width
); """debug read port address"""
48 self
.dbg_q
= Signal(data_width
); """debug read port data"""
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
)
73 # the debug port is an asynchronous read port, allowing direct access
74 # to a given memory location by the formal engine
75 m
.submodules
.dbgport
= dbgport
= mem
.read_port(domain
="comb")
76 m
.d
.comb
+= dbgport
.addr
.eq(self
.dbg_a
)
77 m
.d
.comb
+= self
.dbg_q
.eq(dbgport
.data
)
89 def create_ilang(dut
, ports
, test_name
):
90 vl
= rtlil
.convert(dut
, name
=test_name
, ports
=ports
)
91 with
open("%s.il" % test_name
, "w") as f
:
95 class SinglePortSRAMTestCase(FHDLTestCase
):
97 def test_simple_rtlil():
99 Generate a simple SRAM. Try ``read_rtlil mem_simple.il; proc; show``
100 from a yosys prompt, to see the memory primitives, and
101 ``read_rtlil mem_simple.il; synth; show`` to see it implemented as
104 dut
= SinglePortSRAM(2, 4, 2)
105 create_ilang(dut
, dut
.ports(), "mem_simple")
108 def test_blkram_rtlil():
110 Generates a bigger SRAM.
111 Try ``read_rtlil mem_blkram.il; synth_ecp5; show`` from a yosys
112 prompt, to see it implemented as block RAM
114 dut
= SinglePortSRAM(10, 16, 2)
115 create_ilang(dut
, dut
.ports(), "mem_blkram")
117 def test_sram_model(self
):
119 Simulate some read/write/modify operations on the SRAM model
121 dut
= SinglePortSRAM(7, 32, 4)
126 # 1) write 0x12_34_56_78 to address 0
128 yield dut
.d
.eq(0x12_34_56_78)
129 yield dut
.we
.eq(0b1111)
131 # 2) write 0x9A_BC_DE_F0 to address 1
133 yield dut
.d
.eq(0x9A_BC_DE_F0)
134 yield dut
.we
.eq(0b1111)
136 # ... and read value just written to address 0
137 self
.assertEqual((yield dut
.q
), 0x12_34_56_78)
138 # 3) prepare to read from address 0
140 yield dut
.we
.eq(0b0000)
143 # ... and read value just written to address 1
144 self
.assertEqual((yield dut
.q
), 0x9A_BC_DE_F0)
145 # 4) prepare to read from address 1
148 # ... and read value from address 0
149 self
.assertEqual((yield dut
.q
), 0x12_34_56_78)
150 # 5) write 0x9A and 0xDE to bytes 1 and 3, leaving
151 # bytes 0 and 2 unchanged
153 yield dut
.d
.eq(0x9A_FF_DE_FF)
154 yield dut
.we
.eq(0b1010)
156 # ... and read value from address 1
157 self
.assertEqual((yield dut
.q
), 0x9A_BC_DE_F0)
158 # 6) nothing more to do
162 # ... other than confirm that bytes 1 and 3 were modified
164 self
.assertEqual((yield dut
.q
), 0x9A_34_DE_78)
166 sim
.add_sync_process(process
)
167 traces
= ['rdport.clk', 'a[6:0]', 'we[3:0]', 'd[31:0]', 'q[31:0]']
168 write_gtkw('test_sram_model.gtkw', 'test_sram_model.vcd',
169 traces
, module
='top')
170 sim_writer
= sim
.write_vcd('test_sram_model.vcd')
174 def test_model_sram_proof(self
):
176 Formal proof of the single port SRAM model
179 # 128 x 32-bit, 8-bit granularity
180 m
.submodules
.dut
= dut
= SinglePortSRAM(7, 32, 4)
181 gran
= len(dut
.d
) // len(dut
.we
) # granularity
182 # choose a single random memory location to test
183 a_const
= AnyConst(dut
.a
.shape())
184 # choose a single byte lane to test (one-hot encoding)
185 we_mask
= Signal
.like(dut
.we
)
186 # ... by first creating a random bit pattern
187 we_const
= AnyConst(dut
.we
.shape())
188 # ... and zeroing all but the first non-zero bit
189 m
.d
.comb
+= we_mask
.eq(we_const
& (-we_const
))
190 # holding data register
192 # for some reason, simulated formal memory is not zeroed at reset
193 # ... so, remember whether we wrote it, at least once.
195 # if our memory location and byte lane is being written
196 # ... capture the data in our holding register
197 with m
.If(dut
.a
== a_const
):
198 for i
in range(len(dut
.we
)):
199 with m
.If(we_mask
[i
] & dut
.we
[i
]):
200 m
.d
.sync
+= d_reg
.eq(dut
.d
[i
*gran
:i
*gran
+gran
])
201 m
.d
.sync
+= wrote
.eq(1)
202 # if our memory location is being read
203 # ... and the holding register has valid data
204 # ... then its value must match the memory output, on the given lane
205 with m
.If((Past(dut
.a
) == a_const
) & wrote
):
206 for i
in range(len(dut
.we
)):
207 with m
.If(we_mask
[i
]):
208 m
.d
.sync
+= Assert(d_reg
== dut
.q
[i
*gran
:i
*gran
+gran
])
210 # the following is needed for induction, where an unreachable state
211 # (memory and holding register differ) is turned into an illegal one
212 # first, get the value stored in our memory location, using its debug
214 stored
= Signal
.like(dut
.q
)
215 m
.d
.comb
+= dut
.dbg_a
.eq(a_const
)
216 m
.d
.comb
+= stored
.eq(dut
.dbg_q
)
217 # now, ensure that the value stored in memory is always in sync
218 # with the holding register
220 for i
in range(len(dut
.we
)):
221 with m
.If(we_mask
[i
]):
222 m
.d
.sync
+= Assert(d_reg
== stored
[i
*gran
:i
*gran
+gran
])
224 self
.assertFormal(m
, mode
="prove", depth
=2)
227 class PhasedDualPortRegfile(Elaboratable
):
229 Builds, from a pair of 1RW blocks, a pseudo 1W/1R RAM, where the
230 read port works every cycle, but the write port is only available on
231 either even (1eW/1R) or odd (1oW/1R) cycles.
233 :param addr_width: width of the address bus
234 :param data_width: width of the data bus
235 :param we_width: number of write enable lines
236 :param write_phase: indicates on which phase the write port will
238 :param transparent: whether a simultaneous read and write returns the
239 new value (True) or the old value (False)
241 .. note:: The debug read port is meant only to assist in formal proofs!
244 def __init__(self
, addr_width
, data_width
, we_width
, write_phase
,
246 self
.addr_width
= addr_width
247 self
.data_width
= data_width
248 self
.we_width
= we_width
249 self
.write_phase
= write_phase
250 self
.transparent
= transparent
251 self
.wr_addr_i
= Signal(addr_width
); """write port address"""
252 self
.wr_data_i
= Signal(data_width
); """write port data"""
253 self
.wr_we_i
= Signal(we_width
); """write port enable"""
254 self
.rd_addr_i
= Signal(addr_width
); """read port address"""
255 self
.rd_data_o
= Signal(data_width
); """read port data"""
256 self
.phase
= Signal(); """even/odd cycle indicator"""
257 self
.dbg_a
= Signal(addr_width
); """debug read port address"""
258 self
.dbg_q1
= Signal(data_width
); """debug read port data (1st mem)"""
259 self
.dbg_q2
= Signal(data_width
); """debug read port data (2nd mem)"""
261 def elaborate(self
, _
):
263 # instantiate the two 1RW memory blocks
264 mem1
= SinglePortSRAM(self
.addr_width
, self
.data_width
, self
.we_width
)
265 mem2
= SinglePortSRAM(self
.addr_width
, self
.data_width
, self
.we_width
)
266 m
.submodules
.mem1
= mem1
267 m
.submodules
.mem2
= mem2
268 # wire write port to first memory, and its output to the second
269 m
.d
.comb
+= mem1
.d
.eq(self
.wr_data_i
)
270 m
.d
.comb
+= mem2
.d
.eq(mem1
.q
)
271 # holding registers for the write port of the second memory
272 last_wr_addr
= Signal(self
.addr_width
)
273 last_wr_we
= Signal(self
.we_width
)
274 # do the read and write address coincide?
275 same_read_write
= Signal()
276 with m
.If(self
.phase
== self
.write_phase
):
277 # write phase, start a write on the first memory
278 m
.d
.comb
+= mem1
.a
.eq(self
.wr_addr_i
)
279 m
.d
.comb
+= mem1
.we
.eq(self
.wr_we_i
)
280 # save write address and write select for repeating the write
281 # on the second memory, later
282 m
.d
.sync
+= last_wr_we
.eq(self
.wr_we_i
)
283 m
.d
.sync
+= last_wr_addr
.eq(self
.wr_addr_i
)
284 # start a read on the second memory
285 m
.d
.comb
+= mem2
.a
.eq(self
.rd_addr_i
)
286 # output previously read data from the first memory
287 m
.d
.comb
+= self
.rd_data_o
.eq(mem1
.q
)
289 # remember whether we are reading from the same location we are
291 m
.d
.sync
+= same_read_write
.eq(self
.rd_addr_i
== self
.wr_addr_i
)
293 # read phase, write last written data on second memory
294 m
.d
.comb
+= mem2
.a
.eq(last_wr_addr
)
295 m
.d
.comb
+= mem2
.we
.eq(last_wr_we
)
296 # start a read on the first memory
297 m
.d
.comb
+= mem1
.a
.eq(self
.rd_addr_i
)
299 with m
.If(same_read_write
):
300 # when transparent, and read and write addresses coincide,
301 # output the data just written
302 m
.d
.comb
+= self
.rd_data_o
.eq(mem1
.q
)
304 # otherwise, output previously read data
305 # from the second memory
306 m
.d
.comb
+= self
.rd_data_o
.eq(mem2
.q
)
308 # always output the read data from the second memory,
310 m
.d
.comb
+= self
.rd_data_o
.eq(mem2
.q
)
311 # our debug port allow the formal engine to inspect the content of
312 # a fixed, arbitrary address, on our memory blocks.
313 # wire it to their debug ports.
314 m
.d
.comb
+= mem1
.dbg_a
.eq(self
.dbg_a
)
315 m
.d
.comb
+= mem2
.dbg_a
.eq(self
.dbg_a
)
316 m
.d
.comb
+= self
.dbg_q1
.eq(mem1
.dbg_q
)
317 m
.d
.comb
+= self
.dbg_q2
.eq(mem2
.dbg_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 do_test_phased_dual_port_regfile_proof(self
, write_phase
, transparent
):
438 Formal proof of the pseudo 1W/1R regfile
441 # 128 x 32-bit, 8-bit granularity
442 dut
= PhasedDualPortRegfile(7, 32, 4, write_phase
, transparent
)
443 m
.submodules
.dut
= dut
444 gran
= dut
.data_width
// dut
.we_width
# granularity
445 # choose a single random memory location to test
446 a_const
= AnyConst(dut
.addr_width
)
447 # choose a single byte lane to test (one-hot encoding)
448 we_mask
= Signal(dut
.we_width
)
449 # ... by first creating a random bit pattern
450 we_const
= AnyConst(dut
.we_width
)
451 # ... and zeroing all but the first non-zero bit
452 m
.d
.comb
+= we_mask
.eq(we_const
& (-we_const
))
453 # drive alternating phases
454 m
.d
.comb
+= Assume(dut
.phase
!= Past(dut
.phase
))
455 # holding data register
457 # for some reason, simulated formal memory is not zeroed at reset
458 # ... so, remember whether we wrote it, at least once.
460 # if our memory location and byte lane is being written,
461 # capture the data in our holding register
462 with m
.If((dut
.wr_addr_i
== a_const
)
463 & (dut
.phase
== dut
.write_phase
)):
464 for i
in range(dut
.we_width
):
465 with m
.If(we_mask
[i
] & dut
.wr_we_i
[i
]):
466 m
.d
.sync
+= d_reg
.eq(
467 dut
.wr_data_i
[i
* gran
:i
* gran
+ gran
])
468 m
.d
.sync
+= wrote
.eq(1)
469 # if our memory location is being read,
470 # and the holding register has valid data,
471 # then its value must match the memory output, on the given lane
472 with m
.If(Past(dut
.rd_addr_i
) == a_const
):
475 for i
in range(dut
.we_width
):
476 rd_lane
= dut
.rd_data_o
.word_select(i
, gran
)
477 with m
.If(we_mask
[i
]):
478 m
.d
.sync
+= Assert(d_reg
== rd_lane
)
480 # with a non-transparent read port, the read value depends
481 # on whether there is a simultaneous write, or not
482 with m
.If((Past(dut
.wr_addr_i
) == a_const
)
483 & Past(dut
.phase
) == dut
.write_phase
):
484 # simultaneous write -> check against last written value
485 with m
.If(Past(wrote
)):
486 for i
in range(dut
.we_width
):
487 rd_lane
= dut
.rd_data_o
.word_select(i
, gran
)
488 with m
.If(we_mask
[i
]):
489 m
.d
.sync
+= Assert(Past(d_reg
) == rd_lane
)
491 # otherwise, check against current written value
493 for i
in range(dut
.we_width
):
494 rd_lane
= dut
.rd_data_o
.word_select(i
, gran
)
495 with m
.If(we_mask
[i
]):
496 m
.d
.sync
+= Assert(d_reg
== rd_lane
)
498 # the following is needed for induction, where an unreachable state
499 # (memory and holding register differ) is turned into an illegal one
500 # first, get the values stored in our memory location, using its
502 stored1
= Signal(dut
.data_width
)
503 stored2
= Signal(dut
.data_width
)
504 m
.d
.comb
+= dut
.dbg_a
.eq(a_const
)
505 m
.d
.comb
+= stored1
.eq(dut
.dbg_q1
)
506 m
.d
.comb
+= stored2
.eq(dut
.dbg_q2
)
507 # now, ensure that the value stored in the first memory is always
508 # in sync with the holding register
510 for i
in range(dut
.we_width
):
511 with m
.If(we_mask
[i
]):
513 d_reg
== stored1
[i
* gran
:i
* gran
+ gran
])
514 # same for the second memory, but one cycle later
515 with m
.If(Past(wrote
)):
516 for i
in range(dut
.we_width
):
517 with m
.If(we_mask
[i
]):
519 Past(d_reg
) == stored2
[i
* gran
:i
* gran
+ gran
])
521 self
.assertFormal(m
, mode
="prove", depth
=2)
523 def test_phased_dual_port_regfile_proof(self
):
524 """test both types (odd and even write ports) of phased write memory"""
525 with self
.subTest("writes happen on phase 0"):
526 self
.do_test_phased_dual_port_regfile_proof(0, False)
527 with self
.subTest("writes happen on phase 1"):
528 self
.do_test_phased_dual_port_regfile_proof(1, False)
529 # test again, with transparent read ports
530 with self
.subTest("writes happen on phase 0 (transparent reads)"):
531 self
.do_test_phased_dual_port_regfile_proof(0, True)
532 with self
.subTest("writes happen on phase 1 (transparent reads)"):
533 self
.do_test_phased_dual_port_regfile_proof(1, True)
536 if __name__
== "__main__":