From: awygle Date: Sat, 14 Mar 2020 23:26:07 +0000 (-0700) Subject: Correctly handle resets in AsyncFIFO. X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=07d36b658090d073801955106c051dc5017b17f6;p=nmigen.git Correctly handle resets in AsyncFIFO. This commit improves handling of resets in AsyncFIFO in two ways: * First, resets no longer violate Gray counter CDC invariants. * Second, write domain reset now empties the entire FIFO. --- diff --git a/nmigen/hdl/cd.py b/nmigen/hdl/cd.py index cd08929..96af20c 100644 --- a/nmigen/hdl/cd.py +++ b/nmigen/hdl/cd.py @@ -21,7 +21,7 @@ class ClockDomain: If ``True``, the domain does not use a reset signal. Registers within this domain are still all initialized to their reset state once, e.g. through Verilog `"initial"` statements. - clock_edge : str + clk_edge : str The edge of the clock signal on which signals are sampled. Must be one of "pos" or "neg". async_reset : bool If ``True``, the domain uses an asynchronous reset, and registers within this domain diff --git a/nmigen/lib/fifo.py b/nmigen/lib/fifo.py index ee3fb5c..17d86c8 100644 --- a/nmigen/lib/fifo.py +++ b/nmigen/lib/fifo.py @@ -3,8 +3,8 @@ from .. import * from ..asserts import * from .._utils import log2_int, deprecated -from .coding import GrayEncoder -from .cdc import FFSynchronizer +from .coding import GrayEncoder, GrayDecoder +from .cdc import FFSynchronizer, AsyncFFSynchronizer __all__ = ["FIFOInterface", "SyncFIFO", "SyncFIFOBuffered", "AsyncFIFO", "AsyncFIFOBuffered"] @@ -261,6 +261,10 @@ class AsyncFIFO(Elaboratable, FIFOInterface): Read and write interfaces are accessed from different clock domains, which can be set when constructing the FIFO. + :class:`AsyncFIFO` can be reset from the write clock domain. When the write domain reset is + asserted, the FIFO becomes empty. When the read domain is reset, data remains in the FIFO - the + read domain logic should correctly handle this case. + :class:`AsyncFIFO` only supports power of 2 depths. Unless ``exact_depth`` is specified, the ``depth`` parameter is rounded up to the next power of 2. """.strip(), @@ -317,7 +321,8 @@ class AsyncFIFO(Elaboratable, FIFOInterface): m.d.comb += produce_w_nxt.eq(produce_w_bin + do_write) m.d[self._w_domain] += produce_w_bin.eq(produce_w_nxt) - consume_r_bin = Signal(self._ctr_bits) + # Note: Both read-domain counters must be reset_less (see comments below) + consume_r_bin = Signal(self._ctr_bits, reset_less=True) consume_r_nxt = Signal(self._ctr_bits) m.d.comb += consume_r_nxt.eq(consume_r_bin + do_read) m.d[self._r_domain] += consume_r_bin.eq(consume_r_nxt) @@ -331,7 +336,7 @@ class AsyncFIFO(Elaboratable, FIFOInterface): m.d.comb += produce_enc.i.eq(produce_w_nxt), m.d[self._w_domain] += produce_w_gry.eq(produce_enc.o) - consume_r_gry = Signal(self._ctr_bits) + consume_r_gry = Signal(self._ctr_bits, reset_less=True) consume_w_gry = Signal(self._ctr_bits) consume_enc = m.submodules.consume_enc = \ GrayEncoder(self._ctr_bits) @@ -366,6 +371,34 @@ class AsyncFIFO(Elaboratable, FIFOInterface): self.r_rdy.eq(~r_empty), ] + # Reset handling to maintain FIFO and CDC invariants in the presence of a write-domain + # reset. + # There is a CDC hazard associated with resetting an async FIFO - Gray code counters which + # are reset to 0 violate their Gray code invariant. One way to handle this is to ensure + # that both sides of the FIFO are asynchronously reset by the same signal. We adopt a + # slight variation on this approach - reset control rests entirely with the write domain. + # The write domain's reset signal is used to asynchronously reset the read domain's + # counters and force the FIFO to be empty when the write domain's reset is asserted. + # This requires the two read domain counters to be marked as "reset_less", as they are + # reset through another mechanism. See https://github.com/nmigen/nmigen/issues/181 for the + # full discussion. + w_rst = ResetSignal(domain=self._w_domain, allow_reset_less=True) + r_rst = Signal() + + # Async-set-sync-release synchronizer avoids CDC hazards + rst_cdc = m.submodules.rst_cdc = \ + AsyncFFSynchronizer(w_rst, r_rst, domain=self._r_domain) + + # Decode Gray code counter synchronized from write domain to overwrite binary + # counter in read domain. + rst_dec = m.submodules.rst_dec = \ + GrayDecoder(self._ctr_bits) + m.d.comb += rst_dec.i.eq(produce_r_gry), + with m.If(r_rst): + m.d.comb += r_empty.eq(1) + m.d[self._r_domain] += consume_r_gry.eq(produce_r_gry) + m.d[self._r_domain] += consume_r_bin.eq(rst_dec.o) + if platform == "formal": with m.If(Initial()): m.d.comb += Assume(produce_w_gry == (produce_w_bin ^ produce_w_bin[1:])) diff --git a/nmigen/test/test_lib_fifo.py b/nmigen/test/test_lib_fifo.py index 38019f9..29a28d8 100644 --- a/nmigen/test/test_lib_fifo.py +++ b/nmigen/test/test_lib_fifo.py @@ -220,6 +220,9 @@ class FIFOContractSpec(Elaboratable): with m.If(Past(Initial(), self.bound - 1)): m.d.comb += Assert(read_fsm.ongoing("DONE")) + with m.If(ResetSignal(domain=self.w_domain)): + m.d.comb += Assert(~fifo.r_rdy) + if self.w_domain != "sync" or self.r_domain != "sync": m.d.comb += Assume(Rose(ClockSignal(self.w_domain)) | Rose(ClockSignal(self.r_domain)))