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
573 self
.wr_addr_i
= Signal(addr_width
); """write port address"""
574 self
.wr_data_i
= Signal(data_width
); """write port data"""
575 self
.wr_we_i
= Signal(we_width
); """write port enable"""
576 self
.rd_addr_i
= Signal(addr_width
); """read port address"""
577 self
.rd_data_o
= Signal(data_width
); """read port data"""
579 def elaborate(self
, _
):
581 # depth and granularity
582 depth
= 1 << self
.addr_width
583 gran
= self
.data_width
// self
.we_width
584 # instantiate the two phased 1R/1W memory blocks
585 mem0
= PhasedDualPortRegfile(
586 self
.addr_width
, self
.data_width
, self
.we_width
, 0,
588 mem1
= PhasedDualPortRegfile(
589 self
.addr_width
, self
.data_width
, self
.we_width
, 1,
591 m
.submodules
.mem0
= mem0
592 m
.submodules
.mem1
= mem1
593 # instantiate the backing memory (FFRAM or LUTRAM)
594 # for the Last Value Table
595 # it should have the same number and port types of the desired
596 # memory, but just one bit per write lane
597 lvt_mem
= Memory(width
=self
.we_width
, depth
=depth
)
598 lvt_wr
= lvt_mem
.write_port(granularity
=1)
599 lvt_rd
= lvt_mem
.read_port(transparent
=self
.transparent
)
600 m
.submodules
.lvt_wr
= lvt_wr
601 m
.submodules
.lvt_rd
= lvt_rd
602 # generate and wire the phases for the phased memories
604 m
.d
.sync
+= phase
.eq(~phase
)
606 mem0
.phase
.eq(phase
),
607 mem1
.phase
.eq(phase
),
610 # wire the write ports, directly
611 mem0
.wr_addr_i
.eq(self
.wr_addr_i
),
612 mem1
.wr_addr_i
.eq(self
.wr_addr_i
),
613 mem0
.wr_we_i
.eq(self
.wr_we_i
),
614 mem1
.wr_we_i
.eq(self
.wr_we_i
),
615 mem0
.wr_data_i
.eq(self
.wr_data_i
),
616 mem1
.wr_data_i
.eq(self
.wr_data_i
),
617 # also wire the read addresses
618 mem0
.rd_addr_i
.eq(self
.rd_addr_i
),
619 mem1
.rd_addr_i
.eq(self
.rd_addr_i
),
620 # wire read and write ports to the LVT
621 lvt_wr
.addr
.eq(self
.wr_addr_i
),
622 lvt_wr
.en
.eq(self
.wr_we_i
),
623 lvt_rd
.addr
.eq(self
.rd_addr_i
),
624 # the data for the LVT is the phase on which the value was
626 lvt_wr
.data
.eq(Repl(phase
, self
.we_width
)),
628 for i
in range(self
.we_width
):
629 # select the right memory to assign to the output read port,
630 # in this byte lane, according to the LVT contents
631 m
.d
.comb
+= self
.rd_data_o
.word_select(i
, gran
).eq(
634 mem1
.rd_data_o
.word_select(i
, gran
),
635 mem0
.rd_data_o
.word_select(i
, gran
)))
636 # TODO create debug port and pass state downstream
638 mem0
.dbg_wrote
.eq(0),
639 mem1
.dbg_wrote
.eq(0),
644 class DualPortRegfileTestCase(FHDLTestCase
):
646 def do_test_dual_port_regfile(self
, transparent
):
648 Simulate some read/write/modify operations on the dual port register
651 dut
= DualPortRegfile(7, 32, 4, transparent
)
658 # compare read data with previously written data
659 # and start a new read
660 def read(rd_addr_i
, next_expected
=None):
661 nonlocal expected
, last_expected
662 if expected
is not None:
663 self
.assertEqual((yield dut
.rd_data_o
), expected
)
664 yield dut
.rd_addr_i
.eq(rd_addr_i
)
665 # account for the read latency
666 expected
= last_expected
667 last_expected
= next_expected
670 def write(wr_addr_i
, wr_we_i
, wr_data_i
):
671 yield dut
.wr_addr_i
.eq(wr_addr_i
)
672 yield dut
.wr_we_i
.eq(wr_we_i
)
673 yield dut
.wr_data_i
.eq(wr_data_i
)
676 # write a pair of values, one for each memory
678 yield from write(0x42, 0b1111, 0x87654321)
680 yield from read(0x42, 0x87654321)
681 yield from write(0x43, 0b1111, 0x0FEDCBA9)
684 yield from read(0x43, 0x0FEDCBA9)
685 yield from write(0, 0, 0)
687 # write again, but now they switch memories
689 yield from write(0x42, 0b1111, 0x12345678)
691 yield from read(0x42, 0x12345678)
692 yield from write(0x43, 0b1111, 0x9ABCDEF0)
694 yield from read(0x43, 0x9ABCDEF0)
695 yield from write(0, 0, 0)
697 # test partial writes
699 yield from write(0x42, 0b1001, 0x78FFFF12)
702 yield from write(0x43, 0b0110, 0xFFDEABFF)
704 yield from read(0x42, 0x78345612)
705 yield from write(0, 0, 0)
707 yield from read(0x43, 0x9ADEABF0)
708 yield from write(0, 0, 0)
711 yield from write(0, 0, 0)
714 # returns the value just written
715 yield from read(0x42, 0x55AA9966)
717 # returns the old value
718 yield from read(0x42, 0x78345612)
719 yield from write(0x42, 0b1111, 0x55AA9966)
721 # after a cycle, always returns the new value
722 yield from read(0x42, 0x55AA9966)
723 yield from write(0, 0, 0)
726 yield from write(0, 0, 0)
729 yield from write(0, 0, 0)
731 sim
.add_sync_process(process
)
732 debug_file
= 'test_dual_port_regfile'
734 debug_file
+= '_transparent'
735 traces
= ['clk', 'phase',
736 {'comment': 'write port'},
737 'wr_addr_i[6:0]', 'wr_we_i[3:0]', 'wr_data_i[31:0]',
738 {'comment': 'read port'},
739 'rd_addr_i[6:0]', 'rd_data_o[31:0]',
740 {'comment': 'LVT write port'},
741 'phase', 'lvt_mem_w_addr[6:0]', 'lvt_mem_w_en[3:0]',
742 'lvt_mem_w_data[3:0]',
743 {'comment': 'LVT read port'},
744 'lvt_mem_r_addr[6:0]', 'lvt_mem_r_data[3:0]',
745 {'comment': 'backing memory'},
746 'mem0.rd_data_o[31:0]',
747 'mem1.rd_data_o[31:0]',
749 write_gtkw(debug_file
+ '.gtkw',
751 traces
, module
='top', zoom
=-22)
752 sim_writer
= sim
.write_vcd(debug_file
+ '.vcd')
756 def test_dual_port_regfile(self
):
757 with self
.subTest("non-transparent reads"):
758 self
.do_test_dual_port_regfile(False)
759 with self
.subTest("transparent reads"):
760 self
.do_test_dual_port_regfile(True)
762 def test_dual_port_regfile_proof(self
):
764 Formal proof of the 1W/1R regfile
767 # 128 x 32-bit, 8-bit granularity
768 dut
= DualPortRegfile(7, 32, 4, True)
769 m
.submodules
.dut
= dut
770 gran
= dut
.data_width
// dut
.we_width
# granularity
771 # choose a single random memory location to test
772 a_const
= AnyConst(dut
.addr_width
)
773 # choose a single byte lane to test (one-hot encoding)
774 we_mask
= Signal(dut
.we_width
)
775 # ... by first creating a random bit pattern
776 we_const
= AnyConst(dut
.we_width
)
777 # ... and zeroing all but the first non-zero bit
778 m
.d
.comb
+= we_mask
.eq(we_const
& (-we_const
))
779 # holding data register
781 # for some reason, simulated formal memory is not zeroed at reset
782 # ... so, remember whether we wrote it, at least once.
784 # if our memory location and byte lane is being written,
785 # capture the data in our holding register
786 with m
.If((dut
.wr_addr_i
== a_const
)):
787 for i
in range(dut
.we_width
):
788 with m
.If(we_mask
[i
] & dut
.wr_we_i
[i
]):
789 m
.d
.sync
+= d_reg
.eq(
790 dut
.wr_data_i
[i
* gran
:i
* gran
+ gran
])
791 m
.d
.sync
+= wrote
.eq(1)
792 # if our memory location is being read,
793 # and the holding register has valid data,
794 # then its value must match the memory output, on the given lane
795 with m
.If(Past(dut
.rd_addr_i
) == a_const
):
797 for i
in range(dut
.we_width
):
798 rd_lane
= dut
.rd_data_o
.word_select(i
, gran
)
799 with m
.If(we_mask
[i
]):
800 m
.d
.sync
+= Assert(d_reg
== rd_lane
)
802 self
.assertFormal(m
, mode
="bmc", depth
=10)
805 if __name__
== "__main__":