Comment by Wren6991
Sunday Mar 03, 2019 at 16:12 GMT

Yep looks like I've broken something :D Will update once I've got formal running on my own machine, and fixed the issue.

from amaranth.

Comment by Wren6991
Sunday Mar 03, 2019 at 16:58 GMT

The reset values look nonsensical to me, e.g. 010 (bin) != 010 (gray). Maybe the fact it passed before was a lucky break due to the bin and gray pointers being driven by the same register, so their initial values were correct. I need to dig into this formal stuff more. Note: it fails during BMC.

from amaranth.

Comment by codecov[bot]
Sunday Mar 03, 2019 at 17:18 GMT

Codecov Report

Merging #38 into master will increase coverage by 0.05%.
The diff coverage is 100%.

@@            Coverage Diff             @@
##           master      #38      +/-   ##
==========================================
+ Coverage   85.52%   85.57%   +0.05%     
==========================================
  Files          27       27              
  Lines        3918     3932      +14     
  Branches      765      765              
==========================================
+ Hits         3351     3365      +14     
  Misses        478      478              
  Partials       89       89

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 342bdbe...6b30637. Read the comment docs.

from amaranth.

Comment by Wren6991
Sunday Mar 03, 2019 at 17:21 GMT

I've added an additional commit which asserts FIFO resets whilst $initstate is true, in FIFOContractSpec. On my machine I can now run coverage run -m unittest discover and all tests pass.

Since this fix is outside the scope of this PR, I am happy to open a separate one if you would prefer.

from amaranth.

Comment by whitequark
Sunday Mar 03, 2019 at 17:25 GMT

First, thanks for finding the bug! This is indeed very important, and I'm not sure how I missed it. It is definitely not present in Migen, it's an nMigen bug.

I've added an additional commit which asserts FIFO resets whilst $initstate is true, in FIFOContractSpec. On my machine I can now run coverage run -m unittest discover and all tests pass.

Unfortunately you've significantly weakened the contract by adding a reset. Before your changes, the FIFO contract would test an arbitrary initial state (any block RAM contents and any pointers). After your changes the initial state is always defined, so e.g. a FIFO that would pass just two elements through it and then hang would pass it.

from amaranth.

Comment by whitequark
Sunday Mar 03, 2019 at 17:31 GMT

Can you check if the following diff also fixes the bug, please?

diff --git a/nmigen/lib/fifo.py b/nmigen/lib/fifo.py
index 3af5c51..d4f16e1 100644
--- a/nmigen/lib/fifo.py
+++ b/nmigen/lib/fifo.py
@@ -304,10 +304,8 @@ class AsyncFIFO(FIFOInterface):
             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_bin)
+        m.d.write += produce_w_gry.eq(produce_enc.o)
 
         consume_r_bin = Signal(self._ctr_bits)
         consume_r_gry = Signal(self._ctr_bits)
@@ -316,17 +314,15 @@ class AsyncFIFO(FIFOInterface):
             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_bin)
+        m.d.read  += consume_r_gry.eq(consume_enc.o)
 
         m.d.comb += [
             self.writable.eq(
-                (produce_w_gry[-1]  == consume_w_gry[-1]) |
-                (produce_w_gry[-2]  == consume_w_gry[-2]) |
-                (produce_w_gry[:-2] != consume_w_gry[:-2])),
-            self.readable.eq(consume_r_gry != produce_r_gry)
+                (produce_enc.o[-1]  == consume_w_gry[-1]) |
+                (produce_enc.o[-2]  == consume_w_gry[-2]) |
+                (produce_enc.o[:-2] != consume_w_gry[:-2])),
+            self.readable.eq(consume_enc.o != produce_r_gry)
         ]
 
         do_write = self.writable & self.we
