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, 0b0101, 0x55AA9966)
427 yield from read(0x42)
428 yield from skip_write()
431 # returns the value just written
432 yield from read(0, 0x12AA3466)
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, 0x12AA3466)
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 if not self
.transparent
:
603 # for some reason, formal proofs don't recognize the default
604 # reset value for this signal
605 m
.d
.comb
+= lvt_rd
.en
.eq(1)
606 m
.submodules
.lvt_wr
= lvt_wr
607 m
.submodules
.lvt_rd
= lvt_rd
608 # generate and wire the phases for the phased memories
610 m
.d
.sync
+= phase
.eq(~phase
)
612 mem0
.phase
.eq(phase
),
613 mem1
.phase
.eq(phase
),
616 # wire the write ports, directly
617 mem0
.wr_addr_i
.eq(self
.wr_addr_i
),
618 mem1
.wr_addr_i
.eq(self
.wr_addr_i
),
619 mem0
.wr_we_i
.eq(self
.wr_we_i
),
620 mem1
.wr_we_i
.eq(self
.wr_we_i
),
621 mem0
.wr_data_i
.eq(self
.wr_data_i
),
622 mem1
.wr_data_i
.eq(self
.wr_data_i
),
623 # also wire the read addresses
624 mem0
.rd_addr_i
.eq(self
.rd_addr_i
),
625 mem1
.rd_addr_i
.eq(self
.rd_addr_i
),
626 # wire read and write ports to the LVT
627 lvt_wr
.addr
.eq(self
.wr_addr_i
),
628 lvt_wr
.en
.eq(self
.wr_we_i
),
629 lvt_rd
.addr
.eq(self
.rd_addr_i
),
630 # the data for the LVT is the phase on which the value was
632 lvt_wr
.data
.eq(Repl(phase
, self
.we_width
)),
634 for i
in range(self
.we_width
):
635 # select the right memory to assign to the output read port,
636 # in this byte lane, according to the LVT contents
637 m
.d
.comb
+= self
.rd_data_o
.word_select(i
, gran
).eq(
640 mem1
.rd_data_o
.word_select(i
, gran
),
641 mem0
.rd_data_o
.word_select(i
, gran
)))
643 if platform
== "formal":
644 # pass upstream state to the memories, so they can ensure that
645 # their state are in sync with upstream, for induction
647 # address and write lane under test
648 mem0
.dbg_addr
.eq(self
.dbg_addr
),
649 mem1
.dbg_addr
.eq(self
.dbg_addr
),
650 mem0
.dbg_lane
.eq(self
.dbg_lane
),
651 mem1
.dbg_lane
.eq(self
.dbg_lane
),
653 mem0
.dbg_data
.eq(self
.dbg_data
),
654 mem1
.dbg_data
.eq(self
.dbg_data
),
655 # the memory, on which the write ends up, depends on which
656 # phase it was written
657 mem0
.dbg_wrote
.eq(self
.dbg_wrote
& ~self
.dbg_wrote_phase
),
658 mem1
.dbg_wrote
.eq(self
.dbg_wrote
& self
.dbg_wrote_phase
),
660 # sync phase to upstream
661 m
.d
.comb
+= Assert(self
.dbg_phase
== phase
)
662 # this debug port for the LVT is an asynchronous read port,
663 # allowing direct access to a given memory location
664 # by the formal engine
665 m
.submodules
.dbgport
= dbgport
= lvt_mem
.read_port(domain
='comb')
666 # first, get the value stored in our memory location,
667 stored
= Signal(self
.we_width
)
668 m
.d
.comb
+= dbgport
.addr
.eq(self
.dbg_addr
)
669 m
.d
.comb
+= stored
.eq(dbgport
.data
)
670 # now, ensure that the value stored in memory is always in sync
671 # with the expected value (which memory the value was written to)
672 with m
.If(self
.dbg_wrote
):
673 m
.d
.comb
+= Assert(stored
.bit_select(self
.dbg_lane
, 1)
674 == self
.dbg_wrote_phase
)
687 class DualPortRegfileTestCase(FHDLTestCase
):
689 def do_test_dual_port_regfile(self
, transparent
):
691 Simulate some read/write/modify operations on the dual port register
694 dut
= DualPortRegfile(7, 32, 4, transparent
)
701 # compare read data with previously written data
702 # and start a new read
703 def read(rd_addr_i
, next_expected
=None):
704 nonlocal expected
, last_expected
705 if expected
is not None:
706 self
.assertEqual((yield dut
.rd_data_o
), expected
)
707 yield dut
.rd_addr_i
.eq(rd_addr_i
)
708 # account for the read latency
709 expected
= last_expected
710 last_expected
= next_expected
713 def write(wr_addr_i
, wr_we_i
, wr_data_i
):
714 yield dut
.wr_addr_i
.eq(wr_addr_i
)
715 yield dut
.wr_we_i
.eq(wr_we_i
)
716 yield dut
.wr_data_i
.eq(wr_data_i
)
719 # write a pair of values, one for each memory
721 yield from write(0x42, 0b1111, 0x87654321)
723 yield from read(0x42, 0x87654321)
724 yield from write(0x43, 0b1111, 0x0FEDCBA9)
727 yield from read(0x43, 0x0FEDCBA9)
728 yield from write(0, 0, 0)
730 # write again, but now they switch memories
732 yield from write(0x42, 0b1111, 0x12345678)
734 yield from read(0x42, 0x12345678)
735 yield from write(0x43, 0b1111, 0x9ABCDEF0)
737 yield from read(0x43, 0x9ABCDEF0)
738 yield from write(0, 0, 0)
740 # test partial writes
742 yield from write(0x42, 0b1001, 0x78FFFF12)
745 yield from write(0x43, 0b0110, 0xFFDEABFF)
747 yield from read(0x42, 0x78345612)
748 yield from write(0, 0, 0)
750 yield from read(0x43, 0x9ADEABF0)
751 yield from write(0, 0, 0)
754 yield from write(0, 0, 0)
757 # returns the value just written
758 yield from read(0x42, 0x78AA5666)
760 # returns the old value
761 yield from read(0x42, 0x78345612)
762 yield from write(0x42, 0b0101, 0x55AA9966)
764 # after a cycle, always returns the new value
765 yield from read(0x42, 0x78AA5666)
766 yield from write(0, 0, 0)
769 yield from write(0, 0, 0)
772 yield from write(0, 0, 0)
774 sim
.add_sync_process(process
)
775 debug_file
= 'test_dual_port_regfile'
777 debug_file
+= '_transparent'
778 traces
= ['clk', 'phase',
779 {'comment': 'write port'},
780 'wr_addr_i[6:0]', 'wr_we_i[3:0]', 'wr_data_i[31:0]',
781 {'comment': 'read port'},
782 'rd_addr_i[6:0]', 'rd_data_o[31:0]',
783 {'comment': 'LVT write port'},
784 'phase', 'lvt_mem_w_addr[6:0]', 'lvt_mem_w_en[3:0]',
785 'lvt_mem_w_data[3:0]',
786 {'comment': 'LVT read port'},
787 'lvt_mem_r_addr[6:0]', 'lvt_mem_r_data[3:0]',
788 {'comment': 'backing memory'},
789 'mem0.rd_data_o[31:0]',
790 'mem1.rd_data_o[31:0]',
792 write_gtkw(debug_file
+ '.gtkw',
794 traces
, module
='top', zoom
=-22)
795 sim_writer
= sim
.write_vcd(debug_file
+ '.vcd')
799 def test_dual_port_regfile(self
):
800 with self
.subTest("non-transparent reads"):
801 self
.do_test_dual_port_regfile(False)
802 with self
.subTest("transparent reads"):
803 self
.do_test_dual_port_regfile(True)
805 def do_test_dual_port_regfile_proof(self
, transparent
=True):
807 Formal proof of the 1W/1R regfile
810 # 128 x 32-bit, 8-bit granularity
811 dut
= DualPortRegfile(7, 32, 4, transparent
)
812 m
.submodules
.dut
= dut
813 gran
= dut
.data_width
// dut
.we_width
# granularity
814 # choose a single random memory location to test
815 a_const
= AnyConst(dut
.addr_width
)
816 # choose a single byte lane to test
817 lane
= AnyConst(range(dut
.we_width
))
818 # holding data register
820 # keep track of the phase, so we can remember which memory
823 m
.d
.sync
+= phase
.eq(~phase
)
824 # for some reason, simulated formal memory is not zeroed at reset
825 # ... so, remember whether we wrote it, at least once.
827 # ... and on which phase it was written
828 wrote_phase
= Signal()
829 # if our memory location and byte lane is being written,
830 # capture the data in our holding register
831 with m
.If((dut
.wr_addr_i
== a_const
)
832 & dut
.wr_we_i
.bit_select(lane
, 1)):
833 m
.d
.sync
+= d_reg
.eq(dut
.wr_data_i
.word_select(lane
, gran
))
834 m
.d
.sync
+= wrote
.eq(1)
835 m
.d
.sync
+= wrote_phase
.eq(phase
)
836 # if our memory location is being read,
837 # and the holding register has valid data,
838 # then its value must match the memory output, on the given lane
839 with m
.If(Past(dut
.rd_addr_i
) == a_const
):
842 rd_lane
= dut
.rd_data_o
.word_select(lane
, gran
)
843 m
.d
.sync
+= Assert(d_reg
== rd_lane
)
845 # with a non-transparent read port, the read value depends
846 # on whether there is a simultaneous write, or not
847 with m
.If(Past(dut
.wr_addr_i
) == a_const
):
848 # simultaneous write -> check against last written value
849 with m
.If(wrote
& Past(wrote
)):
850 rd_lane
= dut
.rd_data_o
.word_select(lane
, gran
)
851 m
.d
.sync
+= Assert(Past(d_reg
) == rd_lane
)
853 # otherwise, check against current written value
855 rd_lane
= dut
.rd_data_o
.word_select(lane
, gran
)
856 m
.d
.sync
+= Assert(d_reg
== rd_lane
)
859 dut
.dbg_addr
.eq(a_const
),
860 dut
.dbg_lane
.eq(lane
),
861 dut
.dbg_data
.eq(d_reg
),
862 dut
.dbg_wrote
.eq(wrote
),
863 dut
.dbg_wrote_phase
.eq(wrote_phase
),
864 dut
.dbg_phase
.eq(phase
),
867 self
.assertFormal(m
, mode
="prove", depth
=3)
869 def test_dual_port_regfile_proof(self
):
871 Formal check of 1W/1R regfile (transparent and not)
873 with self
.subTest("transparent reads"):
874 self
.do_test_dual_port_regfile_proof(True)
875 with self
.subTest("non-transparent reads"):
876 self
.do_test_dual_port_regfile_proof(False)
879 class PhasedReadPhasedWriteFullReadSRAM(Elaboratable
):
881 Builds, from three 1RW blocks, a pseudo 1W/2R SRAM, with:
883 * one full read port, which works every cycle,
884 * one write port, which is only available on either even or odd cycles,
885 * an extra transparent read port, available only on the same cycles as the
888 This type of SRAM is useful for a XOR-based 6x1RW implementation of
889 a 1R/1W register file.
891 :param addr_width: width of the address bus
892 :param data_width: width of the data bus
893 :param we_width: number of write enable lines
894 :param write_phase: indicates on which phase the write port will
896 :param transparent: whether a simultaneous read and write returns the
897 new value (True) or the old value (False) on the full
900 .. note:: The debug read port is meant only to assist in formal proofs!
903 def __init__(self
, addr_width
, data_width
, we_width
, write_phase
,
905 self
.addr_width
= addr_width
906 self
.data_width
= data_width
907 self
.we_width
= we_width
908 self
.write_phase
= write_phase
909 self
.transparent
= transparent
911 self
.wr_addr_i
= Signal(addr_width
); """phased write port address"""
912 self
.wr_data_i
= Signal(data_width
); """phased write port data"""
913 self
.wr_we_i
= Signal(we_width
); """phased write port enable"""
914 self
.rd_addr_i
= Signal(addr_width
); """full read port address"""
915 self
.rd_data_o
= Signal(data_width
); """full read port data"""
916 self
.rdp_addr_i
= Signal(addr_width
); """phased read port address"""
917 self
.rdp_data_o
= Signal(data_width
); """phased read port data"""
918 self
.phase
= Signal(); """even/odd cycle indicator"""
919 # debug signals, only used in formal proofs
920 self
.dbg_addr
= Signal(addr_width
); """debug: address under test"""
921 lanes
= range(we_width
)
922 self
.dbg_lane
= Signal(lanes
); """debug: write lane under test"""
923 gran
= self
.data_width
// self
.we_width
924 self
.dbg_data
= Signal(gran
); """debug: data to keep in sync"""
925 self
.dbg_wrote
= Signal(); """debug: data is valid"""
927 def elaborate(self
, platform
):
929 # instantiate the 1RW memory blocks
930 mem1
= SinglePortSRAM(self
.addr_width
, self
.data_width
, self
.we_width
)
931 mem2
= SinglePortSRAM(self
.addr_width
, self
.data_width
, self
.we_width
)
932 mem3
= SinglePortSRAM(self
.addr_width
, self
.data_width
, self
.we_width
)
933 m
.submodules
.mem1
= mem1
934 m
.submodules
.mem2
= mem2
935 m
.submodules
.mem3
= mem3
936 # wire input write data to first memory, and its output to the others
938 mem1
.d
.eq(self
.wr_data_i
),
942 # holding registers for the write port of the other memories
943 last_wr_addr
= Signal(self
.addr_width
)
944 last_wr_we
= Signal(self
.we_width
)
945 # do read and write addresses coincide?
946 same_read_write
= Signal()
947 same_phased_read_write
= Signal()
948 with m
.If(self
.phase
== self
.write_phase
):
949 # write phase, start a write on the first memory
950 m
.d
.comb
+= mem1
.a
.eq(self
.wr_addr_i
)
951 m
.d
.comb
+= mem1
.we
.eq(self
.wr_we_i
)
952 # save write address and write select for repeating the write
953 # on the other memories, one cycle later
954 m
.d
.sync
+= last_wr_we
.eq(self
.wr_we_i
)
955 m
.d
.sync
+= last_wr_addr
.eq(self
.wr_addr_i
)
956 # start a read on the other memories
957 m
.d
.comb
+= mem2
.a
.eq(self
.rd_addr_i
)
958 m
.d
.comb
+= mem3
.a
.eq(self
.rdp_addr_i
)
959 # output previously read data from the first memory
960 m
.d
.comb
+= self
.rd_data_o
.eq(mem1
.q
)
961 # remember whether we are reading from the same location as we
963 m
.d
.sync
+= same_phased_read_write
.eq(
964 self
.rdp_addr_i
== self
.wr_addr_i
)
966 m
.d
.sync
+= same_read_write
.eq(self
.rd_addr_i
== self
.wr_addr_i
)
968 # read phase, write last written data on the other memories
970 mem2
.a
.eq(last_wr_addr
),
971 mem2
.we
.eq(last_wr_we
),
972 mem3
.a
.eq(last_wr_addr
),
973 mem3
.we
.eq(last_wr_we
),
975 # start a read on the first memory
976 m
.d
.comb
+= mem1
.a
.eq(self
.rd_addr_i
)
977 # output the read data from the second memory
979 with m
.If(same_read_write
):
980 # when transparent, and read and write addresses coincide,
981 # output the data just written
982 m
.d
.comb
+= self
.rd_data_o
.eq(mem1
.q
)
984 # otherwise, output previously read data
985 # from the second memory
986 m
.d
.comb
+= self
.rd_data_o
.eq(mem2
.q
)
988 # always output the read data from the second memory,
990 m
.d
.comb
+= self
.rd_data_o
.eq(mem2
.q
)
991 with m
.If(same_phased_read_write
):
992 # if read and write addresses coincide,
993 # output the data just written
994 m
.d
.comb
+= self
.rdp_data_o
.eq(mem1
.q
)
996 # otherwise, output previously read data
997 # from the third memory
998 m
.d
.comb
+= self
.rdp_data_o
.eq(mem3
.q
)
1000 if platform
== "formal":
1001 # pass our state to the device under test, so it can ensure that
1002 # its state is in sync with ours, for induction
1004 # pass the address and write lane under test to both memories
1005 mem1
.dbg_addr
.eq(self
.dbg_addr
),
1006 mem2
.dbg_addr
.eq(self
.dbg_addr
),
1007 mem3
.dbg_addr
.eq(self
.dbg_addr
),
1008 mem1
.dbg_lane
.eq(self
.dbg_lane
),
1009 mem2
.dbg_lane
.eq(self
.dbg_lane
),
1010 mem3
.dbg_lane
.eq(self
.dbg_lane
),
1011 # the other memories copy their state from the first memory,
1012 # after a cycle, so they have a one cycle delay
1013 mem1
.dbg_data
.eq(self
.dbg_data
),
1014 mem2
.dbg_data
.eq(Past(self
.dbg_data
)),
1015 mem3
.dbg_data
.eq(Past(self
.dbg_data
)),
1016 mem1
.dbg_wrote
.eq(self
.dbg_wrote
),
1017 mem2
.dbg_wrote
.eq(Past(self
.dbg_wrote
)),
1018 mem3
.dbg_wrote
.eq(Past(self
.dbg_wrote
)),
1024 class PhasedReadPhasedWriteFullReadSRAMTestCase(FHDLTestCase
):
1026 def do_test_case(self
, write_phase
, transparent
):
1028 Simulate some read/write/modify operations
1030 dut
= PhasedReadPhasedWriteFullReadSRAM(7, 32, 4, write_phase
,
1032 sim
= Simulator(dut
)
1036 last_expected
= None
1038 # compare read data with previously written data
1039 # and start a new read
1040 def read(rd_addr_i
, next_expected
=None):
1041 nonlocal expected
, last_expected
1042 if expected
is not None:
1043 self
.assertEqual((yield dut
.rd_data_o
), expected
)
1044 yield dut
.rd_addr_i
.eq(rd_addr_i
)
1045 # account for the read latency
1046 expected
= last_expected
1047 last_expected
= next_expected
1051 # same as above, but for the phased read port
1052 def phased_read(rdp_addr_i
, next_expected2
=None):
1054 if expected2
is not None:
1055 self
.assertEqual((yield dut
.rdp_data_o
), expected2
)
1056 yield dut
.rdp_addr_i
.eq(rdp_addr_i
)
1057 # account for the read latency
1058 expected2
= next_expected2
1061 def write(wr_addr_i
, wr_we_i
, wr_data_i
):
1062 yield dut
.wr_addr_i
.eq(wr_addr_i
)
1063 yield dut
.wr_we_i
.eq(wr_we_i
)
1064 yield dut
.wr_data_i
.eq(wr_data_i
)
1065 yield dut
.phase
.eq(write_phase
)
1067 # disable writes, and start read phase
1069 yield dut
.wr_addr_i
.eq(0)
1070 yield dut
.wr_we_i
.eq(0)
1071 yield dut
.wr_data_i
.eq(0)
1072 yield dut
.phase
.eq(~write_phase
)
1073 # also skip reading from the phased read port
1074 yield dut
.rdp_addr_i
.eq(0)
1076 # writes a few values on the write port, and read them back
1079 yield from phased_read(0)
1080 yield from write(0x42, 0b1111, 0x12345678)
1082 yield from read(0x42, 0x12345678)
1083 yield from skip_write()
1085 yield from read(0x42, 0x12345678)
1086 yield from phased_read(0x42, 0x12345678)
1087 yield from write(0x43, 0b1111, 0x9ABCDEF0)
1089 yield from read(0x43, 0x9ABCDEF0)
1090 yield from skip_write()
1092 yield from read(0x42, 0x12345678)
1093 yield from phased_read(0x42, 0x12345678)
1094 yield from write(0x43, 0b1001, 0xF0FFFF9A)
1096 yield from read(0x43, 0xF0BCDE9A)
1097 yield from skip_write()
1099 yield from read(0x43, 0xF0BCDE9A)
1100 yield from phased_read(0x43, 0xF0BCDE9A)
1101 yield from write(0x42, 0b0110, 0xFF5634FF)
1103 yield from read(0x42, 0x12563478)
1104 yield from skip_write()
1107 yield from phased_read(0)
1108 yield from write(0, 0, 0)
1111 yield from skip_write()
1113 # try reading and writing at the same time
1115 # transparent port, return the value just written
1116 yield from read(0x42, 0x12AA3466)
1118 # ... otherwise, return the old value
1119 yield from read(0x42, 0x12563478)
1120 # transparent port, always return the value just written
1121 yield from phased_read(0x42, 0x12AA3466)
1122 yield from write(0x42, 0b0101, 0x55AA9966)
1124 # after a cycle, always returns the new value
1125 yield from read(0x42, 0x12AA3466)
1126 yield from skip_write()
1129 yield from phased_read(0)
1130 yield from write(0, 0, 0)
1133 yield from skip_write()
1135 sim
.add_sync_process(process
)
1136 debug_file
= 'test_phased_read_write_sram_' + str(write_phase
)
1138 debug_file
+= '_transparent'
1139 traces
= ['clk', 'phase',
1140 {'comment': 'phased write port'},
1141 'wr_addr_i[6:0]', 'wr_we_i[3:0]', 'wr_data_i[31:0]',
1142 {'comment': 'full read port'},
1143 'rd_addr_i[6:0]', 'rd_data_o[31:0]',
1144 {'comment': 'phased read port'},
1145 'rdp_addr_i[6:0]', 'rdp_data_o[31:0]']
1146 write_gtkw(debug_file
+ '.gtkw',
1147 debug_file
+ '.vcd',
1148 traces
, module
='top', zoom
=-22)
1149 sim_writer
= sim
.write_vcd(debug_file
+ '.vcd')
1153 def test_case(self
):
1154 """test both types (odd and even write ports) of phased memory"""
1155 with self
.subTest("writes happen on phase 0"):
1156 self
.do_test_case(0, True)
1157 with self
.subTest("writes happen on phase 1"):
1158 self
.do_test_case(1, True)
1159 with self
.subTest("writes happen on phase 0 (non-transparent reads)"):
1160 self
.do_test_case(0, False)
1161 with self
.subTest("writes happen on phase 1 (non-transparent reads)"):
1162 self
.do_test_case(1, False)
1164 def do_test_formal(self
, write_phase
, transparent
):
1166 Formal proof of the pseudo 1W/2R regfile
1169 # 128 x 32-bit, 8-bit granularity
1170 dut
= PhasedReadPhasedWriteFullReadSRAM(7, 32, 4, write_phase
,
1172 m
.submodules
.dut
= dut
1173 gran
= dut
.data_width
// dut
.we_width
# granularity
1174 # choose a single random memory location to test
1175 a_const
= AnyConst(dut
.addr_width
)
1176 # choose a single byte lane to test
1177 lane
= AnyConst(range(dut
.we_width
))
1178 # drive alternating phases
1179 m
.d
.comb
+= Assume(dut
.phase
!= Past(dut
.phase
))
1180 # holding data register
1181 d_reg
= Signal(gran
)
1182 # for some reason, simulated formal memory is not zeroed at reset
1183 # ... so, remember whether we wrote it, at least once.
1185 # if our memory location and byte lane is being written,
1186 # capture the data in our holding register
1187 with m
.If((dut
.wr_addr_i
== a_const
)
1188 & dut
.wr_we_i
.bit_select(lane
, 1)
1189 & (dut
.phase
== dut
.write_phase
)):
1190 m
.d
.sync
+= d_reg
.eq(dut
.wr_data_i
.word_select(lane
, gran
))
1191 m
.d
.sync
+= wrote
.eq(1)
1192 # if our memory location is being read,
1193 # and the holding register has valid data,
1194 # then its value must match the memory output, on the given lane
1195 with m
.If(Past(dut
.rd_addr_i
) == a_const
):
1198 rd_lane
= dut
.rd_data_o
.word_select(lane
, gran
)
1199 m
.d
.sync
+= Assert(d_reg
== rd_lane
)
1201 # with a non-transparent read port, the read value depends
1202 # on whether there is a simultaneous write, or not
1203 with m
.If((Past(dut
.wr_addr_i
) == a_const
)
1204 & Past(dut
.phase
) == dut
.write_phase
):
1205 # simultaneous write -> check against last written value
1206 with m
.If(Past(wrote
)):
1207 rd_lane
= dut
.rd_data_o
.word_select(lane
, gran
)
1208 m
.d
.sync
+= Assert(Past(d_reg
) == rd_lane
)
1210 # otherwise, check against current written value
1212 rd_lane
= dut
.rd_data_o
.word_select(lane
, gran
)
1213 m
.d
.sync
+= Assert(d_reg
== rd_lane
)
1214 # same for the phased read port, except it's always transparent
1215 # and the port works only on the write phase
1216 with m
.If((Past(dut
.rdp_addr_i
) == a_const
) & wrote
1217 & (Past(dut
.phase
) == dut
.write_phase
)):
1218 rdp_lane
= dut
.rdp_data_o
.word_select(lane
, gran
)
1219 m
.d
.sync
+= Assert(d_reg
== rdp_lane
)
1221 # pass our state to the device under test, so it can ensure that
1222 # its state is in sync with ours, for induction
1224 # address and mask under test
1225 dut
.dbg_addr
.eq(a_const
),
1226 dut
.dbg_lane
.eq(lane
),
1227 # state of our holding register
1228 dut
.dbg_data
.eq(d_reg
),
1229 dut
.dbg_wrote
.eq(wrote
),
1232 self
.assertFormal(m
, mode
="prove", depth
=3)
1234 def test_formal(self
):
1235 """test both types (odd and even write ports) of phased write memory"""
1236 with self
.subTest("writes happen on phase 0"):
1237 self
.do_test_formal(0, False)
1238 with self
.subTest("writes happen on phase 1"):
1239 self
.do_test_formal(1, False)
1240 # test again, with transparent read ports
1241 with self
.subTest("writes happen on phase 0 (transparent reads)"):
1242 self
.do_test_formal(0, True)
1243 with self
.subTest("writes happen on phase 1 (transparent reads)"):
1244 self
.do_test_formal(1, True)
1247 class DualPortXorRegfile(Elaboratable
):
1249 Builds, from a pair of phased 1W/2R blocks, a true 1W/1R RAM, where both
1250 write and (non-transparent) read ports work every cycle.
1252 It employs a XOR trick, as follows:
1254 1) Like before, there are two memories, each reading on every cycle, and
1255 writing on alternate cycles
1256 2) Instead of a MUX, the read port is a direct XOR of the two memories.
1257 3) Writes happens in two cycles:
1259 First, read the current value of the *other* memory, at the write
1262 Then, on *this* memory, write that read value, XORed with the desired
1265 This recovers the desired value when read:
1266 (other XOR desired) XOR other = desired
1268 :param addr_width: width of the address bus
1269 :param data_width: width of the data bus
1270 :param we_width: number of write enable lines
1271 :param transparent: whether a simultaneous read and write returns the
1272 new value (True) or the old value (False) on the full
1276 def __init__(self
, addr_width
, data_width
, we_width
, transparent
):
1277 self
.addr_width
= addr_width
1278 self
.data_width
= data_width
1279 self
.we_width
= we_width
1280 self
.transparent
= transparent
1282 self
.wr_addr_i
= Signal(addr_width
); """write port address"""
1283 self
.wr_data_i
= Signal(data_width
); """write port data"""
1284 self
.wr_we_i
= Signal(we_width
); """write port enable"""
1285 self
.rd_addr_i
= Signal(addr_width
); """read port address"""
1286 self
.rd_data_o
= Signal(data_width
); """read port data"""
1288 def elaborate(self
, platform
):
1290 # instantiate the two phased 1W/2R memory blocks
1291 mem0
= PhasedReadPhasedWriteFullReadSRAM(
1292 self
.addr_width
, self
.data_width
, self
.we_width
, 0, True)
1293 mem1
= PhasedReadPhasedWriteFullReadSRAM(
1294 self
.addr_width
, self
.data_width
, self
.we_width
, 1, True)
1295 m
.submodules
.mem0
= mem0
1296 m
.submodules
.mem1
= mem1
1297 # generate and wire the phases for the phased memories
1299 m
.d
.sync
+= phase
.eq(~phase
)
1301 mem0
.phase
.eq(phase
),
1302 mem1
.phase
.eq(phase
),
1304 # store the write information for the next cycle
1305 last_addr
= Signal(self
.addr_width
)
1306 last_we
= Signal(self
.we_width
)
1307 last_data
= Signal(self
.data_width
)
1309 last_addr
.eq(self
.wr_addr_i
),
1310 last_we
.eq(self
.wr_we_i
),
1311 last_data
.eq(self
.wr_data_i
),
1314 # wire read address to memories, and XOR their output
1315 xor_data
= Signal(self
.data_width
)
1317 mem0
.rd_addr_i
.eq(self
.rd_addr_i
),
1318 mem1
.rd_addr_i
.eq(self
.rd_addr_i
),
1319 xor_data
.eq(mem0
.rd_data_o ^ mem1
.rd_data_o
),
1321 if self
.transparent
:
1322 # do the read and write addresses coincide?
1323 same_read_write
= Signal()
1324 m
.d
.sync
+= same_read_write
.eq(self
.rd_addr_i
== self
.wr_addr_i
)
1325 gran
= self
.data_width
// self
.we_width
1326 for i
in range(self
.we_width
):
1327 # when simultaneously reading and writing to the same location
1328 # and write lane, bypass the memory, and output the write
1329 # holding register instead
1330 with m
.If(same_read_write
& last_we
[i
]):
1331 m
.d
.comb
+= self
.rd_data_o
.word_select(i
, gran
).eq(
1332 last_data
.word_select(i
, gran
))
1333 # otherwise, output the xor data
1335 m
.d
.comb
+= self
.rd_data_o
.word_select(i
, gran
).eq(
1336 xor_data
.word_select(i
, gran
))
1337 # when not transparent, just output the memory contents (xor data)
1339 m
.d
.comb
+= self
.rd_data_o
.eq(xor_data
)
1341 # 1) read the memory location which is about to be written
1343 mem0
.rdp_addr_i
.eq(self
.wr_addr_i
),
1344 mem1
.rdp_addr_i
.eq(self
.wr_addr_i
),
1346 # 2) write the XOR of the other memory data, and the desired value
1348 mem0
.wr_addr_i
.eq(last_addr
),
1349 mem1
.wr_addr_i
.eq(last_addr
),
1350 mem0
.wr_we_i
.eq(last_we
),
1351 mem1
.wr_we_i
.eq(last_we
),
1352 mem0
.wr_data_i
.eq(last_data ^ mem1
.rdp_data_o
),
1353 mem1
.wr_data_i
.eq(last_data ^ mem0
.rdp_data_o
),
1358 class DualPortXorRegfileTestCase(FHDLTestCase
):
1360 def do_test_case(self
, transparent
):
1362 Simulate some read/write/modify operations on the dual port register
1365 dut
= DualPortXorRegfile(7, 32, 4, transparent
)
1366 sim
= Simulator(dut
)
1370 last_expected
= None
1372 # compare read data with previously written data
1373 # and start a new read
1374 def read(rd_addr_i
, next_expected
=None):
1375 nonlocal expected
, last_expected
1376 if expected
is not None:
1377 self
.assertEqual((yield dut
.rd_data_o
), expected
)
1378 yield dut
.rd_addr_i
.eq(rd_addr_i
)
1379 # account for the read latency
1380 expected
= last_expected
1381 last_expected
= next_expected
1384 def write(wr_addr_i
, wr_we_i
, wr_data_i
):
1385 yield dut
.wr_addr_i
.eq(wr_addr_i
)
1386 yield dut
.wr_we_i
.eq(wr_we_i
)
1387 yield dut
.wr_data_i
.eq(wr_data_i
)
1390 # write a pair of values, one for each memory
1392 yield from write(0x42, 0b1111, 0x87654321)
1394 yield from read(0x42, 0x87654321)
1395 yield from write(0x43, 0b1111, 0x0FEDCBA9)
1398 yield from read(0x43, 0x0FEDCBA9)
1399 yield from write(0, 0, 0)
1401 # write again, but now they switch memories
1403 yield from write(0x42, 0b1111, 0x12345678)
1405 yield from read(0x42, 0x12345678)
1406 yield from write(0x43, 0b1111, 0x9ABCDEF0)
1408 yield from read(0x43, 0x9ABCDEF0)
1409 yield from write(0, 0, 0)
1411 # test partial writes
1413 yield from write(0x42, 0b1001, 0x78FFFF12)
1416 yield from write(0x43, 0b0110, 0xFFDEABFF)
1418 yield from read(0x42, 0x78345612)
1419 yield from write(0, 0, 0)
1421 yield from read(0x43, 0x9ADEABF0)
1422 yield from write(0, 0, 0)
1425 yield from write(0, 0, 0)
1427 # test simultaneous read and write
1429 # transparent reads, returns the new value
1430 yield from read(0x42, 0x78AA5666)
1432 # non-transparent read: returns the old value
1433 yield from read(0x42, 0x78345612)
1434 yield from write(0x42, 0b0101, 0x55AA9966)
1436 # after a cycle, returns the new value
1437 yield from read(0x42, 0x78AA5666)
1438 yield from write(0, 0, 0)
1442 yield from write(0, 0, 0)
1445 yield from write(0, 0, 0)
1447 sim
.add_sync_process(process
)
1448 debug_file
= 'test_dual_port_xor_regfile'
1450 debug_file
+= '_transparent'
1451 traces
= ['clk', 'phase',
1452 {'comment': 'write port'},
1453 'wr_addr_i[6:0]', 'wr_we_i[3:0]', 'wr_data_i[31:0]',
1454 {'comment': 'read port'},
1455 'rd_addr_i[6:0]', 'rd_data_o[31:0]',
1457 write_gtkw(debug_file
+ '.gtkw',
1458 debug_file
+ '.vcd',
1459 traces
, module
='top', zoom
=-22)
1460 sim_writer
= sim
.write_vcd(debug_file
+ '.vcd')
1464 def test_case(self
):
1465 with self
.subTest("non-transparent reads"):
1466 self
.do_test_case(False)
1467 with self
.subTest("transparent reads"):
1468 self
.do_test_case(True)
1471 if __name__
== "__main__":