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
)),
354 class PhasedDualPortRegfileTestCase(FHDLTestCase
):
356 def do_test_phased_dual_port_regfile(self
, write_phase
, transparent
):
358 Simulate some read/write/modify operations on the phased write memory
360 dut
= PhasedDualPortRegfile(7, 32, 4, write_phase
, transparent
)
364 # compare read data with previously written data
365 # and start a new read
366 def read(rd_addr_i
, expected
=None):
367 if expected
is not None:
368 self
.assertEqual((yield dut
.rd_data_o
), expected
)
369 yield dut
.rd_addr_i
.eq(rd_addr_i
)
371 # start a write, and set write phase
372 def write(wr_addr_i
, wr_we_i
, wr_data_i
):
373 yield dut
.wr_addr_i
.eq(wr_addr_i
)
374 yield dut
.wr_we_i
.eq(wr_we_i
)
375 yield dut
.wr_data_i
.eq(wr_data_i
)
376 yield dut
.phase
.eq(write_phase
)
378 # disable writes, and start read phase
380 yield dut
.wr_addr_i
.eq(0)
381 yield dut
.wr_we_i
.eq(0)
382 yield dut
.wr_data_i
.eq(0)
383 yield dut
.phase
.eq(~write_phase
)
385 # writes a few values on the write port, and read them back
386 # ... reads can happen every cycle
387 # ... writes, only every two cycles.
388 # since reads have a one cycle delay, the expected value on
389 # each read refers to the last read performed, not the
390 # current one, which is in progress.
393 yield from write(0x42, 0b1111, 0x12345678)
395 yield from read(0x42)
396 yield from skip_write()
398 yield from read(0x42)
399 yield from write(0x43, 0b1111, 0x9ABCDEF0)
401 yield from read(0x43, 0x12345678)
402 yield from skip_write()
404 yield from read(0x42, 0x12345678)
405 yield from write(0x43, 0b1001, 0xF0FFFF9A)
407 yield from read(0x43, 0x9ABCDEF0)
408 yield from skip_write()
410 yield from read(0x43, 0x12345678)
411 yield from write(0x42, 0b0110, 0xFF5634FF)
413 yield from read(0x42, 0xF0BCDE9A)
414 yield from skip_write()
416 yield from read(0, 0xF0BCDE9A)
417 yield from write(0, 0, 0)
419 yield from read(0, 0x12563478)
420 yield from skip_write()
422 # try reading and writing to the same location, simultaneously
423 yield from read(0x42)
424 yield from write(0x42, 0b1111, 0x55AA9966)
427 yield from read(0x42)
428 yield from skip_write()
431 # returns the value just written
432 yield from read(0, 0x55AA9966)
434 # returns the old value
435 yield from read(0, 0x12563478)
436 yield from write(0, 0, 0)
438 # after a cycle, always returns the new value
439 yield from read(0, 0x55AA9966)
440 yield from skip_write()
442 sim
.add_sync_process(process
)
443 debug_file
= f
'test_phased_dual_port_{write_phase}'
445 debug_file
+= '_transparent'
446 traces
= ['clk', 'phase',
447 'wr_addr_i[6:0]', 'wr_we_i[3:0]', 'wr_data_i[31:0]',
448 'rd_addr_i[6:0]', 'rd_data_o[31:0]']
449 write_gtkw(debug_file
+ '.gtkw',
451 traces
, module
='top', zoom
=-22)
452 sim_writer
= sim
.write_vcd(debug_file
+ '.vcd')
456 def test_phased_dual_port_regfile(self
):
457 """test both types (odd and even write ports) of phased write memory"""
458 with self
.subTest("writes happen on phase 0"):
459 self
.do_test_phased_dual_port_regfile(0, False)
460 with self
.subTest("writes happen on phase 1"):
461 self
.do_test_phased_dual_port_regfile(1, False)
462 """test again, with a transparent read port"""
463 with self
.subTest("writes happen on phase 0 (transparent reads)"):
464 self
.do_test_phased_dual_port_regfile(0, True)
465 with self
.subTest("writes happen on phase 1 (transparent reads)"):
466 self
.do_test_phased_dual_port_regfile(1, True)
468 def do_test_phased_dual_port_regfile_proof(self
, write_phase
, transparent
):
470 Formal proof of the pseudo 1W/1R regfile
473 # 128 x 32-bit, 8-bit granularity
474 dut
= PhasedDualPortRegfile(7, 32, 4, write_phase
, transparent
)
475 m
.submodules
.dut
= dut
476 gran
= dut
.data_width
// dut
.we_width
# granularity
477 # choose a single random memory location to test
478 a_const
= AnyConst(dut
.addr_width
)
479 # choose a single byte lane to test
480 lane
= AnyConst(range(dut
.we_width
))
481 # drive alternating phases
482 m
.d
.comb
+= Assume(dut
.phase
!= Past(dut
.phase
))
483 # holding data register
485 # for some reason, simulated formal memory is not zeroed at reset
486 # ... so, remember whether we wrote it, at least once.
488 # if our memory location and byte lane is being written,
489 # capture the data in our holding register
490 with m
.If((dut
.wr_addr_i
== a_const
)
491 & dut
.wr_we_i
.bit_select(lane
, 1)
492 & (dut
.phase
== dut
.write_phase
)):
493 m
.d
.sync
+= d_reg
.eq(dut
.wr_data_i
.word_select(lane
, gran
))
494 m
.d
.sync
+= wrote
.eq(1)
495 # if our memory location is being read,
496 # and the holding register has valid data,
497 # then its value must match the memory output, on the given lane
498 with m
.If(Past(dut
.rd_addr_i
) == a_const
):
501 rd_lane
= dut
.rd_data_o
.word_select(lane
, gran
)
502 m
.d
.sync
+= Assert(d_reg
== rd_lane
)
504 # with a non-transparent read port, the read value depends
505 # on whether there is a simultaneous write, or not
506 with m
.If((Past(dut
.wr_addr_i
) == a_const
)
507 & Past(dut
.phase
) == dut
.write_phase
):
508 # simultaneous write -> check against last written value
509 with m
.If(Past(wrote
)):
510 rd_lane
= dut
.rd_data_o
.word_select(lane
, gran
)
511 m
.d
.sync
+= Assert(Past(d_reg
) == rd_lane
)
513 # otherwise, check against current written value
515 rd_lane
= dut
.rd_data_o
.word_select(lane
, gran
)
516 m
.d
.sync
+= Assert(d_reg
== rd_lane
)
518 # pass our state to the device under test, so it can ensure that
519 # its state is in sync with ours, for induction
521 # address and mask under test
522 dut
.dbg_addr
.eq(a_const
),
523 dut
.dbg_lane
.eq(lane
),
524 # state of our holding register
525 dut
.dbg_data
.eq(d_reg
),
526 dut
.dbg_wrote
.eq(wrote
),
529 self
.assertFormal(m
, mode
="prove", depth
=3)
531 def test_phased_dual_port_regfile_proof(self
):
532 """test both types (odd and even write ports) of phased write memory"""
533 with self
.subTest("writes happen on phase 0"):
534 self
.do_test_phased_dual_port_regfile_proof(0, False)
535 with self
.subTest("writes happen on phase 1"):
536 self
.do_test_phased_dual_port_regfile_proof(1, False)
537 # test again, with transparent read ports
538 with self
.subTest("writes happen on phase 0 (transparent reads)"):
539 self
.do_test_phased_dual_port_regfile_proof(0, True)
540 with self
.subTest("writes happen on phase 1 (transparent reads)"):
541 self
.do_test_phased_dual_port_regfile_proof(1, True)
544 class DualPortRegfile(Elaboratable
):
546 Builds, from a pair of phased 1W/1R blocks, a true 1W/1R RAM, where both
547 read and write ports work every cycle.
548 It employs a Last Value Table, that tracks to which memory each address was
551 :param addr_width: width of the address bus
552 :param data_width: width of the data bus
553 :param we_width: number of write enable lines
554 :param transparent: whether a simultaneous read and write returns the
555 new value (True) or the old value (False)
558 def __init__(self
, addr_width
, data_width
, we_width
, transparent
=True):
559 self
.addr_width
= addr_width
560 self
.data_width
= data_width
561 self
.we_width
= we_width
562 self
.transparent
= transparent
564 self
.wr_addr_i
= Signal(addr_width
); """write port address"""
565 self
.wr_data_i
= Signal(data_width
); """write port data"""
566 self
.wr_we_i
= Signal(we_width
); """write port enable"""
567 self
.rd_addr_i
= Signal(addr_width
); """read port address"""
568 self
.rd_data_o
= Signal(data_width
); """read port data"""
569 # debug signals, only used in formal proofs
570 # address and write lane under test
571 self
.dbg_addr
= Signal(addr_width
); """debug: address under test"""
572 lanes
= range(we_width
)
573 self
.dbg_lane
= Signal(lanes
); """debug: write lane under test"""
574 # upstream state, to keep in sync with ours
575 gran
= self
.data_width
// self
.we_width
576 self
.dbg_data
= Signal(gran
); """debug: data to keep in sync"""
577 self
.dbg_wrote
= Signal(); """debug: data is valid"""
578 self
.dbg_wrote_phase
= Signal(); """debug: the phase data was written"""
579 self
.dbg_phase
= Signal(); """debug: current phase"""
581 def elaborate(self
, platform
):
583 # depth and granularity
584 depth
= 1 << self
.addr_width
585 gran
= self
.data_width
// self
.we_width
586 # instantiate the two phased 1R/1W memory blocks
587 mem0
= PhasedDualPortRegfile(
588 self
.addr_width
, self
.data_width
, self
.we_width
, 0,
590 mem1
= PhasedDualPortRegfile(
591 self
.addr_width
, self
.data_width
, self
.we_width
, 1,
593 m
.submodules
.mem0
= mem0
594 m
.submodules
.mem1
= mem1
595 # instantiate the backing memory (FFRAM or LUTRAM)
596 # for the Last Value Table
597 # it should have the same number and port types of the desired
598 # memory, but just one bit per write lane
599 lvt_mem
= Memory(width
=self
.we_width
, depth
=depth
)
600 lvt_wr
= lvt_mem
.write_port(granularity
=1)
601 lvt_rd
= lvt_mem
.read_port(transparent
=self
.transparent
)
602 m
.submodules
.lvt_wr
= lvt_wr
603 m
.submodules
.lvt_rd
= lvt_rd
604 # generate and wire the phases for the phased memories
606 m
.d
.sync
+= phase
.eq(~phase
)
608 mem0
.phase
.eq(phase
),
609 mem1
.phase
.eq(phase
),
612 # wire the write ports, directly
613 mem0
.wr_addr_i
.eq(self
.wr_addr_i
),
614 mem1
.wr_addr_i
.eq(self
.wr_addr_i
),
615 mem0
.wr_we_i
.eq(self
.wr_we_i
),
616 mem1
.wr_we_i
.eq(self
.wr_we_i
),
617 mem0
.wr_data_i
.eq(self
.wr_data_i
),
618 mem1
.wr_data_i
.eq(self
.wr_data_i
),
619 # also wire the read addresses
620 mem0
.rd_addr_i
.eq(self
.rd_addr_i
),
621 mem1
.rd_addr_i
.eq(self
.rd_addr_i
),
622 # wire read and write ports to the LVT
623 lvt_wr
.addr
.eq(self
.wr_addr_i
),
624 lvt_wr
.en
.eq(self
.wr_we_i
),
625 lvt_rd
.addr
.eq(self
.rd_addr_i
),
626 # the data for the LVT is the phase on which the value was
628 lvt_wr
.data
.eq(Repl(phase
, self
.we_width
)),
630 for i
in range(self
.we_width
):
631 # select the right memory to assign to the output read port,
632 # in this byte lane, according to the LVT contents
633 m
.d
.comb
+= self
.rd_data_o
.word_select(i
, gran
).eq(
636 mem1
.rd_data_o
.word_select(i
, gran
),
637 mem0
.rd_data_o
.word_select(i
, gran
)))
639 if platform
== "formal":
640 # pass upstream state to the memories, so they can ensure that
641 # their state are in sync with upstream, for induction
643 # address and write lane under test
644 mem0
.dbg_addr
.eq(self
.dbg_addr
),
645 mem1
.dbg_addr
.eq(self
.dbg_addr
),
646 mem0
.dbg_lane
.eq(self
.dbg_lane
),
647 mem1
.dbg_lane
.eq(self
.dbg_lane
),
649 mem0
.dbg_data
.eq(self
.dbg_data
),
650 mem1
.dbg_data
.eq(self
.dbg_data
),
651 # the memory, on which the write ends up, depends on which
652 # phase it was written
653 mem0
.dbg_wrote
.eq(self
.dbg_wrote
& ~self
.dbg_wrote_phase
),
654 mem1
.dbg_wrote
.eq(self
.dbg_wrote
& self
.dbg_wrote_phase
),
656 # sync phase to upstream
657 m
.d
.comb
+= Assert(self
.dbg_phase
== phase
)
658 # this debug port for the LVT is an asynchronous read port,
659 # allowing direct access to a given memory location
660 # by the formal engine
661 m
.submodules
.dbgport
= dbgport
= lvt_mem
.read_port(domain
='comb')
662 # first, get the value stored in our memory location,
663 stored
= Signal(self
.we_width
)
664 m
.d
.comb
+= dbgport
.addr
.eq(self
.dbg_addr
)
665 m
.d
.comb
+= stored
.eq(dbgport
.data
)
666 # now, ensure that the value stored in memory is always in sync
667 # with the expected value (which memory the value was written to)
668 with m
.If(self
.dbg_wrote
):
669 m
.d
.comb
+= Assert(stored
.bit_select(self
.dbg_lane
, 1)
670 == self
.dbg_wrote_phase
)
683 class DualPortRegfileTestCase(FHDLTestCase
):
685 def do_test_dual_port_regfile(self
, transparent
):
687 Simulate some read/write/modify operations on the dual port register
690 dut
= DualPortRegfile(7, 32, 4, transparent
)
697 # compare read data with previously written data
698 # and start a new read
699 def read(rd_addr_i
, next_expected
=None):
700 nonlocal expected
, last_expected
701 if expected
is not None:
702 self
.assertEqual((yield dut
.rd_data_o
), expected
)
703 yield dut
.rd_addr_i
.eq(rd_addr_i
)
704 # account for the read latency
705 expected
= last_expected
706 last_expected
= next_expected
709 def write(wr_addr_i
, wr_we_i
, wr_data_i
):
710 yield dut
.wr_addr_i
.eq(wr_addr_i
)
711 yield dut
.wr_we_i
.eq(wr_we_i
)
712 yield dut
.wr_data_i
.eq(wr_data_i
)
715 # write a pair of values, one for each memory
717 yield from write(0x42, 0b1111, 0x87654321)
719 yield from read(0x42, 0x87654321)
720 yield from write(0x43, 0b1111, 0x0FEDCBA9)
723 yield from read(0x43, 0x0FEDCBA9)
724 yield from write(0, 0, 0)
726 # write again, but now they switch memories
728 yield from write(0x42, 0b1111, 0x12345678)
730 yield from read(0x42, 0x12345678)
731 yield from write(0x43, 0b1111, 0x9ABCDEF0)
733 yield from read(0x43, 0x9ABCDEF0)
734 yield from write(0, 0, 0)
736 # test partial writes
738 yield from write(0x42, 0b1001, 0x78FFFF12)
741 yield from write(0x43, 0b0110, 0xFFDEABFF)
743 yield from read(0x42, 0x78345612)
744 yield from write(0, 0, 0)
746 yield from read(0x43, 0x9ADEABF0)
747 yield from write(0, 0, 0)
750 yield from write(0, 0, 0)
753 # returns the value just written
754 yield from read(0x42, 0x55AA9966)
756 # returns the old value
757 yield from read(0x42, 0x78345612)
758 yield from write(0x42, 0b1111, 0x55AA9966)
760 # after a cycle, always returns the new value
761 yield from read(0x42, 0x55AA9966)
762 yield from write(0, 0, 0)
765 yield from write(0, 0, 0)
768 yield from write(0, 0, 0)
770 sim
.add_sync_process(process
)
771 debug_file
= 'test_dual_port_regfile'
773 debug_file
+= '_transparent'
774 traces
= ['clk', 'phase',
775 {'comment': 'write port'},
776 'wr_addr_i[6:0]', 'wr_we_i[3:0]', 'wr_data_i[31:0]',
777 {'comment': 'read port'},
778 'rd_addr_i[6:0]', 'rd_data_o[31:0]',
779 {'comment': 'LVT write port'},
780 'phase', 'lvt_mem_w_addr[6:0]', 'lvt_mem_w_en[3:0]',
781 'lvt_mem_w_data[3:0]',
782 {'comment': 'LVT read port'},
783 'lvt_mem_r_addr[6:0]', 'lvt_mem_r_data[3:0]',
784 {'comment': 'backing memory'},
785 'mem0.rd_data_o[31:0]',
786 'mem1.rd_data_o[31:0]',
788 write_gtkw(debug_file
+ '.gtkw',
790 traces
, module
='top', zoom
=-22)
791 sim_writer
= sim
.write_vcd(debug_file
+ '.vcd')
795 def test_dual_port_regfile(self
):
796 with self
.subTest("non-transparent reads"):
797 self
.do_test_dual_port_regfile(False)
798 with self
.subTest("transparent reads"):
799 self
.do_test_dual_port_regfile(True)
801 def test_dual_port_regfile_proof(self
):
803 Formal proof of the 1W/1R regfile
806 # 128 x 32-bit, 8-bit granularity
807 dut
= DualPortRegfile(7, 32, 4, True)
808 m
.submodules
.dut
= dut
809 gran
= dut
.data_width
// dut
.we_width
# granularity
810 # choose a single random memory location to test
811 a_const
= AnyConst(dut
.addr_width
)
812 # choose a single byte lane to test
813 lane
= AnyConst(range(dut
.we_width
))
814 # holding data register
816 # keep track of the phase, so we can remember which memory
819 m
.d
.sync
+= phase
.eq(~phase
)
820 # for some reason, simulated formal memory is not zeroed at reset
821 # ... so, remember whether we wrote it, at least once.
823 # ... and on which phase it was written
824 wrote_phase
= Signal()
825 # if our memory location and byte lane is being written,
826 # capture the data in our holding register
827 with m
.If((dut
.wr_addr_i
== a_const
)
828 & dut
.wr_we_i
.bit_select(lane
, 1)):
829 m
.d
.sync
+= d_reg
.eq(dut
.wr_data_i
.word_select(lane
, gran
))
830 m
.d
.sync
+= wrote
.eq(1)
831 m
.d
.sync
+= wrote_phase
.eq(phase
)
832 # if our memory location is being read,
833 # and the holding register has valid data,
834 # then its value must match the memory output, on the given lane
835 with m
.If(Past(dut
.rd_addr_i
) == a_const
):
837 rd_lane
= dut
.rd_data_o
.word_select(lane
, gran
)
838 m
.d
.sync
+= Assert(d_reg
== rd_lane
)
841 dut
.dbg_addr
.eq(a_const
),
842 dut
.dbg_lane
.eq(lane
),
843 dut
.dbg_data
.eq(d_reg
),
844 dut
.dbg_wrote
.eq(wrote
),
845 dut
.dbg_wrote_phase
.eq(wrote_phase
),
846 dut
.dbg_phase
.eq(phase
),
849 self
.assertFormal(m
, mode
="prove", depth
=3)
852 if __name__
== "__main__":