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
43 self
.d
= Signal(data_width
); """ write data"""
44 self
.q
= Signal(data_width
); """read data"""
45 self
.a
= Signal(addr_width
); """ read/write address"""
46 self
.we
= Signal(we_width
); """write enable"""
47 self
.dbg_a
= Signal(addr_width
); """debug read port address"""
48 self
.dbg_q
= Signal(data_width
); """debug read port data"""
50 def elaborate(self
, _
):
53 depth
= 1 << self
.addr_width
54 granularity
= self
.data_width
// self
.we_width
55 mem
= Memory(width
=self
.data_width
, depth
=depth
)
56 # create read and write ports
57 # By connecting the same address to both ports, they behave, in fact,
58 # as a single, "half-duplex" port.
59 # The transparent attribute means that, on a write, we read the new
60 # value, on the next cycle
61 # Note that nmigen memories have a one cycle delay, for reads,
63 m
.submodules
.rdport
= rdport
= mem
.read_port(transparent
=True)
64 m
.submodules
.wrport
= wrport
= mem
.write_port(granularity
=granularity
)
65 # duplicate the address to both ports
66 m
.d
.comb
+= wrport
.addr
.eq(self
.a
)
67 m
.d
.comb
+= rdport
.addr
.eq(self
.a
)
69 m
.d
.comb
+= wrport
.en
.eq(self
.we
)
71 m
.d
.comb
+= wrport
.data
.eq(self
.d
)
72 m
.d
.comb
+= self
.q
.eq(rdport
.data
)
73 # the debug port is an asynchronous read port, allowing direct access
74 # to a given memory location by the formal engine
75 m
.submodules
.dbgport
= dbgport
= mem
.read_port(domain
="comb")
76 m
.d
.comb
+= dbgport
.addr
.eq(self
.dbg_a
)
77 m
.d
.comb
+= self
.dbg_q
.eq(dbgport
.data
)
89 def create_ilang(dut
, ports
, test_name
):
90 vl
= rtlil
.convert(dut
, name
=test_name
, ports
=ports
)
91 with
open("%s.il" % test_name
, "w") as f
:
95 class SinglePortSRAMTestCase(FHDLTestCase
):
97 def test_simple_rtlil():
99 Generate a simple SRAM. Try ``read_rtlil mem_simple.il; proc; show``
100 from a yosys prompt, to see the memory primitives, and
101 ``read_rtlil mem_simple.il; synth; show`` to see it implemented as
104 dut
= SinglePortSRAM(2, 4, 2)
105 create_ilang(dut
, dut
.ports(), "mem_simple")
108 def test_blkram_rtlil():
110 Generates a bigger SRAM.
111 Try ``read_rtlil mem_blkram.il; synth_ecp5; show`` from a yosys
112 prompt, to see it implemented as block RAM
114 dut
= SinglePortSRAM(10, 16, 2)
115 create_ilang(dut
, dut
.ports(), "mem_blkram")
117 def test_sram_model(self
):
119 Simulate some read/write/modify operations on the SRAM model
121 dut
= SinglePortSRAM(7, 32, 4)
126 # 1) write 0x12_34_56_78 to address 0
128 yield dut
.d
.eq(0x12_34_56_78)
129 yield dut
.we
.eq(0b1111)
131 # 2) write 0x9A_BC_DE_F0 to address 1
133 yield dut
.d
.eq(0x9A_BC_DE_F0)
134 yield dut
.we
.eq(0b1111)
136 # ... and read value just written to address 0
137 self
.assertEqual((yield dut
.q
), 0x12_34_56_78)
138 # 3) prepare to read from address 0
140 yield dut
.we
.eq(0b0000)
143 # ... and read value just written to address 1
144 self
.assertEqual((yield dut
.q
), 0x9A_BC_DE_F0)
145 # 4) prepare to read from address 1
148 # ... and read value from address 0
149 self
.assertEqual((yield dut
.q
), 0x12_34_56_78)
150 # 5) write 0x9A and 0xDE to bytes 1 and 3, leaving
151 # bytes 0 and 2 unchanged
153 yield dut
.d
.eq(0x9A_FF_DE_FF)
154 yield dut
.we
.eq(0b1010)
156 # ... and read value from address 1
157 self
.assertEqual((yield dut
.q
), 0x9A_BC_DE_F0)
158 # 6) nothing more to do
162 # ... other than confirm that bytes 1 and 3 were modified
164 self
.assertEqual((yield dut
.q
), 0x9A_34_DE_78)
166 sim
.add_sync_process(process
)
167 traces
= ['rdport.clk', 'a[6:0]', 'we[3:0]', 'd[31:0]', 'q[31:0]']
168 write_gtkw('test_sram_model.gtkw', 'test_sram_model.vcd',
169 traces
, module
='top')
170 sim_writer
= sim
.write_vcd('test_sram_model.vcd')
174 def test_model_sram_proof(self
):
176 Formal proof of the single port SRAM model
179 # 128 x 32-bit, 8-bit granularity
180 m
.submodules
.dut
= dut
= SinglePortSRAM(7, 32, 4)
181 gran
= len(dut
.d
) // len(dut
.we
) # granularity
182 # choose a single random memory location to test
183 a_const
= AnyConst(dut
.a
.shape())
184 # choose a single byte lane to test (one-hot encoding)
185 we_mask
= Signal
.like(dut
.we
)
186 # ... by first creating a random bit pattern
187 we_const
= AnyConst(dut
.we
.shape())
188 # ... and zeroing all but the first non-zero bit
189 m
.d
.comb
+= we_mask
.eq(we_const
& (-we_const
))
190 # holding data register
192 # for some reason, simulated formal memory is not zeroed at reset
193 # ... so, remember whether we wrote it, at least once.
195 # if our memory location and byte lane is being written
196 # ... capture the data in our holding register
197 with m
.If(dut
.a
== a_const
):
198 for i
in range(len(dut
.we
)):
199 with m
.If(we_mask
[i
] & dut
.we
[i
]):
200 m
.d
.sync
+= d_reg
.eq(dut
.d
[i
*gran
:i
*gran
+gran
])
201 m
.d
.sync
+= wrote
.eq(1)
202 # if our memory location is being read
203 # ... and the holding register has valid data
204 # ... then its value must match the memory output, on the given lane
205 with m
.If((Past(dut
.a
) == a_const
) & wrote
):
206 for i
in range(len(dut
.we
)):
207 with m
.If(we_mask
[i
]):
208 m
.d
.sync
+= Assert(d_reg
== dut
.q
[i
*gran
:i
*gran
+gran
])
210 # the following is needed for induction, where an unreachable state
211 # (memory and holding register differ) is turned into an illegal one
212 # first, get the value stored in our memory location, using its debug
214 stored
= Signal
.like(dut
.q
)
215 m
.d
.comb
+= dut
.dbg_a
.eq(a_const
)
216 m
.d
.comb
+= stored
.eq(dut
.dbg_q
)
217 # now, ensure that the value stored in memory is always in sync
218 # with the holding register
220 for i
in range(len(dut
.we
)):
221 with m
.If(we_mask
[i
]):
222 m
.d
.sync
+= Assert(d_reg
== stored
[i
*gran
:i
*gran
+gran
])
224 self
.assertFormal(m
, mode
="prove", depth
=2)
227 class PhasedDualPortRegfile(Elaboratable
):
229 Builds, from a pair of 1RW blocks, a pseudo 1W/1R RAM, where the
230 read port works every cycle, but the write port is only available on
231 either even (1eW/1R) or odd (1oW/1R) cycles.
233 :param addr_width: width of the address bus
234 :param data_width: width of the data bus
235 :param we_width: number of write enable lines
236 :param write_phase: indicates on which phase the write port will
238 :param transparent: whether a simultaneous read and write returns the
239 new value (True) or the old value (False)
241 .. note:: The debug read port is meant only to assist in formal proofs!
244 def __init__(self
, addr_width
, data_width
, we_width
, write_phase
,
246 self
.addr_width
= addr_width
247 self
.data_width
= data_width
248 self
.we_width
= we_width
249 self
.write_phase
= write_phase
250 self
.transparent
= transparent
252 self
.wr_addr_i
= Signal(addr_width
); """write port address"""
253 self
.wr_data_i
= Signal(data_width
); """write port data"""
254 self
.wr_we_i
= Signal(we_width
); """write port enable"""
255 self
.rd_addr_i
= Signal(addr_width
); """read port address"""
256 self
.rd_data_o
= Signal(data_width
); """read port data"""
257 self
.phase
= Signal(); """even/odd cycle indicator"""
258 # debug signals, only used in formal proofs
259 self
.dbg_addr
= Signal(addr_width
); """debug: address under test"""
260 self
.dbg_we_mask
= Signal(we_width
); """debug: write lane under test"""
261 self
.dbg_data
= Signal(data_width
); """debug: data to keep in sync"""
262 self
.dbg_wrote
= Signal(addr_width
); """debug: data is valid"""
264 def elaborate(self
, platform
):
267 gran
= self
.data_width
// self
.we_width
268 # instantiate the two 1RW memory blocks
269 mem1
= SinglePortSRAM(self
.addr_width
, self
.data_width
, self
.we_width
)
270 mem2
= SinglePortSRAM(self
.addr_width
, self
.data_width
, self
.we_width
)
271 m
.submodules
.mem1
= mem1
272 m
.submodules
.mem2
= mem2
273 # wire write port to first memory, and its output to the second
274 m
.d
.comb
+= mem1
.d
.eq(self
.wr_data_i
)
275 m
.d
.comb
+= mem2
.d
.eq(mem1
.q
)
276 # holding registers for the write port of the second memory
277 last_wr_addr
= Signal(self
.addr_width
)
278 last_wr_we
= Signal(self
.we_width
)
279 # do the read and write address coincide?
280 same_read_write
= Signal()
281 with m
.If(self
.phase
== self
.write_phase
):
282 # write phase, start a write on the first memory
283 m
.d
.comb
+= mem1
.a
.eq(self
.wr_addr_i
)
284 m
.d
.comb
+= mem1
.we
.eq(self
.wr_we_i
)
285 # save write address and write select for repeating the write
286 # on the second memory, later
287 m
.d
.sync
+= last_wr_we
.eq(self
.wr_we_i
)
288 m
.d
.sync
+= last_wr_addr
.eq(self
.wr_addr_i
)
289 # start a read on the second memory
290 m
.d
.comb
+= mem2
.a
.eq(self
.rd_addr_i
)
291 # output previously read data from the first memory
292 m
.d
.comb
+= self
.rd_data_o
.eq(mem1
.q
)
294 # remember whether we are reading from the same location we are
296 m
.d
.sync
+= same_read_write
.eq(self
.rd_addr_i
== self
.wr_addr_i
)
298 # read phase, write last written data on second memory
299 m
.d
.comb
+= mem2
.a
.eq(last_wr_addr
)
300 m
.d
.comb
+= mem2
.we
.eq(last_wr_we
)
301 # start a read on the first memory
302 m
.d
.comb
+= mem1
.a
.eq(self
.rd_addr_i
)
304 with m
.If(same_read_write
):
305 # when transparent, and read and write addresses coincide,
306 # output the data just written
307 m
.d
.comb
+= self
.rd_data_o
.eq(mem1
.q
)
309 # otherwise, output previously read data
310 # from the second memory
311 m
.d
.comb
+= self
.rd_data_o
.eq(mem2
.q
)
313 # always output the read data from the second memory,
315 m
.d
.comb
+= self
.rd_data_o
.eq(mem2
.q
)
317 if platform
== "formal":
318 # the following is needed for induction, where an unreachable
319 # state (memory and holding register differ) is turned into an
321 # first, get the values stored in our memory location, using its
323 m
.d
.comb
+= mem1
.dbg_a
.eq(self
.dbg_addr
)
324 m
.d
.comb
+= mem2
.dbg_a
.eq(self
.dbg_addr
)
325 stored1
= Signal(self
.data_width
)
326 stored2
= Signal(self
.data_width
)
327 m
.d
.comb
+= stored1
.eq(mem1
.dbg_q
)
328 m
.d
.comb
+= stored2
.eq(mem2
.dbg_q
)
329 # now, ensure that the value stored in the first memory is always
330 # in sync with the holding register
331 with m
.If(self
.dbg_wrote
):
332 for i
in range(self
.we_width
):
333 with m
.If(self
.dbg_we_mask
[i
]):
335 self
.dbg_data
== stored1
.word_select(i
, gran
))
336 # same for the second memory, but one cycle later
337 with m
.If(Past(self
.dbg_wrote
)):
338 for i
in range(self
.we_width
):
339 with m
.If(self
.dbg_we_mask
[i
]):
341 Past(self
.dbg_data
) == stored2
.word_select(i
, gran
))
346 class PhasedDualPortRegfileTestCase(FHDLTestCase
):
348 def do_test_phased_dual_port_regfile(self
, write_phase
, transparent
):
350 Simulate some read/write/modify operations on the phased write memory
352 dut
= PhasedDualPortRegfile(7, 32, 4, write_phase
, transparent
)
356 # compare read data with previously written data
357 # and start a new read
358 def read(rd_addr_i
, expected
=None):
359 if expected
is not None:
360 self
.assertEqual((yield dut
.rd_data_o
), expected
)
361 yield dut
.rd_addr_i
.eq(rd_addr_i
)
363 # start a write, and set write phase
364 def write(wr_addr_i
, wr_we_i
, wr_data_i
):
365 yield dut
.wr_addr_i
.eq(wr_addr_i
)
366 yield dut
.wr_we_i
.eq(wr_we_i
)
367 yield dut
.wr_data_i
.eq(wr_data_i
)
368 yield dut
.phase
.eq(write_phase
)
370 # disable writes, and start read phase
372 yield dut
.wr_addr_i
.eq(0)
373 yield dut
.wr_we_i
.eq(0)
374 yield dut
.wr_data_i
.eq(0)
375 yield dut
.phase
.eq(~write_phase
)
377 # writes a few values on the write port, and read them back
378 # ... reads can happen every cycle
379 # ... writes, only every two cycles.
380 # since reads have a one cycle delay, the expected value on
381 # each read refers to the last read performed, not the
382 # current one, which is in progress.
385 yield from write(0x42, 0b1111, 0x12345678)
387 yield from read(0x42)
388 yield from skip_write()
390 yield from read(0x42)
391 yield from write(0x43, 0b1111, 0x9ABCDEF0)
393 yield from read(0x43, 0x12345678)
394 yield from skip_write()
396 yield from read(0x42, 0x12345678)
397 yield from write(0x43, 0b1001, 0xF0FFFF9A)
399 yield from read(0x43, 0x9ABCDEF0)
400 yield from skip_write()
402 yield from read(0x43, 0x12345678)
403 yield from write(0x42, 0b0110, 0xFF5634FF)
405 yield from read(0x42, 0xF0BCDE9A)
406 yield from skip_write()
408 yield from read(0, 0xF0BCDE9A)
409 yield from write(0, 0, 0)
411 yield from read(0, 0x12563478)
412 yield from skip_write()
414 # try reading and writing to the same location, simultaneously
415 yield from read(0x42)
416 yield from write(0x42, 0b1111, 0x55AA9966)
419 yield from read(0x42)
420 yield from skip_write()
423 # returns the value just written
424 yield from read(0, 0x55AA9966)
426 # returns the old value
427 yield from read(0, 0x12563478)
428 yield from write(0, 0, 0)
430 # after a cycle, always returns the new value
431 yield from read(0, 0x55AA9966)
432 yield from skip_write()
434 sim
.add_sync_process(process
)
435 debug_file
= f
'test_phased_dual_port_{write_phase}'
437 debug_file
+= '_transparent'
438 traces
= ['clk', 'phase',
439 'wr_addr_i[6:0]', 'wr_we_i[3:0]', 'wr_data_i[31:0]',
440 'rd_addr_i[6:0]', 'rd_data_o[31:0]']
441 write_gtkw(debug_file
+ '.gtkw',
443 traces
, module
='top', zoom
=-22)
444 sim_writer
= sim
.write_vcd(debug_file
+ '.vcd')
448 def test_phased_dual_port_regfile(self
):
449 """test both types (odd and even write ports) of phased write memory"""
450 with self
.subTest("writes happen on phase 0"):
451 self
.do_test_phased_dual_port_regfile(0, False)
452 with self
.subTest("writes happen on phase 1"):
453 self
.do_test_phased_dual_port_regfile(1, False)
454 """test again, with a transparent read port"""
455 with self
.subTest("writes happen on phase 0 (transparent reads)"):
456 self
.do_test_phased_dual_port_regfile(0, True)
457 with self
.subTest("writes happen on phase 1 (transparent reads)"):
458 self
.do_test_phased_dual_port_regfile(1, True)
460 def do_test_phased_dual_port_regfile_proof(self
, write_phase
, transparent
):
462 Formal proof of the pseudo 1W/1R regfile
465 # 128 x 32-bit, 8-bit granularity
466 dut
= PhasedDualPortRegfile(7, 32, 4, write_phase
, transparent
)
467 m
.submodules
.dut
= dut
468 gran
= dut
.data_width
// dut
.we_width
# granularity
469 # choose a single random memory location to test
470 a_const
= AnyConst(dut
.addr_width
)
471 # choose a single byte lane to test (one-hot encoding)
472 we_mask
= Signal(dut
.we_width
)
473 # ... by first creating a random bit pattern
474 we_const
= AnyConst(dut
.we_width
)
475 # ... and zeroing all but the first non-zero bit
476 m
.d
.comb
+= we_mask
.eq(we_const
& (-we_const
))
477 # drive alternating phases
478 m
.d
.comb
+= Assume(dut
.phase
!= Past(dut
.phase
))
479 # holding data register
481 # for some reason, simulated formal memory is not zeroed at reset
482 # ... so, remember whether we wrote it, at least once.
484 # if our memory location and byte lane is being written,
485 # capture the data in our holding register
486 with m
.If((dut
.wr_addr_i
== a_const
)
487 & (dut
.phase
== dut
.write_phase
)):
488 for i
in range(dut
.we_width
):
489 with m
.If(we_mask
[i
] & dut
.wr_we_i
[i
]):
490 m
.d
.sync
+= d_reg
.eq(
491 dut
.wr_data_i
[i
* gran
:i
* gran
+ gran
])
492 m
.d
.sync
+= wrote
.eq(1)
493 # if our memory location is being read,
494 # and the holding register has valid data,
495 # then its value must match the memory output, on the given lane
496 with m
.If(Past(dut
.rd_addr_i
) == a_const
):
499 for i
in range(dut
.we_width
):
500 rd_lane
= dut
.rd_data_o
.word_select(i
, gran
)
501 with m
.If(we_mask
[i
]):
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 for i
in range(dut
.we_width
):
511 rd_lane
= dut
.rd_data_o
.word_select(i
, gran
)
512 with m
.If(we_mask
[i
]):
513 m
.d
.sync
+= Assert(Past(d_reg
) == rd_lane
)
515 # otherwise, check against current written value
517 for i
in range(dut
.we_width
):
518 rd_lane
= dut
.rd_data_o
.word_select(i
, gran
)
519 with m
.If(we_mask
[i
]):
520 m
.d
.sync
+= Assert(d_reg
== rd_lane
)
522 # pass our state to the device under test, so it can ensure that
523 # its state is in sync with ours, for induction
525 # address and mask under test
526 dut
.dbg_addr
.eq(a_const
),
527 dut
.dbg_we_mask
.eq(we_mask
),
528 # state of our holding register
529 dut
.dbg_data
.eq(d_reg
),
530 dut
.dbg_wrote
.eq(wrote
),
533 self
.assertFormal(m
, mode
="prove", depth
=2)
535 def test_phased_dual_port_regfile_proof(self
):
536 """test both types (odd and even write ports) of phased write memory"""
537 with self
.subTest("writes happen on phase 0"):
538 self
.do_test_phased_dual_port_regfile_proof(0, False)
539 with self
.subTest("writes happen on phase 1"):
540 self
.do_test_phased_dual_port_regfile_proof(1, False)
541 # test again, with transparent read ports
542 with self
.subTest("writes happen on phase 0 (transparent reads)"):
543 self
.do_test_phased_dual_port_regfile_proof(0, True)
544 with self
.subTest("writes happen on phase 1 (transparent reads)"):
545 self
.do_test_phased_dual_port_regfile_proof(1, True)
548 class DualPortRegfile(Elaboratable
):
550 Builds, from a pair of phased 1W/1R blocks, a true 1W/1R RAM, where both
551 read and write ports work every cycle.
552 It employs a Last Value Table, that tracks to which memory each address was
555 :param addr_width: width of the address bus
556 :param data_width: width of the data bus
557 :param we_width: number of write enable lines
558 :param transparent: whether a simultaneous read and write returns the
559 new value (True) or the old value (False)
562 def __init__(self
, addr_width
, data_width
, we_width
, transparent
=True):
563 self
.addr_width
= addr_width
564 self
.data_width
= data_width
565 self
.we_width
= we_width
566 self
.transparent
= transparent
567 self
.wr_addr_i
= Signal(addr_width
); """write port address"""
568 self
.wr_data_i
= Signal(data_width
); """write port data"""
569 self
.wr_we_i
= Signal(we_width
); """write port enable"""
570 self
.rd_addr_i
= Signal(addr_width
); """read port address"""
571 self
.rd_data_o
= Signal(data_width
); """read port data"""
573 def elaborate(self
, _
):
575 # depth and granularity
576 depth
= 1 << self
.addr_width
577 gran
= self
.data_width
// self
.we_width
578 # instantiate the two phased 1R/1W memory blocks
579 mem0
= PhasedDualPortRegfile(
580 self
.addr_width
, self
.data_width
, self
.we_width
, 0,
582 mem1
= PhasedDualPortRegfile(
583 self
.addr_width
, self
.data_width
, self
.we_width
, 1,
585 m
.submodules
.mem0
= mem0
586 m
.submodules
.mem1
= mem1
587 # instantiate the backing memory (FFRAM or LUTRAM)
588 # for the Last Value Table
589 # it should have the same number and port types of the desired
590 # memory, but just one bit per write lane
591 lvt_mem
= Memory(width
=self
.we_width
, depth
=depth
)
592 lvt_wr
= lvt_mem
.write_port(granularity
=1)
593 lvt_rd
= lvt_mem
.read_port(transparent
=self
.transparent
)
594 m
.submodules
.lvt_wr
= lvt_wr
595 m
.submodules
.lvt_rd
= lvt_rd
596 # generate and wire the phases for the phased memories
598 m
.d
.sync
+= phase
.eq(~phase
)
600 mem0
.phase
.eq(phase
),
601 mem1
.phase
.eq(phase
),
604 # wire the write ports, directly
605 mem0
.wr_addr_i
.eq(self
.wr_addr_i
),
606 mem1
.wr_addr_i
.eq(self
.wr_addr_i
),
607 mem0
.wr_we_i
.eq(self
.wr_we_i
),
608 mem1
.wr_we_i
.eq(self
.wr_we_i
),
609 mem0
.wr_data_i
.eq(self
.wr_data_i
),
610 mem1
.wr_data_i
.eq(self
.wr_data_i
),
611 # also wire the read addresses
612 mem0
.rd_addr_i
.eq(self
.rd_addr_i
),
613 mem1
.rd_addr_i
.eq(self
.rd_addr_i
),
614 # wire read and write ports to the LVT
615 lvt_wr
.addr
.eq(self
.wr_addr_i
),
616 lvt_wr
.en
.eq(self
.wr_we_i
),
617 lvt_rd
.addr
.eq(self
.rd_addr_i
),
618 # the data for the LVT is the phase on which the value was
620 lvt_wr
.data
.eq(Repl(phase
, self
.we_width
)),
622 for i
in range(self
.we_width
):
623 # select the right memory to assign to the output read port,
624 # in this byte lane, according to the LVT contents
625 m
.d
.comb
+= self
.rd_data_o
.word_select(i
, gran
).eq(
628 mem1
.rd_data_o
.word_select(i
, gran
),
629 mem0
.rd_data_o
.word_select(i
, gran
)))
630 # TODO create debug port and pass state downstream
632 mem0
.dbg_wrote
.eq(0),
633 mem1
.dbg_wrote
.eq(0),
638 class DualPortRegfileTestCase(FHDLTestCase
):
640 def do_test_dual_port_regfile(self
, transparent
):
642 Simulate some read/write/modify operations on the dual port register
645 dut
= DualPortRegfile(7, 32, 4, transparent
)
652 # compare read data with previously written data
653 # and start a new read
654 def read(rd_addr_i
, next_expected
=None):
655 nonlocal expected
, last_expected
656 if expected
is not None:
657 self
.assertEqual((yield dut
.rd_data_o
), expected
)
658 yield dut
.rd_addr_i
.eq(rd_addr_i
)
659 # account for the read latency
660 expected
= last_expected
661 last_expected
= next_expected
664 def write(wr_addr_i
, wr_we_i
, wr_data_i
):
665 yield dut
.wr_addr_i
.eq(wr_addr_i
)
666 yield dut
.wr_we_i
.eq(wr_we_i
)
667 yield dut
.wr_data_i
.eq(wr_data_i
)
670 # write a pair of values, one for each memory
672 yield from write(0x42, 0b1111, 0x87654321)
674 yield from read(0x42, 0x87654321)
675 yield from write(0x43, 0b1111, 0x0FEDCBA9)
678 yield from read(0x43, 0x0FEDCBA9)
679 yield from write(0, 0, 0)
681 # write again, but now they switch memories
683 yield from write(0x42, 0b1111, 0x12345678)
685 yield from read(0x42, 0x12345678)
686 yield from write(0x43, 0b1111, 0x9ABCDEF0)
688 yield from read(0x43, 0x9ABCDEF0)
689 yield from write(0, 0, 0)
691 # test partial writes
693 yield from write(0x42, 0b1001, 0x78FFFF12)
696 yield from write(0x43, 0b0110, 0xFFDEABFF)
698 yield from read(0x42, 0x78345612)
699 yield from write(0, 0, 0)
701 yield from read(0x43, 0x9ADEABF0)
702 yield from write(0, 0, 0)
705 yield from write(0, 0, 0)
708 # returns the value just written
709 yield from read(0x42, 0x55AA9966)
711 # returns the old value
712 yield from read(0x42, 0x78345612)
713 yield from write(0x42, 0b1111, 0x55AA9966)
715 # after a cycle, always returns the new value
716 yield from read(0x42, 0x55AA9966)
717 yield from write(0, 0, 0)
720 yield from write(0, 0, 0)
723 yield from write(0, 0, 0)
725 sim
.add_sync_process(process
)
726 debug_file
= 'test_dual_port_regfile'
728 debug_file
+= '_transparent'
729 traces
= ['clk', 'phase',
730 {'comment': 'write port'},
731 'wr_addr_i[6:0]', 'wr_we_i[3:0]', 'wr_data_i[31:0]',
732 {'comment': 'read port'},
733 'rd_addr_i[6:0]', 'rd_data_o[31:0]',
734 {'comment': 'LVT write port'},
735 'phase', 'lvt_mem_w_addr[6:0]', 'lvt_mem_w_en[3:0]',
736 'lvt_mem_w_data[3:0]',
737 {'comment': 'LVT read port'},
738 'lvt_mem_r_addr[6:0]', 'lvt_mem_r_data[3:0]',
739 {'comment': 'backing memory'},
740 'mem0.rd_data_o[31:0]',
741 'mem1.rd_data_o[31:0]',
743 write_gtkw(debug_file
+ '.gtkw',
745 traces
, module
='top', zoom
=-22)
746 sim_writer
= sim
.write_vcd(debug_file
+ '.vcd')
750 def test_dual_port_regfile(self
):
751 with self
.subTest("non-transparent reads"):
752 self
.do_test_dual_port_regfile(False)
753 with self
.subTest("transparent reads"):
754 self
.do_test_dual_port_regfile(True)
756 def test_dual_port_regfile_proof(self
):
758 Formal proof of the 1W/1R regfile
761 # 128 x 32-bit, 8-bit granularity
762 dut
= DualPortRegfile(7, 32, 4, True)
763 m
.submodules
.dut
= dut
764 gran
= dut
.data_width
// dut
.we_width
# granularity
765 # choose a single random memory location to test
766 a_const
= AnyConst(dut
.addr_width
)
767 # choose a single byte lane to test (one-hot encoding)
768 we_mask
= Signal(dut
.we_width
)
769 # ... by first creating a random bit pattern
770 we_const
= AnyConst(dut
.we_width
)
771 # ... and zeroing all but the first non-zero bit
772 m
.d
.comb
+= we_mask
.eq(we_const
& (-we_const
))
773 # holding data register
775 # for some reason, simulated formal memory is not zeroed at reset
776 # ... so, remember whether we wrote it, at least once.
778 # if our memory location and byte lane is being written,
779 # capture the data in our holding register
780 with m
.If((dut
.wr_addr_i
== a_const
)):
781 for i
in range(dut
.we_width
):
782 with m
.If(we_mask
[i
] & dut
.wr_we_i
[i
]):
783 m
.d
.sync
+= d_reg
.eq(
784 dut
.wr_data_i
[i
* gran
:i
* gran
+ gran
])
785 m
.d
.sync
+= wrote
.eq(1)
786 # if our memory location is being read,
787 # and the holding register has valid data,
788 # then its value must match the memory output, on the given lane
789 with m
.If(Past(dut
.rd_addr_i
) == a_const
):
791 for i
in range(dut
.we_width
):
792 rd_lane
= dut
.rd_data_o
.word_select(i
, gran
)
793 with m
.If(we_mask
[i
]):
794 m
.d
.sync
+= Assert(d_reg
== rd_lane
)
796 self
.assertFormal(m
, mode
="bmc", depth
=10)
799 if __name__
== "__main__":