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
, Repl
, Mux
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
44 self
.d
= Signal(data_width
); """ write data"""
45 self
.q
= Signal(data_width
); """read data"""
46 self
.a
= Signal(addr_width
); """ read/write address"""
47 self
.we
= Signal(we_width
); """write enable"""
48 # debug signals, only used in formal proofs
49 self
.dbg_addr
= Signal(addr_width
); """debug: address under test"""
50 self
.dbg_we_mask
= Signal(we_width
); """debug: write lane under test"""
51 gran
= self
.data_width
// self
.we_width
52 self
.dbg_data
= Signal(gran
); """debug: data to keep in sync"""
53 self
.dbg_wrote
= Signal(); """debug: data is valid"""
55 def elaborate(self
, platform
):
58 depth
= 1 << self
.addr_width
59 gran
= self
.data_width
// self
.we_width
60 mem
= Memory(width
=self
.data_width
, depth
=depth
)
61 # create read and write ports
62 # By connecting the same address to both ports, they behave, in fact,
63 # as a single, "half-duplex" port.
64 # The transparent attribute means that, on a write, we read the new
65 # value, on the next cycle
66 # Note that nmigen memories have a one cycle delay, for reads,
68 m
.submodules
.rdport
= rdport
= mem
.read_port(transparent
=True)
69 m
.submodules
.wrport
= wrport
= mem
.write_port(granularity
=gran
)
70 # duplicate the address to both ports
71 m
.d
.comb
+= wrport
.addr
.eq(self
.a
)
72 m
.d
.comb
+= rdport
.addr
.eq(self
.a
)
74 m
.d
.comb
+= wrport
.en
.eq(self
.we
)
76 m
.d
.comb
+= wrport
.data
.eq(self
.d
)
77 m
.d
.comb
+= self
.q
.eq(rdport
.data
)
79 # the following is needed for induction, where an unreachable state
80 # (memory and holding register differ) is turned into an illegal one
81 if platform
== "formal":
82 # the debug port is an asynchronous read port, allowing direct
83 # access to a given memory location by the formal engine
84 m
.submodules
.dbgport
= dbgport
= mem
.read_port(domain
="comb")
85 # first, get the value stored in our memory location,
86 # using its debug port
87 stored
= Signal(self
.data_width
)
88 m
.d
.comb
+= dbgport
.addr
.eq(self
.dbg_addr
)
89 m
.d
.comb
+= stored
.eq(dbgport
.data
)
90 # now, ensure that the value stored in memory is always in sync
91 # with the holding register
92 with m
.If(self
.dbg_wrote
):
93 for i
in range(self
.we_width
):
94 with m
.If(self
.dbg_we_mask
[i
]):
95 m
.d
.sync
+= Assert(self
.dbg_data
==
96 stored
.word_select(i
, gran
))
109 def create_ilang(dut
, ports
, test_name
):
110 vl
= rtlil
.convert(dut
, name
=test_name
, ports
=ports
)
111 with
open("%s.il" % test_name
, "w") as f
:
115 class SinglePortSRAMTestCase(FHDLTestCase
):
117 def test_simple_rtlil():
119 Generate a simple SRAM. Try ``read_rtlil mem_simple.il; proc; show``
120 from a yosys prompt, to see the memory primitives, and
121 ``read_rtlil mem_simple.il; synth; show`` to see it implemented as
124 dut
= SinglePortSRAM(2, 4, 2)
125 create_ilang(dut
, dut
.ports(), "mem_simple")
128 def test_blkram_rtlil():
130 Generates a bigger SRAM.
131 Try ``read_rtlil mem_blkram.il; synth_ecp5; show`` from a yosys
132 prompt, to see it implemented as block RAM
134 dut
= SinglePortSRAM(10, 16, 2)
135 create_ilang(dut
, dut
.ports(), "mem_blkram")
137 def test_sram_model(self
):
139 Simulate some read/write/modify operations on the SRAM model
141 dut
= SinglePortSRAM(7, 32, 4)
146 # 1) write 0x12_34_56_78 to address 0
148 yield dut
.d
.eq(0x12_34_56_78)
149 yield dut
.we
.eq(0b1111)
151 # 2) write 0x9A_BC_DE_F0 to address 1
153 yield dut
.d
.eq(0x9A_BC_DE_F0)
154 yield dut
.we
.eq(0b1111)
156 # ... and read value just written to address 0
157 self
.assertEqual((yield dut
.q
), 0x12_34_56_78)
158 # 3) prepare to read from address 0
160 yield dut
.we
.eq(0b0000)
163 # ... and read value just written to address 1
164 self
.assertEqual((yield dut
.q
), 0x9A_BC_DE_F0)
165 # 4) prepare to read from address 1
168 # ... and read value from address 0
169 self
.assertEqual((yield dut
.q
), 0x12_34_56_78)
170 # 5) write 0x9A and 0xDE to bytes 1 and 3, leaving
171 # bytes 0 and 2 unchanged
173 yield dut
.d
.eq(0x9A_FF_DE_FF)
174 yield dut
.we
.eq(0b1010)
176 # ... and read value from address 1
177 self
.assertEqual((yield dut
.q
), 0x9A_BC_DE_F0)
178 # 6) nothing more to do
182 # ... other than confirm that bytes 1 and 3 were modified
184 self
.assertEqual((yield dut
.q
), 0x9A_34_DE_78)
186 sim
.add_sync_process(process
)
187 traces
= ['rdport.clk', 'a[6:0]', 'we[3:0]', 'd[31:0]', 'q[31:0]']
188 write_gtkw('test_sram_model.gtkw', 'test_sram_model.vcd',
189 traces
, module
='top')
190 sim_writer
= sim
.write_vcd('test_sram_model.vcd')
194 def test_model_sram_proof(self
):
196 Formal proof of the single port SRAM model
199 # 128 x 32-bit, 8-bit granularity
200 m
.submodules
.dut
= dut
= SinglePortSRAM(7, 32, 4)
201 gran
= len(dut
.d
) // len(dut
.we
) # granularity
202 # choose a single random memory location to test
203 a_const
= AnyConst(dut
.a
.shape())
204 # choose a single byte lane to test (one-hot encoding)
205 we_mask
= Signal
.like(dut
.we
)
206 # ... by first creating a random bit pattern
207 we_const
= AnyConst(dut
.we
.shape())
208 # ... and zeroing all but the first non-zero bit
209 m
.d
.comb
+= we_mask
.eq(we_const
& (-we_const
))
210 # holding data register
212 # for some reason, simulated formal memory is not zeroed at reset
213 # ... so, remember whether we wrote it, at least once.
215 # if our memory location and byte lane is being written
216 # ... capture the data in our holding register
217 with m
.If(dut
.a
== a_const
):
218 for i
in range(len(dut
.we
)):
219 with m
.If(we_mask
[i
] & dut
.we
[i
]):
220 m
.d
.sync
+= d_reg
.eq(dut
.d
[i
*gran
:i
*gran
+gran
])
221 m
.d
.sync
+= wrote
.eq(1)
222 # if our memory location is being read
223 # ... and the holding register has valid data
224 # ... then its value must match the memory output, on the given lane
225 with m
.If((Past(dut
.a
) == a_const
) & wrote
):
226 for i
in range(len(dut
.we
)):
227 with m
.If(we_mask
[i
]):
228 m
.d
.sync
+= Assert(d_reg
== dut
.q
[i
*gran
:i
*gran
+gran
])
230 # pass our state to the device under test, so it can ensure that
231 # its state is in sync with ours, for induction
233 dut
.dbg_addr
.eq(a_const
),
234 dut
.dbg_we_mask
.eq(we_mask
),
235 dut
.dbg_data
.eq(d_reg
),
236 dut
.dbg_wrote
.eq(wrote
),
239 self
.assertFormal(m
, mode
="prove", depth
=2)
242 class PhasedDualPortRegfile(Elaboratable
):
244 Builds, from a pair of 1RW blocks, a pseudo 1W/1R RAM, where the
245 read port works every cycle, but the write port is only available on
246 either even (1eW/1R) or odd (1oW/1R) cycles.
248 :param addr_width: width of the address bus
249 :param data_width: width of the data bus
250 :param we_width: number of write enable lines
251 :param write_phase: indicates on which phase the write port will
253 :param transparent: whether a simultaneous read and write returns the
254 new value (True) or the old value (False)
256 .. note:: The debug read port is meant only to assist in formal proofs!
259 def __init__(self
, addr_width
, data_width
, we_width
, write_phase
,
261 self
.addr_width
= addr_width
262 self
.data_width
= data_width
263 self
.we_width
= we_width
264 self
.write_phase
= write_phase
265 self
.transparent
= transparent
267 self
.wr_addr_i
= Signal(addr_width
); """write port address"""
268 self
.wr_data_i
= Signal(data_width
); """write port data"""
269 self
.wr_we_i
= Signal(we_width
); """write port enable"""
270 self
.rd_addr_i
= Signal(addr_width
); """read port address"""
271 self
.rd_data_o
= Signal(data_width
); """read port data"""
272 self
.phase
= Signal(); """even/odd cycle indicator"""
273 # debug signals, only used in formal proofs
274 self
.dbg_addr
= Signal(addr_width
); """debug: address under test"""
275 self
.dbg_we_mask
= Signal(we_width
); """debug: write lane under test"""
276 gran
= self
.data_width
// self
.we_width
277 self
.dbg_data
= Signal(gran
); """debug: data to keep in sync"""
278 self
.dbg_wrote
= Signal(); """debug: data is valid"""
280 def elaborate(self
, platform
):
283 # instantiate the two 1RW memory blocks
284 mem1
= SinglePortSRAM(self
.addr_width
, self
.data_width
, self
.we_width
)
285 mem2
= SinglePortSRAM(self
.addr_width
, self
.data_width
, self
.we_width
)
286 m
.submodules
.mem1
= mem1
287 m
.submodules
.mem2
= mem2
288 # wire write port to first memory, and its output to the second
289 m
.d
.comb
+= mem1
.d
.eq(self
.wr_data_i
)
290 m
.d
.comb
+= mem2
.d
.eq(mem1
.q
)
291 # holding registers for the write port of the second memory
292 last_wr_addr
= Signal(self
.addr_width
)
293 last_wr_we
= Signal(self
.we_width
)
294 # do the read and write address coincide?
295 same_read_write
= Signal()
296 with m
.If(self
.phase
== self
.write_phase
):
297 # write phase, start a write on the first memory
298 m
.d
.comb
+= mem1
.a
.eq(self
.wr_addr_i
)
299 m
.d
.comb
+= mem1
.we
.eq(self
.wr_we_i
)
300 # save write address and write select for repeating the write
301 # on the second memory, later
302 m
.d
.sync
+= last_wr_we
.eq(self
.wr_we_i
)
303 m
.d
.sync
+= last_wr_addr
.eq(self
.wr_addr_i
)
304 # start a read on the second memory
305 m
.d
.comb
+= mem2
.a
.eq(self
.rd_addr_i
)
306 # output previously read data from the first memory
307 m
.d
.comb
+= self
.rd_data_o
.eq(mem1
.q
)
309 # remember whether we are reading from the same location we are
311 m
.d
.sync
+= same_read_write
.eq(self
.rd_addr_i
== self
.wr_addr_i
)
313 # read phase, write last written data on second memory
314 m
.d
.comb
+= mem2
.a
.eq(last_wr_addr
)
315 m
.d
.comb
+= mem2
.we
.eq(last_wr_we
)
316 # start a read on the first memory
317 m
.d
.comb
+= mem1
.a
.eq(self
.rd_addr_i
)
319 with m
.If(same_read_write
):
320 # when transparent, and read and write addresses coincide,
321 # output the data just written
322 m
.d
.comb
+= self
.rd_data_o
.eq(mem1
.q
)
324 # otherwise, output previously read data
325 # from the second memory
326 m
.d
.comb
+= self
.rd_data_o
.eq(mem2
.q
)
328 # always output the read data from the second memory,
330 m
.d
.comb
+= self
.rd_data_o
.eq(mem2
.q
)
332 if platform
== "formal":
333 # pass our state to the device under test, so it can ensure that
334 # its state is in sync with ours, for induction
336 # pass the address and write lane under test to both memories
337 mem1
.dbg_addr
.eq(self
.dbg_addr
),
338 mem2
.dbg_addr
.eq(self
.dbg_addr
),
339 mem1
.dbg_we_mask
.eq(self
.dbg_we_mask
),
340 mem2
.dbg_we_mask
.eq(self
.dbg_we_mask
),
341 # the second memory copies its state from the first memory,
342 # after a cycle, so it has a one cycle delay
343 mem1
.dbg_data
.eq(self
.dbg_data
),
344 mem2
.dbg_data
.eq(Past(self
.dbg_data
)),
345 mem1
.dbg_wrote
.eq(self
.dbg_wrote
),
346 mem2
.dbg_wrote
.eq(Past(self
.dbg_wrote
)),
352 class PhasedDualPortRegfileTestCase(FHDLTestCase
):
354 def do_test_phased_dual_port_regfile(self
, write_phase
, transparent
):
356 Simulate some read/write/modify operations on the phased write memory
358 dut
= PhasedDualPortRegfile(7, 32, 4, write_phase
, transparent
)
362 # compare read data with previously written data
363 # and start a new read
364 def read(rd_addr_i
, expected
=None):
365 if expected
is not None:
366 self
.assertEqual((yield dut
.rd_data_o
), expected
)
367 yield dut
.rd_addr_i
.eq(rd_addr_i
)
369 # start a write, and set write phase
370 def write(wr_addr_i
, wr_we_i
, wr_data_i
):
371 yield dut
.wr_addr_i
.eq(wr_addr_i
)
372 yield dut
.wr_we_i
.eq(wr_we_i
)
373 yield dut
.wr_data_i
.eq(wr_data_i
)
374 yield dut
.phase
.eq(write_phase
)
376 # disable writes, and start read phase
378 yield dut
.wr_addr_i
.eq(0)
379 yield dut
.wr_we_i
.eq(0)
380 yield dut
.wr_data_i
.eq(0)
381 yield dut
.phase
.eq(~write_phase
)
383 # writes a few values on the write port, and read them back
384 # ... reads can happen every cycle
385 # ... writes, only every two cycles.
386 # since reads have a one cycle delay, the expected value on
387 # each read refers to the last read performed, not the
388 # current one, which is in progress.
391 yield from write(0x42, 0b1111, 0x12345678)
393 yield from read(0x42)
394 yield from skip_write()
396 yield from read(0x42)
397 yield from write(0x43, 0b1111, 0x9ABCDEF0)
399 yield from read(0x43, 0x12345678)
400 yield from skip_write()
402 yield from read(0x42, 0x12345678)
403 yield from write(0x43, 0b1001, 0xF0FFFF9A)
405 yield from read(0x43, 0x9ABCDEF0)
406 yield from skip_write()
408 yield from read(0x43, 0x12345678)
409 yield from write(0x42, 0b0110, 0xFF5634FF)
411 yield from read(0x42, 0xF0BCDE9A)
412 yield from skip_write()
414 yield from read(0, 0xF0BCDE9A)
415 yield from write(0, 0, 0)
417 yield from read(0, 0x12563478)
418 yield from skip_write()
420 # try reading and writing to the same location, simultaneously
421 yield from read(0x42)
422 yield from write(0x42, 0b1111, 0x55AA9966)
425 yield from read(0x42)
426 yield from skip_write()
429 # returns the value just written
430 yield from read(0, 0x55AA9966)
432 # returns the old value
433 yield from read(0, 0x12563478)
434 yield from write(0, 0, 0)
436 # after a cycle, always returns the new value
437 yield from read(0, 0x55AA9966)
438 yield from skip_write()
440 sim
.add_sync_process(process
)
441 debug_file
= f
'test_phased_dual_port_{write_phase}'
443 debug_file
+= '_transparent'
444 traces
= ['clk', 'phase',
445 'wr_addr_i[6:0]', 'wr_we_i[3:0]', 'wr_data_i[31:0]',
446 'rd_addr_i[6:0]', 'rd_data_o[31:0]']
447 write_gtkw(debug_file
+ '.gtkw',
449 traces
, module
='top', zoom
=-22)
450 sim_writer
= sim
.write_vcd(debug_file
+ '.vcd')
454 def test_phased_dual_port_regfile(self
):
455 """test both types (odd and even write ports) of phased write memory"""
456 with self
.subTest("writes happen on phase 0"):
457 self
.do_test_phased_dual_port_regfile(0, False)
458 with self
.subTest("writes happen on phase 1"):
459 self
.do_test_phased_dual_port_regfile(1, False)
460 """test again, with a transparent read port"""
461 with self
.subTest("writes happen on phase 0 (transparent reads)"):
462 self
.do_test_phased_dual_port_regfile(0, True)
463 with self
.subTest("writes happen on phase 1 (transparent reads)"):
464 self
.do_test_phased_dual_port_regfile(1, True)
466 def do_test_phased_dual_port_regfile_proof(self
, write_phase
, transparent
):
468 Formal proof of the pseudo 1W/1R regfile
471 # 128 x 32-bit, 8-bit granularity
472 dut
= PhasedDualPortRegfile(7, 32, 4, write_phase
, transparent
)
473 m
.submodules
.dut
= dut
474 gran
= dut
.data_width
// dut
.we_width
# granularity
475 # choose a single random memory location to test
476 a_const
= AnyConst(dut
.addr_width
)
477 # choose a single byte lane to test (one-hot encoding)
478 we_mask
= Signal(dut
.we_width
)
479 # ... by first creating a random bit pattern
480 we_const
= AnyConst(dut
.we_width
)
481 # ... and zeroing all but the first non-zero bit
482 m
.d
.comb
+= we_mask
.eq(we_const
& (-we_const
))
483 # drive alternating phases
484 m
.d
.comb
+= Assume(dut
.phase
!= Past(dut
.phase
))
485 # holding data register
487 # for some reason, simulated formal memory is not zeroed at reset
488 # ... so, remember whether we wrote it, at least once.
490 # if our memory location and byte lane is being written,
491 # capture the data in our holding register
492 with m
.If((dut
.wr_addr_i
== a_const
)
493 & (dut
.phase
== dut
.write_phase
)):
494 for i
in range(dut
.we_width
):
495 with m
.If(we_mask
[i
] & dut
.wr_we_i
[i
]):
496 m
.d
.sync
+= d_reg
.eq(
497 dut
.wr_data_i
[i
* gran
:i
* gran
+ gran
])
498 m
.d
.sync
+= wrote
.eq(1)
499 # if our memory location is being read,
500 # and the holding register has valid data,
501 # then its value must match the memory output, on the given lane
502 with m
.If(Past(dut
.rd_addr_i
) == a_const
):
505 for i
in range(dut
.we_width
):
506 rd_lane
= dut
.rd_data_o
.word_select(i
, gran
)
507 with m
.If(we_mask
[i
]):
508 m
.d
.sync
+= Assert(d_reg
== rd_lane
)
510 # with a non-transparent read port, the read value depends
511 # on whether there is a simultaneous write, or not
512 with m
.If((Past(dut
.wr_addr_i
) == a_const
)
513 & Past(dut
.phase
) == dut
.write_phase
):
514 # simultaneous write -> check against last written value
515 with m
.If(Past(wrote
)):
516 for i
in range(dut
.we_width
):
517 rd_lane
= dut
.rd_data_o
.word_select(i
, gran
)
518 with m
.If(we_mask
[i
]):
519 m
.d
.sync
+= Assert(Past(d_reg
) == rd_lane
)
521 # otherwise, check against current written value
523 for i
in range(dut
.we_width
):
524 rd_lane
= dut
.rd_data_o
.word_select(i
, gran
)
525 with m
.If(we_mask
[i
]):
526 m
.d
.sync
+= Assert(d_reg
== rd_lane
)
528 # pass our state to the device under test, so it can ensure that
529 # its state is in sync with ours, for induction
531 # address and mask under test
532 dut
.dbg_addr
.eq(a_const
),
533 dut
.dbg_we_mask
.eq(we_mask
),
534 # state of our holding register
535 dut
.dbg_data
.eq(d_reg
),
536 dut
.dbg_wrote
.eq(wrote
),
539 self
.assertFormal(m
, mode
="prove", depth
=3)
541 def test_phased_dual_port_regfile_proof(self
):
542 """test both types (odd and even write ports) of phased write memory"""
543 with self
.subTest("writes happen on phase 0"):
544 self
.do_test_phased_dual_port_regfile_proof(0, False)
545 with self
.subTest("writes happen on phase 1"):
546 self
.do_test_phased_dual_port_regfile_proof(1, False)
547 # test again, with transparent read ports
548 with self
.subTest("writes happen on phase 0 (transparent reads)"):
549 self
.do_test_phased_dual_port_regfile_proof(0, True)
550 with self
.subTest("writes happen on phase 1 (transparent reads)"):
551 self
.do_test_phased_dual_port_regfile_proof(1, True)
554 class DualPortRegfile(Elaboratable
):
556 Builds, from a pair of phased 1W/1R blocks, a true 1W/1R RAM, where both
557 read and write ports work every cycle.
558 It employs a Last Value Table, that tracks to which memory each address was
561 :param addr_width: width of the address bus
562 :param data_width: width of the data bus
563 :param we_width: number of write enable lines
564 :param transparent: whether a simultaneous read and write returns the
565 new value (True) or the old value (False)
568 def __init__(self
, addr_width
, data_width
, we_width
, transparent
=True):
569 self
.addr_width
= addr_width
570 self
.data_width
= data_width
571 self
.we_width
= we_width
572 self
.transparent
= transparent
574 self
.wr_addr_i
= Signal(addr_width
); """write port address"""
575 self
.wr_data_i
= Signal(data_width
); """write port data"""
576 self
.wr_we_i
= Signal(we_width
); """write port enable"""
577 self
.rd_addr_i
= Signal(addr_width
); """read port address"""
578 self
.rd_data_o
= Signal(data_width
); """read port data"""
579 # debug signals, only used in formal proofs
580 # address and write lane under test
581 self
.dbg_addr
= Signal(addr_width
); """debug: address under test"""
582 self
.dbg_we_mask
= Signal(we_width
); """debug: write lane under test"""
583 # upstream state, to keep in sync with ours
584 gran
= self
.data_width
// self
.we_width
585 self
.dbg_data
= Signal(gran
); """debug: data to keep in sync"""
586 self
.dbg_wrote
= Signal(); """debug: data is valid"""
587 self
.dbg_wrote_phase
= Signal(); """debug: the phase data was written"""
588 self
.dbg_phase
= Signal(); """debug: current phase"""
590 def elaborate(self
, platform
):
592 # depth and granularity
593 depth
= 1 << self
.addr_width
594 gran
= self
.data_width
// self
.we_width
595 # instantiate the two phased 1R/1W memory blocks
596 mem0
= PhasedDualPortRegfile(
597 self
.addr_width
, self
.data_width
, self
.we_width
, 0,
599 mem1
= PhasedDualPortRegfile(
600 self
.addr_width
, self
.data_width
, self
.we_width
, 1,
602 m
.submodules
.mem0
= mem0
603 m
.submodules
.mem1
= mem1
604 # instantiate the backing memory (FFRAM or LUTRAM)
605 # for the Last Value Table
606 # it should have the same number and port types of the desired
607 # memory, but just one bit per write lane
608 lvt_mem
= Memory(width
=self
.we_width
, depth
=depth
)
609 lvt_wr
= lvt_mem
.write_port(granularity
=1)
610 lvt_rd
= lvt_mem
.read_port(transparent
=self
.transparent
)
611 m
.submodules
.lvt_wr
= lvt_wr
612 m
.submodules
.lvt_rd
= lvt_rd
613 # generate and wire the phases for the phased memories
615 m
.d
.sync
+= phase
.eq(~phase
)
617 mem0
.phase
.eq(phase
),
618 mem1
.phase
.eq(phase
),
621 # wire the write ports, directly
622 mem0
.wr_addr_i
.eq(self
.wr_addr_i
),
623 mem1
.wr_addr_i
.eq(self
.wr_addr_i
),
624 mem0
.wr_we_i
.eq(self
.wr_we_i
),
625 mem1
.wr_we_i
.eq(self
.wr_we_i
),
626 mem0
.wr_data_i
.eq(self
.wr_data_i
),
627 mem1
.wr_data_i
.eq(self
.wr_data_i
),
628 # also wire the read addresses
629 mem0
.rd_addr_i
.eq(self
.rd_addr_i
),
630 mem1
.rd_addr_i
.eq(self
.rd_addr_i
),
631 # wire read and write ports to the LVT
632 lvt_wr
.addr
.eq(self
.wr_addr_i
),
633 lvt_wr
.en
.eq(self
.wr_we_i
),
634 lvt_rd
.addr
.eq(self
.rd_addr_i
),
635 # the data for the LVT is the phase on which the value was
637 lvt_wr
.data
.eq(Repl(phase
, self
.we_width
)),
639 for i
in range(self
.we_width
):
640 # select the right memory to assign to the output read port,
641 # in this byte lane, according to the LVT contents
642 m
.d
.comb
+= self
.rd_data_o
.word_select(i
, gran
).eq(
645 mem1
.rd_data_o
.word_select(i
, gran
),
646 mem0
.rd_data_o
.word_select(i
, gran
)))
648 if platform
== "formal":
649 # pass upstream state to the memories, so they can ensure that
650 # their state are in sync with upstream, for induction
652 # address and write lane under test
653 mem0
.dbg_addr
.eq(self
.dbg_addr
),
654 mem1
.dbg_addr
.eq(self
.dbg_addr
),
655 mem0
.dbg_we_mask
.eq(self
.dbg_we_mask
),
656 mem1
.dbg_we_mask
.eq(self
.dbg_we_mask
),
658 mem0
.dbg_data
.eq(self
.dbg_data
),
659 mem1
.dbg_data
.eq(self
.dbg_data
),
660 # the memory, on which the write ends up, depends on which
661 # phase it was written
662 mem0
.dbg_wrote
.eq(self
.dbg_wrote
& ~self
.dbg_wrote_phase
),
663 mem1
.dbg_wrote
.eq(self
.dbg_wrote
& self
.dbg_wrote_phase
),
665 # sync phase to upstream
666 m
.d
.comb
+= Assert(self
.dbg_phase
== phase
)
670 class DualPortRegfileTestCase(FHDLTestCase
):
672 def do_test_dual_port_regfile(self
, transparent
):
674 Simulate some read/write/modify operations on the dual port register
677 dut
= DualPortRegfile(7, 32, 4, transparent
)
684 # compare read data with previously written data
685 # and start a new read
686 def read(rd_addr_i
, next_expected
=None):
687 nonlocal expected
, last_expected
688 if expected
is not None:
689 self
.assertEqual((yield dut
.rd_data_o
), expected
)
690 yield dut
.rd_addr_i
.eq(rd_addr_i
)
691 # account for the read latency
692 expected
= last_expected
693 last_expected
= next_expected
696 def write(wr_addr_i
, wr_we_i
, wr_data_i
):
697 yield dut
.wr_addr_i
.eq(wr_addr_i
)
698 yield dut
.wr_we_i
.eq(wr_we_i
)
699 yield dut
.wr_data_i
.eq(wr_data_i
)
702 # write a pair of values, one for each memory
704 yield from write(0x42, 0b1111, 0x87654321)
706 yield from read(0x42, 0x87654321)
707 yield from write(0x43, 0b1111, 0x0FEDCBA9)
710 yield from read(0x43, 0x0FEDCBA9)
711 yield from write(0, 0, 0)
713 # write again, but now they switch memories
715 yield from write(0x42, 0b1111, 0x12345678)
717 yield from read(0x42, 0x12345678)
718 yield from write(0x43, 0b1111, 0x9ABCDEF0)
720 yield from read(0x43, 0x9ABCDEF0)
721 yield from write(0, 0, 0)
723 # test partial writes
725 yield from write(0x42, 0b1001, 0x78FFFF12)
728 yield from write(0x43, 0b0110, 0xFFDEABFF)
730 yield from read(0x42, 0x78345612)
731 yield from write(0, 0, 0)
733 yield from read(0x43, 0x9ADEABF0)
734 yield from write(0, 0, 0)
737 yield from write(0, 0, 0)
740 # returns the value just written
741 yield from read(0x42, 0x55AA9966)
743 # returns the old value
744 yield from read(0x42, 0x78345612)
745 yield from write(0x42, 0b1111, 0x55AA9966)
747 # after a cycle, always returns the new value
748 yield from read(0x42, 0x55AA9966)
749 yield from write(0, 0, 0)
752 yield from write(0, 0, 0)
755 yield from write(0, 0, 0)
757 sim
.add_sync_process(process
)
758 debug_file
= 'test_dual_port_regfile'
760 debug_file
+= '_transparent'
761 traces
= ['clk', 'phase',
762 {'comment': 'write port'},
763 'wr_addr_i[6:0]', 'wr_we_i[3:0]', 'wr_data_i[31:0]',
764 {'comment': 'read port'},
765 'rd_addr_i[6:0]', 'rd_data_o[31:0]',
766 {'comment': 'LVT write port'},
767 'phase', 'lvt_mem_w_addr[6:0]', 'lvt_mem_w_en[3:0]',
768 'lvt_mem_w_data[3:0]',
769 {'comment': 'LVT read port'},
770 'lvt_mem_r_addr[6:0]', 'lvt_mem_r_data[3:0]',
771 {'comment': 'backing memory'},
772 'mem0.rd_data_o[31:0]',
773 'mem1.rd_data_o[31:0]',
775 write_gtkw(debug_file
+ '.gtkw',
777 traces
, module
='top', zoom
=-22)
778 sim_writer
= sim
.write_vcd(debug_file
+ '.vcd')
782 def test_dual_port_regfile(self
):
783 with self
.subTest("non-transparent reads"):
784 self
.do_test_dual_port_regfile(False)
785 with self
.subTest("transparent reads"):
786 self
.do_test_dual_port_regfile(True)
788 def test_dual_port_regfile_proof(self
):
790 Formal proof of the 1W/1R regfile
793 # 128 x 32-bit, 8-bit granularity
794 dut
= DualPortRegfile(7, 32, 4, True)
795 m
.submodules
.dut
= dut
796 gran
= dut
.data_width
// dut
.we_width
# granularity
797 # choose a single random memory location to test
798 a_const
= AnyConst(dut
.addr_width
)
799 # choose a single byte lane to test (one-hot encoding)
800 we_mask
= Signal(dut
.we_width
)
801 # ... by first creating a random bit pattern
802 we_const
= AnyConst(dut
.we_width
)
803 # ... and zeroing all but the first non-zero bit
804 m
.d
.comb
+= we_mask
.eq(we_const
& (-we_const
))
805 # holding data register
807 # keep track of the phase, so we can remember which memory
810 m
.d
.sync
+= phase
.eq(~phase
)
811 # for some reason, simulated formal memory is not zeroed at reset
812 # ... so, remember whether we wrote it, at least once.
814 # ... and on which phase it was written
815 wrote_phase
= Signal()
816 # if our memory location and byte lane is being written,
817 # capture the data in our holding register
818 with m
.If((dut
.wr_addr_i
== a_const
)):
819 for i
in range(dut
.we_width
):
820 with m
.If(we_mask
[i
] & dut
.wr_we_i
[i
]):
821 m
.d
.sync
+= d_reg
.eq(dut
.wr_data_i
.word_select(i
, gran
))
822 m
.d
.sync
+= wrote
.eq(1)
823 m
.d
.sync
+= wrote_phase
.eq(phase
)
824 # if our memory location is being read,
825 # and the holding register has valid data,
826 # then its value must match the memory output, on the given lane
827 with m
.If(Past(dut
.rd_addr_i
) == a_const
):
829 for i
in range(dut
.we_width
):
830 rd_lane
= dut
.rd_data_o
.word_select(i
, gran
)
831 with m
.If(we_mask
[i
]):
832 m
.d
.sync
+= Assert(d_reg
== rd_lane
)
835 dut
.dbg_addr
.eq(a_const
),
836 dut
.dbg_we_mask
.eq(we_mask
),
837 dut
.dbg_data
.eq(d_reg
),
838 dut
.dbg_wrote
.eq(wrote
),
839 dut
.dbg_wrote_phase
.eq(wrote_phase
),
840 dut
.dbg_phase
.eq(phase
),
843 self
.assertFormal(m
, mode
="bmc", depth
=10)
846 if __name__
== "__main__":