Comments (13)
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 is100%
.
@@ 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
Impacted Files | Coverage Δ | |
---|---|---|
nmigen/lib/fifo.py | 98.78% <100%> (+0.11%) |
⬆️ |
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 runcoverage 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, likeMultiReg
, but I saw references elsewhere to theDomainRenamer
class, which seems cleaner. However it seems you can only call this onFragment
s, notModules
, and I currently don't know what aFragment
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 Assume
s. 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.
Related Issues (20)
- Unclear error message on `m.domains.cd_tx = ClockDomain()`
- Can't emit Verilog/RTLIL with Signature array members HOT 1
- Add `AMDPlatform`, aliasing `XilinxPlatform`
- Make `Module` explode if you try to modify it after it's elaborated
- Extremely slow Verilog generation HOT 5
- Pysim should reject async generators
- Constraint generation from platform resource with `DiffPairs` of type LVDS incorrect. HOT 1
- Adding simulator processes after starting the simulation is not well-defined HOT 2
- Indexing into signals with layouts could be improved HOT 1
- `AttributeError` caused by `UnusedElaboratable` after an elaboratable has failed its initialization HOT 1
- `create_missing_domain` uses `platform.request()` in deprecated mode in all platforms
- Views with an array layout should have `len()` applicable to them
- `stream.Signature` should allow setting the init value for the payload HOT 4
- Views with an array layout should be indexable with a slice HOT 1
- VCD files do not display glitches and can get extremely confusing HOT 2
- Unshaped enumeration values don't work when used in a constant initializer
- Allow comparison of `data.Const` with `dict` and `list`
- Warn after simulation ends if a domain's clock isn't driven by either logic or testbench
- Add a way to have fine grained control over `oe` for `io.Buffer`, `io.FFBuffer`, `io.DDRBuffer` HOT 2
- Add a `PortLike` that can be used in simulation to test designs which instantiate I/O buffers HOT 2
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from amaranth.