usb-tools/amaranth
1
0
Fork 0
Code Issues Pull requests Actions Packages Projects Releases Wiki Activity

lib.fifo: register GrayEncoder output before CDC.

Browse source 
Without this register, static hazards in the encoder could cause
multiple encoder output bits to toggle, which would be incorrectly
sampled by the 2FF synchronizer.

Reported by @Wren6991.
This commit is contained in:
whitequark 2019-03-03 18:23:51 +00:00
parent e93bf4bf4b
commit 4027317835
1 changed files with 25 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

39
nmigen/lib/fifo.py
View file

@ -297,29 +297,37 @@ class AsyncFIFO(FIFOInterface):
m = Module()
do_write = self.writable & self.we
do_read = self.readable & self.re
# TODO: extract this pattern into lib.cdc.GrayCounter
produce_w_bin = Signal(self._ctr_bits)
produce_w_nxt = Signal(self._ctr_bits)
m.d.comb += produce_w_nxt.eq(produce_w_bin + do_write)
m.d.write += produce_w_bin.eq(produce_w_nxt)
consume_r_bin = Signal(self._ctr_bits)
consume_r_nxt = Signal(self._ctr_bits)
m.d.comb += consume_r_nxt.eq(consume_r_bin + do_read)
m.d.read += consume_r_bin.eq(consume_r_nxt)
produce_w_gry = Signal(self._ctr_bits)
produce_r_gry = Signal(self._ctr_bits)
produce_enc = m.submodules.produce_enc = \
GrayEncoder(self._ctr_bits)
produce_cdc = m.submodules.produce_cdc = \
MultiReg(produce_w_gry, produce_r_gry, odomain="read")
m.d.comb += [
produce_enc.i.eq(produce_w_bin),
produce_w_gry.eq(produce_enc.o),
]
m.d.comb += produce_enc.i.eq(produce_w_nxt),
m.d.write += produce_w_gry.eq(produce_enc.o)
consume_r_bin = Signal(self._ctr_bits)
consume_r_gry = Signal(self._ctr_bits)
consume_w_gry = Signal(self._ctr_bits)
consume_enc = m.submodules.consume_enc = \
GrayEncoder(self._ctr_bits)
consume_cdc = m.submodules.consume_cdc = \
MultiReg(consume_r_gry, consume_w_gry, odomain="write")
m.d.comb += [
consume_enc.i.eq(consume_r_bin),
consume_r_gry.eq(consume_enc.o),
]
m.d.comb += consume_enc.i.eq(consume_r_nxt)
m.d.read += consume_r_gry.eq(consume_enc.o)
m.d.comb += [
self.writable.eq(
@ -329,11 +337,6 @@ class AsyncFIFO(FIFOInterface):
self.readable.eq(consume_r_gry != produce_r_gry)
]
do_write = self.writable & self.we
do_read = self.readable & self.re
m.d.write += produce_w_bin.eq(produce_w_bin + do_write)
m.d.read += consume_r_bin.eq(consume_r_bin + do_read)
storage = Memory(self.width, self.depth)
wrport = m.submodules.wrport = storage.write_port(domain="write")
rdport = m.submodules.rdport = storage.read_port (domain="read")
@ -347,6 +350,14 @@ class AsyncFIFO(FIFOInterface):
self.dout.eq(rdport.data),
]
if platform == "formal":
# TODO: move this logic elsewhere
initstate = Signal()
m.submodules += Instance("$initstate", o_Y=initstate)
with m.If(initstate):
m.d.comb += Assume(produce_w_gry == (produce_w_bin ^ produce_w_bin[1:]))
m.d.comb += Assume(consume_r_gry == (consume_r_bin ^ consume_r_bin[1:]))
return m