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 lanes
= range(we_width
)
51 self
.dbg_lane
= Signal(lanes
); """debug: write lane under test"""
52 gran
= self
.data_width
// self
.we_width
53 self
.dbg_data
= Signal(gran
); """debug: data to keep in sync"""
54 self
.dbg_wrote
= Signal(); """debug: data is valid"""
56 def elaborate(self
, platform
):
59 depth
= 1 << self
.addr_width
60 gran
= 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
=gran
)
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
)
80 # the following is needed for induction, where an unreachable state
81 # (memory and holding register differ) is turned into an illegal one
82 if platform
== "formal":
83 # the debug port is an asynchronous read port, allowing direct
84 # access to a given memory location by the formal engine
85 m
.submodules
.dbgport
= dbgport
= mem
.read_port(domain
="comb")
86 # first, get the value stored in our memory location,
87 # using its debug port
88 stored
= Signal(self
.data_width
)
89 m
.d
.comb
+= dbgport
.addr
.eq(self
.dbg_addr
)
90 m
.d
.comb
+= stored
.eq(dbgport
.data
)
91 # now, ensure that the value stored in memory is always in sync
92 # with the holding register
93 with m
.If(self
.dbg_wrote
):
94 m
.d
.sync
+= Assert(self
.dbg_data
==
95 stored
.word_select(self
.dbg_lane
, gran
))
108 def create_ilang(dut
, ports
, test_name
):
109 vl
= rtlil
.convert(dut
, name
=test_name
, ports
=ports
)
110 with
open("%s.il" % test_name
, "w") as f
:
114 class SinglePortSRAMTestCase(FHDLTestCase
):
116 def test_simple_rtlil():
118 Generate a simple SRAM. Try ``read_rtlil mem_simple.il; proc; show``
119 from a yosys prompt, to see the memory primitives, and
120 ``read_rtlil mem_simple.il; synth; show`` to see it implemented as
123 dut
= SinglePortSRAM(2, 4, 2)
124 create_ilang(dut
, dut
.ports(), "mem_simple")
127 def test_blkram_rtlil():
129 Generates a bigger SRAM.
130 Try ``read_rtlil mem_blkram.il; synth_ecp5; show`` from a yosys
131 prompt, to see it implemented as block RAM
133 dut
= SinglePortSRAM(10, 16, 2)
134 create_ilang(dut
, dut
.ports(), "mem_blkram")
136 def test_sram_model(self
):
138 Simulate some read/write/modify operations on the SRAM model
140 dut
= SinglePortSRAM(7, 32, 4)
145 # 1) write 0x12_34_56_78 to address 0
147 yield dut
.d
.eq(0x12_34_56_78)
148 yield dut
.we
.eq(0b1111)
150 # 2) write 0x9A_BC_DE_F0 to address 1
152 yield dut
.d
.eq(0x9A_BC_DE_F0)
153 yield dut
.we
.eq(0b1111)
155 # ... and read value just written to address 0
156 self
.assertEqual((yield dut
.q
), 0x12_34_56_78)
157 # 3) prepare to read from address 0
159 yield dut
.we
.eq(0b0000)
162 # ... and read value just written to address 1
163 self
.assertEqual((yield dut
.q
), 0x9A_BC_DE_F0)
164 # 4) prepare to read from address 1
167 # ... and read value from address 0
168 self
.assertEqual((yield dut
.q
), 0x12_34_56_78)
169 # 5) write 0x9A and 0xDE to bytes 1 and 3, leaving
170 # bytes 0 and 2 unchanged
172 yield dut
.d
.eq(0x9A_FF_DE_FF)
173 yield dut
.we
.eq(0b1010)
175 # ... and read value from address 1
176 self
.assertEqual((yield dut
.q
), 0x9A_BC_DE_F0)
177 # 6) nothing more to do
181 # ... other than confirm that bytes 1 and 3 were modified
183 self
.assertEqual((yield dut
.q
), 0x9A_34_DE_78)
185 sim
.add_sync_process(process
)
186 traces
= ['rdport.clk', 'a[6:0]', 'we[3:0]', 'd[31:0]', 'q[31:0]']
187 write_gtkw('test_sram_model.gtkw', 'test_sram_model.vcd',
188 traces
, module
='top')
189 sim_writer
= sim
.write_vcd('test_sram_model.vcd')
193 def test_model_sram_proof(self
):
195 Formal proof of the single port SRAM model
198 # 128 x 32-bit, 8-bit granularity
199 m
.submodules
.dut
= dut
= SinglePortSRAM(7, 32, 4)
200 gran
= len(dut
.d
) // len(dut
.we
) # granularity
201 # choose a single random memory location to test
202 a_const
= AnyConst(dut
.a
.shape())
203 # choose a single byte lane to test
204 lane
= AnyConst(range(dut
.we_width
))
205 # holding data register
207 # for some reason, simulated formal memory is not zeroed at reset
208 # ... so, remember whether we wrote it, at least once.
210 # if our memory location and byte lane is being written
211 # ... capture the data in our holding register
212 with m
.If((dut
.a
== a_const
) & dut
.we
.bit_select(lane
, 1)):
213 m
.d
.sync
+= d_reg
.eq(dut
.d
.word_select(lane
, gran
))
214 m
.d
.sync
+= wrote
.eq(1)
215 # if our memory location is being read
216 # ... and the holding register has valid data
217 # ... then its value must match the memory output, on the given lane
218 with m
.If((Past(dut
.a
) == a_const
) & wrote
):
219 m
.d
.sync
+= Assert(d_reg
== dut
.q
.word_select(lane
, gran
))
221 # pass our state to the device under test, so it can ensure that
222 # its state is in sync with ours, for induction
224 dut
.dbg_addr
.eq(a_const
),
225 dut
.dbg_lane
.eq(lane
),
226 dut
.dbg_data
.eq(d_reg
),
227 dut
.dbg_wrote
.eq(wrote
),
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
258 self
.wr_addr_i
= Signal(addr_width
); """write port address"""
259 self
.wr_data_i
= Signal(data_width
); """write port data"""
260 self
.wr_we_i
= Signal(we_width
); """write port enable"""
261 self
.rd_addr_i
= Signal(addr_width
); """read port address"""
262 self
.rd_data_o
= Signal(data_width
); """read port data"""
263 self
.phase
= Signal(); """even/odd cycle indicator"""
264 # debug signals, only used in formal proofs
265 self
.dbg_addr
= Signal(addr_width
); """debug: address under test"""
266 lanes
= range(we_width
)
267 self
.dbg_lane
= Signal(lanes
); """debug: write lane under test"""
268 gran
= self
.data_width
// self
.we_width
269 self
.dbg_data
= Signal(gran
); """debug: data to keep in sync"""
270 self
.dbg_wrote
= Signal(); """debug: data is valid"""
272 def elaborate(self
, platform
):
275 # instantiate the two 1RW memory blocks
276 mem1
= SinglePortSRAM(self
.addr_width
, self
.data_width
, self
.we_width
)
277 mem2
= SinglePortSRAM(self
.addr_width
, self
.data_width
, self
.we_width
)
278 m
.submodules
.mem1
= mem1
279 m
.submodules
.mem2
= mem2
280 # wire write port to first memory, and its output to the second
281 m
.d
.comb
+= mem1
.d
.eq(self
.wr_data_i
)
282 m
.d
.comb
+= mem2
.d
.eq(mem1
.q
)
283 # holding registers for the write port of the second memory
284 last_wr_addr
= Signal(self
.addr_width
)
285 last_wr_we
= Signal(self
.we_width
)
286 # do the read and write address coincide?
287 same_read_write
= Signal()
288 with m
.If(self
.phase
== self
.write_phase
):
289 # write phase, start a write on the first memory
290 m
.d
.comb
+= mem1
.a
.eq(self
.wr_addr_i
)
291 m
.d
.comb
+= mem1
.we
.eq(self
.wr_we_i
)
292 # save write address and write select for repeating the write
293 # on the second memory, later
294 m
.d
.sync
+= last_wr_we
.eq(self
.wr_we_i
)
295 m
.d
.sync
+= last_wr_addr
.eq(self
.wr_addr_i
)
296 # start a read on the second memory
297 m
.d
.comb
+= mem2
.a
.eq(self
.rd_addr_i
)
298 # output previously read data from the first memory
299 m
.d
.comb
+= self
.rd_data_o
.eq(mem1
.q
)
301 # remember whether we are reading from the same location we are
303 m
.d
.sync
+= same_read_write
.eq(self
.rd_addr_i
== self
.wr_addr_i
)
305 # read phase, write last written data on second memory
306 m
.d
.comb
+= mem2
.a
.eq(last_wr_addr
)
307 m
.d
.comb
+= mem2
.we
.eq(last_wr_we
)
308 # start a read on the first memory
309 m
.d
.comb
+= mem1
.a
.eq(self
.rd_addr_i
)
311 with m
.If(same_read_write
):
312 # when transparent, and read and write addresses coincide,
313 # output the data just written
314 m
.d
.comb
+= self
.rd_data_o
.eq(mem1
.q
)
316 # otherwise, output previously read data
317 # from the second memory
318 m
.d
.comb
+= self
.rd_data_o
.eq(mem2
.q
)
320 # always output the read data from the second memory,
322 m
.d
.comb
+= self
.rd_data_o
.eq(mem2
.q
)
324 if platform
== "formal":
325 # pass our state to the device under test, so it can ensure that
326 # its state is in sync with ours, for induction
328 # pass the address and write lane under test to both memories
329 mem1
.dbg_addr
.eq(self
.dbg_addr
),
330 mem2
.dbg_addr
.eq(self
.dbg_addr
),
331 mem1
.dbg_lane
.eq(self
.dbg_lane
),
332 mem2
.dbg_lane
.eq(self
.dbg_lane
),
333 # the second memory copies its state from the first memory,
334 # after a cycle, so it has a one cycle delay
335 mem1
.dbg_data
.eq(self
.dbg_data
),
336 mem2
.dbg_data
.eq(Past(self
.dbg_data
)),
337 mem1
.dbg_wrote
.eq(self
.dbg_wrote
),
338 mem2
.dbg_wrote
.eq(Past(self
.dbg_wrote
)),
344 class PhasedDualPortRegfileTestCase(FHDLTestCase
):
346 def do_test_phased_dual_port_regfile(self
, write_phase
, transparent
):
348 Simulate some read/write/modify operations on the phased write memory
350 dut
= PhasedDualPortRegfile(7, 32, 4, write_phase
, transparent
)
354 # compare read data with previously written data
355 # and start a new read
356 def read(rd_addr_i
, expected
=None):
357 if expected
is not None:
358 self
.assertEqual((yield dut
.rd_data_o
), expected
)
359 yield dut
.rd_addr_i
.eq(rd_addr_i
)
361 # start a write, and set write phase
362 def write(wr_addr_i
, wr_we_i
, wr_data_i
):
363 yield dut
.wr_addr_i
.eq(wr_addr_i
)
364 yield dut
.wr_we_i
.eq(wr_we_i
)
365 yield dut
.wr_data_i
.eq(wr_data_i
)
366 yield dut
.phase
.eq(write_phase
)
368 # disable writes, and start read phase
370 yield dut
.wr_addr_i
.eq(0)
371 yield dut
.wr_we_i
.eq(0)
372 yield dut
.wr_data_i
.eq(0)
373 yield dut
.phase
.eq(~write_phase
)
375 # writes a few values on the write port, and read them back
376 # ... reads can happen every cycle
377 # ... writes, only every two cycles.
378 # since reads have a one cycle delay, the expected value on
379 # each read refers to the last read performed, not the
380 # current one, which is in progress.
383 yield from write(0x42, 0b1111, 0x12345678)
385 yield from read(0x42)
386 yield from skip_write()
388 yield from read(0x42)
389 yield from write(0x43, 0b1111, 0x9ABCDEF0)
391 yield from read(0x43, 0x12345678)
392 yield from skip_write()
394 yield from read(0x42, 0x12345678)
395 yield from write(0x43, 0b1001, 0xF0FFFF9A)
397 yield from read(0x43, 0x9ABCDEF0)
398 yield from skip_write()
400 yield from read(0x43, 0x12345678)
401 yield from write(0x42, 0b0110, 0xFF5634FF)
403 yield from read(0x42, 0xF0BCDE9A)
404 yield from skip_write()
406 yield from read(0, 0xF0BCDE9A)
407 yield from write(0, 0, 0)
409 yield from read(0, 0x12563478)
410 yield from skip_write()
412 # try reading and writing to the same location, simultaneously
413 yield from read(0x42)
414 yield from write(0x42, 0b1111, 0x55AA9966)
417 yield from read(0x42)
418 yield from skip_write()
421 # returns the value just written
422 yield from read(0, 0x55AA9966)
424 # returns the old value
425 yield from read(0, 0x12563478)
426 yield from write(0, 0, 0)
428 # after a cycle, always returns the new value
429 yield from read(0, 0x55AA9966)
430 yield from skip_write()
432 sim
.add_sync_process(process
)
433 debug_file
= f
'test_phased_dual_port_{write_phase}'
435 debug_file
+= '_transparent'
436 traces
= ['clk', 'phase',
437 'wr_addr_i[6:0]', 'wr_we_i[3:0]', 'wr_data_i[31:0]',
438 'rd_addr_i[6:0]', 'rd_data_o[31:0]']
439 write_gtkw(debug_file
+ '.gtkw',
441 traces
, module
='top', zoom
=-22)
442 sim_writer
= sim
.write_vcd(debug_file
+ '.vcd')
446 def test_phased_dual_port_regfile(self
):
447 """test both types (odd and even write ports) of phased write memory"""
448 with self
.subTest("writes happen on phase 0"):
449 self
.do_test_phased_dual_port_regfile(0, False)
450 with self
.subTest("writes happen on phase 1"):
451 self
.do_test_phased_dual_port_regfile(1, False)
452 """test again, with a transparent read port"""
453 with self
.subTest("writes happen on phase 0 (transparent reads)"):
454 self
.do_test_phased_dual_port_regfile(0, True)
455 with self
.subTest("writes happen on phase 1 (transparent reads)"):
456 self
.do_test_phased_dual_port_regfile(1, True)
458 def do_test_phased_dual_port_regfile_proof(self
, write_phase
, transparent
):
460 Formal proof of the pseudo 1W/1R regfile
463 # 128 x 32-bit, 8-bit granularity
464 dut
= PhasedDualPortRegfile(7, 32, 4, write_phase
, transparent
)
465 m
.submodules
.dut
= dut
466 gran
= dut
.data_width
// dut
.we_width
# granularity
467 # choose a single random memory location to test
468 a_const
= AnyConst(dut
.addr_width
)
469 # choose a single byte lane to test
470 lane
= AnyConst(range(dut
.we_width
))
471 # drive alternating phases
472 m
.d
.comb
+= Assume(dut
.phase
!= Past(dut
.phase
))
473 # holding data register
475 # for some reason, simulated formal memory is not zeroed at reset
476 # ... so, remember whether we wrote it, at least once.
478 # if our memory location and byte lane is being written,
479 # capture the data in our holding register
480 with m
.If((dut
.wr_addr_i
== a_const
)
481 & dut
.wr_we_i
.bit_select(lane
, 1)
482 & (dut
.phase
== dut
.write_phase
)):
483 m
.d
.sync
+= d_reg
.eq(dut
.wr_data_i
.word_select(lane
, gran
))
484 m
.d
.sync
+= wrote
.eq(1)
485 # if our memory location is being read,
486 # and the holding register has valid data,
487 # then its value must match the memory output, on the given lane
488 with m
.If(Past(dut
.rd_addr_i
) == a_const
):
491 rd_lane
= dut
.rd_data_o
.word_select(lane
, gran
)
492 m
.d
.sync
+= Assert(d_reg
== rd_lane
)
494 # with a non-transparent read port, the read value depends
495 # on whether there is a simultaneous write, or not
496 with m
.If((Past(dut
.wr_addr_i
) == a_const
)
497 & Past(dut
.phase
) == dut
.write_phase
):
498 # simultaneous write -> check against last written value
499 with m
.If(Past(wrote
)):
500 rd_lane
= dut
.rd_data_o
.word_select(lane
, gran
)
501 m
.d
.sync
+= Assert(Past(d_reg
) == rd_lane
)
503 # otherwise, check against current written value
505 rd_lane
= dut
.rd_data_o
.word_select(lane
, gran
)
506 m
.d
.sync
+= Assert(d_reg
== rd_lane
)
508 # pass our state to the device under test, so it can ensure that
509 # its state is in sync with ours, for induction
511 # address and mask under test
512 dut
.dbg_addr
.eq(a_const
),
513 dut
.dbg_lane
.eq(lane
),
514 # state of our holding register
515 dut
.dbg_data
.eq(d_reg
),
516 dut
.dbg_wrote
.eq(wrote
),
519 self
.assertFormal(m
, mode
="prove", depth
=3)
521 def test_phased_dual_port_regfile_proof(self
):
522 """test both types (odd and even write ports) of phased write memory"""
523 with self
.subTest("writes happen on phase 0"):
524 self
.do_test_phased_dual_port_regfile_proof(0, False)
525 with self
.subTest("writes happen on phase 1"):
526 self
.do_test_phased_dual_port_regfile_proof(1, False)
527 # test again, with transparent read ports
528 with self
.subTest("writes happen on phase 0 (transparent reads)"):
529 self
.do_test_phased_dual_port_regfile_proof(0, True)
530 with self
.subTest("writes happen on phase 1 (transparent reads)"):
531 self
.do_test_phased_dual_port_regfile_proof(1, True)
534 class DualPortRegfile(Elaboratable
):
536 Builds, from a pair of phased 1W/1R blocks, a true 1W/1R RAM, where both
537 read and write ports work every cycle.
538 It employs a Last Value Table, that tracks to which memory each address was
541 :param addr_width: width of the address bus
542 :param data_width: width of the data bus
543 :param we_width: number of write enable lines
544 :param transparent: whether a simultaneous read and write returns the
545 new value (True) or the old value (False)
548 def __init__(self
, addr_width
, data_width
, we_width
, transparent
=True):
549 self
.addr_width
= addr_width
550 self
.data_width
= data_width
551 self
.we_width
= we_width
552 self
.transparent
= transparent
554 self
.wr_addr_i
= Signal(addr_width
); """write port address"""
555 self
.wr_data_i
= Signal(data_width
); """write port data"""
556 self
.wr_we_i
= Signal(we_width
); """write port enable"""
557 self
.rd_addr_i
= Signal(addr_width
); """read port address"""
558 self
.rd_data_o
= Signal(data_width
); """read port data"""
559 # debug signals, only used in formal proofs
560 # address and write lane under test
561 self
.dbg_addr
= Signal(addr_width
); """debug: address under test"""
562 lanes
= range(we_width
)
563 self
.dbg_lane
= Signal(lanes
); """debug: write lane under test"""
564 # upstream state, to keep in sync with ours
565 gran
= self
.data_width
// self
.we_width
566 self
.dbg_data
= Signal(gran
); """debug: data to keep in sync"""
567 self
.dbg_wrote
= Signal(); """debug: data is valid"""
568 self
.dbg_wrote_phase
= Signal(); """debug: the phase data was written"""
569 self
.dbg_phase
= Signal(); """debug: current phase"""
571 def elaborate(self
, platform
):
573 # depth and granularity
574 depth
= 1 << self
.addr_width
575 gran
= self
.data_width
// self
.we_width
576 # instantiate the two phased 1R/1W memory blocks
577 mem0
= PhasedDualPortRegfile(
578 self
.addr_width
, self
.data_width
, self
.we_width
, 0,
580 mem1
= PhasedDualPortRegfile(
581 self
.addr_width
, self
.data_width
, self
.we_width
, 1,
583 m
.submodules
.mem0
= mem0
584 m
.submodules
.mem1
= mem1
585 # instantiate the backing memory (FFRAM or LUTRAM)
586 # for the Last Value Table
587 # it should have the same number and port types of the desired
588 # memory, but just one bit per write lane
589 lvt_mem
= Memory(width
=self
.we_width
, depth
=depth
)
590 lvt_wr
= lvt_mem
.write_port(granularity
=1)
591 lvt_rd
= lvt_mem
.read_port(transparent
=self
.transparent
)
592 m
.submodules
.lvt_wr
= lvt_wr
593 m
.submodules
.lvt_rd
= lvt_rd
594 # generate and wire the phases for the phased memories
596 m
.d
.sync
+= phase
.eq(~phase
)
598 mem0
.phase
.eq(phase
),
599 mem1
.phase
.eq(phase
),
602 # wire the write ports, directly
603 mem0
.wr_addr_i
.eq(self
.wr_addr_i
),
604 mem1
.wr_addr_i
.eq(self
.wr_addr_i
),
605 mem0
.wr_we_i
.eq(self
.wr_we_i
),
606 mem1
.wr_we_i
.eq(self
.wr_we_i
),
607 mem0
.wr_data_i
.eq(self
.wr_data_i
),
608 mem1
.wr_data_i
.eq(self
.wr_data_i
),
609 # also wire the read addresses
610 mem0
.rd_addr_i
.eq(self
.rd_addr_i
),
611 mem1
.rd_addr_i
.eq(self
.rd_addr_i
),
612 # wire read and write ports to the LVT
613 lvt_wr
.addr
.eq(self
.wr_addr_i
),
614 lvt_wr
.en
.eq(self
.wr_we_i
),
615 lvt_rd
.addr
.eq(self
.rd_addr_i
),
616 # the data for the LVT is the phase on which the value was
618 lvt_wr
.data
.eq(Repl(phase
, self
.we_width
)),
620 for i
in range(self
.we_width
):
621 # select the right memory to assign to the output read port,
622 # in this byte lane, according to the LVT contents
623 m
.d
.comb
+= self
.rd_data_o
.word_select(i
, gran
).eq(
626 mem1
.rd_data_o
.word_select(i
, gran
),
627 mem0
.rd_data_o
.word_select(i
, gran
)))
629 if platform
== "formal":
630 # pass upstream state to the memories, so they can ensure that
631 # their state are in sync with upstream, for induction
633 # address and write lane under test
634 mem0
.dbg_addr
.eq(self
.dbg_addr
),
635 mem1
.dbg_addr
.eq(self
.dbg_addr
),
636 mem0
.dbg_lane
.eq(self
.dbg_lane
),
637 mem1
.dbg_lane
.eq(self
.dbg_lane
),
639 mem0
.dbg_data
.eq(self
.dbg_data
),
640 mem1
.dbg_data
.eq(self
.dbg_data
),
641 # the memory, on which the write ends up, depends on which
642 # phase it was written
643 mem0
.dbg_wrote
.eq(self
.dbg_wrote
& ~self
.dbg_wrote_phase
),
644 mem1
.dbg_wrote
.eq(self
.dbg_wrote
& self
.dbg_wrote_phase
),
646 # sync phase to upstream
647 m
.d
.comb
+= Assert(self
.dbg_phase
== phase
)
648 # this debug port for the LVT is an asynchronous read port,
649 # allowing direct access to a given memory location
650 # by the formal engine
651 m
.submodules
.dbgport
= dbgport
= lvt_mem
.read_port(domain
='comb')
652 # first, get the value stored in our memory location,
653 stored
= Signal(self
.we_width
)
654 m
.d
.comb
+= dbgport
.addr
.eq(self
.dbg_addr
)
655 m
.d
.comb
+= stored
.eq(dbgport
.data
)
656 # now, ensure that the value stored in memory is always in sync
657 # with the expected value (which memory the value was written to)
658 with m
.If(self
.dbg_wrote
):
659 m
.d
.comb
+= Assert(stored
.bit_select(self
.dbg_lane
, 1)
660 == self
.dbg_wrote_phase
)
664 class DualPortRegfileTestCase(FHDLTestCase
):
666 def do_test_dual_port_regfile(self
, transparent
):
668 Simulate some read/write/modify operations on the dual port register
671 dut
= DualPortRegfile(7, 32, 4, transparent
)
678 # compare read data with previously written data
679 # and start a new read
680 def read(rd_addr_i
, next_expected
=None):
681 nonlocal expected
, last_expected
682 if expected
is not None:
683 self
.assertEqual((yield dut
.rd_data_o
), expected
)
684 yield dut
.rd_addr_i
.eq(rd_addr_i
)
685 # account for the read latency
686 expected
= last_expected
687 last_expected
= next_expected
690 def write(wr_addr_i
, wr_we_i
, wr_data_i
):
691 yield dut
.wr_addr_i
.eq(wr_addr_i
)
692 yield dut
.wr_we_i
.eq(wr_we_i
)
693 yield dut
.wr_data_i
.eq(wr_data_i
)
696 # write a pair of values, one for each memory
698 yield from write(0x42, 0b1111, 0x87654321)
700 yield from read(0x42, 0x87654321)
701 yield from write(0x43, 0b1111, 0x0FEDCBA9)
704 yield from read(0x43, 0x0FEDCBA9)
705 yield from write(0, 0, 0)
707 # write again, but now they switch memories
709 yield from write(0x42, 0b1111, 0x12345678)
711 yield from read(0x42, 0x12345678)
712 yield from write(0x43, 0b1111, 0x9ABCDEF0)
714 yield from read(0x43, 0x9ABCDEF0)
715 yield from write(0, 0, 0)
717 # test partial writes
719 yield from write(0x42, 0b1001, 0x78FFFF12)
722 yield from write(0x43, 0b0110, 0xFFDEABFF)
724 yield from read(0x42, 0x78345612)
725 yield from write(0, 0, 0)
727 yield from read(0x43, 0x9ADEABF0)
728 yield from write(0, 0, 0)
731 yield from write(0, 0, 0)
734 # returns the value just written
735 yield from read(0x42, 0x55AA9966)
737 # returns the old value
738 yield from read(0x42, 0x78345612)
739 yield from write(0x42, 0b1111, 0x55AA9966)
741 # after a cycle, always returns the new value
742 yield from read(0x42, 0x55AA9966)
743 yield from write(0, 0, 0)
746 yield from write(0, 0, 0)
749 yield from write(0, 0, 0)
751 sim
.add_sync_process(process
)
752 debug_file
= 'test_dual_port_regfile'
754 debug_file
+= '_transparent'
755 traces
= ['clk', 'phase',
756 {'comment': 'write port'},
757 'wr_addr_i[6:0]', 'wr_we_i[3:0]', 'wr_data_i[31:0]',
758 {'comment': 'read port'},
759 'rd_addr_i[6:0]', 'rd_data_o[31:0]',
760 {'comment': 'LVT write port'},
761 'phase', 'lvt_mem_w_addr[6:0]', 'lvt_mem_w_en[3:0]',
762 'lvt_mem_w_data[3:0]',
763 {'comment': 'LVT read port'},
764 'lvt_mem_r_addr[6:0]', 'lvt_mem_r_data[3:0]',
765 {'comment': 'backing memory'},
766 'mem0.rd_data_o[31:0]',
767 'mem1.rd_data_o[31:0]',
769 write_gtkw(debug_file
+ '.gtkw',
771 traces
, module
='top', zoom
=-22)
772 sim_writer
= sim
.write_vcd(debug_file
+ '.vcd')
776 def test_dual_port_regfile(self
):
777 with self
.subTest("non-transparent reads"):
778 self
.do_test_dual_port_regfile(False)
779 with self
.subTest("transparent reads"):
780 self
.do_test_dual_port_regfile(True)
782 def test_dual_port_regfile_proof(self
):
784 Formal proof of the 1W/1R regfile
787 # 128 x 32-bit, 8-bit granularity
788 dut
= DualPortRegfile(7, 32, 4, True)
789 m
.submodules
.dut
= dut
790 gran
= dut
.data_width
// dut
.we_width
# granularity
791 # choose a single random memory location to test
792 a_const
= AnyConst(dut
.addr_width
)
793 # choose a single byte lane to test
794 lane
= AnyConst(range(dut
.we_width
))
795 # holding data register
797 # keep track of the phase, so we can remember which memory
800 m
.d
.sync
+= phase
.eq(~phase
)
801 # for some reason, simulated formal memory is not zeroed at reset
802 # ... so, remember whether we wrote it, at least once.
804 # ... and on which phase it was written
805 wrote_phase
= Signal()
806 # if our memory location and byte lane is being written,
807 # capture the data in our holding register
808 with m
.If((dut
.wr_addr_i
== a_const
)
809 & dut
.wr_we_i
.bit_select(lane
, 1)):
810 m
.d
.sync
+= d_reg
.eq(dut
.wr_data_i
.word_select(lane
, gran
))
811 m
.d
.sync
+= wrote
.eq(1)
812 m
.d
.sync
+= wrote_phase
.eq(phase
)
813 # if our memory location is being read,
814 # and the holding register has valid data,
815 # then its value must match the memory output, on the given lane
816 with m
.If(Past(dut
.rd_addr_i
) == a_const
):
818 rd_lane
= dut
.rd_data_o
.word_select(lane
, gran
)
819 m
.d
.sync
+= Assert(d_reg
== rd_lane
)
822 dut
.dbg_addr
.eq(a_const
),
823 dut
.dbg_lane
.eq(lane
),
824 dut
.dbg_data
.eq(d_reg
),
825 dut
.dbg_wrote
.eq(wrote
),
826 dut
.dbg_wrote_phase
.eq(wrote_phase
),
827 dut
.dbg_phase
.eq(phase
),
830 self
.assertFormal(m
, mode
="prove", depth
=3)
833 if __name__
== "__main__":