lib.fifo: register GrayEncoder output before CDC.

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.

diff --git a/nmigen/lib/fifo.py b/nmigen/lib/fifo.py
index 3af5c511ffcdacba0107991a77f9a831347b9428..e484ec8c64bd876e94f0ceb8e35ef0a33e00483f 100644 (file)
--- a/nmigen/lib/fifo.py
+++ b/nmigen/lib/fifo.py
@@ -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