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)
247 .. note:: The debug read port is meant only to assist in formal proofs!
250 def __init__(self
, addr_width
, data_width
, we_width
, write_phase
,
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
)
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)"""
276 def elaborate(self
, _
):
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
)
304 # remember whether we are reading from the same location we are
306 m
.d
.sync
+= same_read_write
.eq(self
.rd_addr_i
== self
.wr_addr_i
)
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
)
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
)
319 # otherwise, output previously read data
320 # from the second memory
321 m
.d
.comb
+= self
.rd_data_o
.eq(mem2
.q
)
323 # always output the read data from the second memory,
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
)
337 class PhasedDualPortRegfileTestCase(FHDLTestCase
):
339 def do_test_phased_dual_port_regfile(self
, write_phase
, transparent
):
341 Simulate some read/write/modify operations on the phased write memory
343 dut
= PhasedDualPortRegfile(7, 32, 4, write_phase
, transparent
)
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
)
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
)
361 # disable writes, and start read phase
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
)
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.
376 yield from write(0x42, 0b1111, 0x12345678)
378 yield from read(0x42)
379 yield from skip_write()
381 yield from read(0x42)
382 yield from write(0x43, 0b1111, 0x9ABCDEF0)
384 yield from read(0x43, 0x12345678)
385 yield from skip_write()
387 yield from read(0x42, 0x12345678)
388 yield from write(0x43, 0b1001, 0xF0FFFF9A)
390 yield from read(0x43, 0x9ABCDEF0)
391 yield from skip_write()
393 yield from read(0x43, 0x12345678)
394 yield from write(0x42, 0b0110, 0xFF5634FF)
396 yield from read(0x42, 0xF0BCDE9A)
397 yield from skip_write()
399 yield from read(0, 0xF0BCDE9A)
400 yield from write(0, 0, 0)
402 yield from read(0, 0x12563478)
403 yield from skip_write()
405 # try reading and writing to the same location, simultaneously
406 yield from read(0x42)
407 yield from write(0x42, 0b1111, 0x55AA9966)
410 yield from read(0x42)
411 yield from skip_write()
414 # returns the value just written
415 yield from read(0, 0x55AA9966)
417 # returns the old value
418 yield from read(0, 0x12563478)
419 yield from write(0, 0, 0)
421 # after a cycle, always returns the new value
422 yield from read(0, 0x55AA9966)
423 yield from skip_write()
425 sim
.add_sync_process(process
)
426 debug_file
= f
'test_phased_dual_port_{write_phase}'
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',
434 traces
, module
='top', zoom
=-22)
435 sim_writer
= sim
.write_vcd(debug_file
+ '.vcd')
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)
451 def test_phased_dual_port_regfile_proof(self
):
453 Formal proof of the pseudo 1W/1R regfile
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
471 # for some reason, simulated formal memory is not zeroed at reset
472 # ... so, remember whether we wrote it, at least once.
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
]):
490 d_reg
== dut
.rd_data_o
[i
* gran
:i
* gran
+ gran
])
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
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
504 for i
in range(dut
.we_width
):
505 with m
.If(we_mask
[i
]):
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
]):
513 Past(d_reg
) == stored2
[i
* gran
:i
* gran
+ gran
])
515 self
.assertFormal(m
, mode
="prove", depth
=2)
518 if __name__
== "__main__":