diff --git a/nmigen/test/test_lib_fifo.py b/nmigen/test/test_lib_fifo.py
index c7f4c28..e70d7be 100644
--- a/nmigen/test/test_lib_fifo.py
+++ b/nmigen/test/test_lib_fifo.py
@@ -262,8 +262,8 @@ class FIFOFormalCase(FHDLTestCase):
         # self.assertFormal(FIFOModelEquivalenceSpec(fifo, rdomain="read", wdomain="write"),
         #                   mode="bmc", depth=fifo.depth * 3 + 1)
         self.assertFormal(FIFOContractSpec(fifo, rdomain="read", wdomain="write",
-                                           bound=fifo.depth * 4 + 1),
-                          mode="hybrid", depth=fifo.depth * 4 + 1)
+                                           bound=(fifo.depth + 1) * 4),
+                          mode="hybrid", depth=(fifo.depth + 1) * 4)
 
     def test_async(self):
         self.check_async_fifo(AsyncFIFO(width=8, depth=4))

from amaranth.

Comment by Wren6991
Sunday Mar 03, 2019 at 17:32 GMT

I'm not sure how I missed it

Possibly distracted by CC's name!

Unfortunately you've significantly weakened the contract by adding a reset. Before your changes, the FIFO contract would test an arbitrary initial state (any block RAM contents and any pointers). After your changes the initial state is always defined, so e.g. a FIFO that would pass just two elements through it and then hang would pass it.

Ah okay, I see the problem.

Wouldn't you normally test this with a separate induction pass? The failure I saw was due to the design starting in an unreachable state. You are talking about reachable states, which should be testable by induction after a sufficiently long BMC. I haven't used SymbiYosys before, but have used yosys-smtbmc with a different solver backend, and always performed BMC followed by induction.

from amaranth.

Comment by whitequark
Sunday Mar 03, 2019 at 17:33 GMT

Wouldn't you normally test this with a separate induction pass?

Yes, but I never got induction to work on all the FIFO designs. This oddball BMC is the best I could do.

from amaranth.

Comment by Wren6991
Sunday Mar 03, 2019 at 17:41 GMT

That diff fixes the bug, but does introduce an extra cycle of latency in each direction. Immediate problem is defused :)

Yes, but I never got induction to work on all the FIFO designs. This oddball BMC is the best I could do.

Sounds like your experience with formal has been similar to mine... if this would be a valuable thing then I can have a play with it. It would be nice at some point in the future to win back that additional latency cycle, without breaking the test!

Thank you for taking a look at my patch.

from amaranth.

Comment by whitequark
Sunday Mar 03, 2019 at 17:56 GMT

That diff fixes the bug, but does introduce an extra cycle of latency in each direction. Immediate problem is defused :)

Oh, I see! I will do something about it. Thanks for pointing out!

• Currently I'm passing the domain name into the __init__ of this class, like MultiReg, but I saw references elsewhere to the DomainRenamer class, which seems cleaner. However it seems you can only call this on Fragments, not Modules, and I currently don't know what a Fragment is :)

This is an open issue, #29. For now I will do the copy-pastey thing.

from amaranth.

Comment by Wren6991
Sunday Mar 03, 2019 at 18:16 GMT

This is an open issue, #29. For now I will do the copy-pastey thing.

Ah okay. I had a quick look at that area of code (Module etc) and decided I needed to learn some GoF patterns first!

If it's any help at all, this is what my "flat" patch looked like: link to commit

But this had the same issue with the FIFO contract test.

from amaranth.

Comment by whitequark
Sunday Mar 03, 2019 at 18:17 GMT

I had a quick look at that area of code (Module etc) and decided I needed to learn some GoF patterns first!

I'm not really a huge fan of GoF. That code doesn't need patterns so much as one horrible hack, and I can't decide exactly how horrible it's going to be. So it's not done just yet.

from amaranth.

Comment by whitequark
Sunday Mar 03, 2019 at 18:24 GMT

Fixed by 4027317, without any added latency. I've solved this properly by adding appropriate Assumes. You are right that this pattern should be extracted into a GrayCounter; it was in Migen, but I did not understand exactly why.

from amaranth.