From a5bfe8eed88236efe205c6937e8af9f5bfdb6187 Mon Sep 17 00:00:00 2001
From: whitequark <cz@m-labs.hk>
Date: Sun, 3 Mar 2019 18:23:51 +0000
Subject: [PATCH] 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.
---
 nmigen/lib/fifo.py | 39 +++++++++++++++++++++++++--------------
 1 file changed, 25 insertions(+), 14 deletions(-)

diff --git a/nmigen/lib/fifo.py b/nmigen/lib/fifo.py
index 3af5c51..e484ec8 100644
--- 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
 
 
-- 
2.30.2