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.

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

nmigen/lib/fifo.py

@@ -3,8 +3,8 @@
 from .. import *
 from ..asserts import *
 from .._utils import log2_int, deprecated
-from .coding import GrayEncoder
+from .coding import GrayEncoder, GrayDecoder
-from .cdc import FFSynchronizer
+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:]))

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)))