-
Notifications
You must be signed in to change notification settings - Fork 175
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Fix directory for formal. #399
Conversation
Hm we check that on CI, do you have an unusual environment? No problem merging this, I'm just curious whether this hides a deeper issue. |
Hello WQ, Yehowshua from LibreSOC. I think we all had the same issue and had manually been applying |
I can give you a gist test case where it failed for me if that helps. |
Codecov Report
@@ Coverage Diff @@
## master #399 +/- ##
=======================================
Coverage 82.10% 82.10%
=======================================
Files 36 36
Lines 6075 6075
Branches 1234 1234
=======================================
Hits 4988 4988
+ Misses 914 913 -1
- Partials 173 174 +1
Continue to review full report at Codecov.
|
Are you just unable to run nMigen tests? Or were you using |
OK so here's a toy file test.py
FileNotFoundError: [Errno 2] No such file or directory: '': ''
----------------------------------------------------------------------
Ran 1 test in 0.012s
FAILED (errors=1) """
formal verification of adder.
A.K.A, we mathematically prove the adder
works.
We do this for 16 bits.
"""
from nmigen import (Module, Signal, Elaboratable, Mux, Cat, Repl,
signed)
from nmigen.asserts import Assert, AnyConst, Assume, Cover
from nmigen.test.utils import FHDLTestCase
from primitives.adder3 import Adder3
import unittest
class Adder3(Elaboratable):
def __init__(self, WIDTH):
self.PARAMS = {"WIDTH":WIDTH}
# inputs
self.A_in = Signal(signed(WIDTH))
self.B_in = Signal(signed(WIDTH))
self.C_in = Signal(signed(WIDTH))
# outputs
self.C_out = Signal(signed(WIDTH))
def elaborate(self, platform):
m = Module()
m.d.comb += self.C_out.eq(
self.A_in + self.B_in + self.C_in
)
return m
def ports(self):
return [self.A_in,
self.B_in,
self.C_in,
self.C_out]
class Driver(Elaboratable):
def __init__(self):
# no additional signals needed
pass
def elaborate(self, platform):
m = Module()
m.submodules.adder3 = adder = Adder3(WIDTH=16)
m.d.comb += [
adder.A_in.eq(AnyConst(16)),
adder.B_in.eq(AnyConst(16)),
adder.C_in.eq(AnyConst(16))
]
m.d.comb += Assert(adder.C_out == adder.A_in +
adder.B_in + adder.C_in
)
return m
class TestAdder3(FHDLTestCase):
def test_formal(self):
module = Driver()
self.assertFormal(module, mode="bmc", depth=2)
self.assertFormal(module, mode="cover", depth=2)
if __name__ == "__main__":
unittest.main() |
Only formal tests derived from the |
Its quite possible this isn't the way formal was meant to be done in nMigen(referring to the example toy code from above)? |
Right so everything under |
If you find FHDLTestCase useful please copy it into your code because it was just a quick hack I threw together in a hour as a proof of concept and it's really not intended to have any sort of stability or anything. |
Oh! ok - so how are we supposed to do formal with nMigen haha. |
There isn't an official example. nMigen has basic support for formal verification but (unlike for synthesis) it does not yet provide an out-of-box way to run |
This makes sense. Well, we do have several hundred lines of proof written using Given that only one line needs to be fixed, do you think a merge is still possible? |
Please copy the implementation of |
Ok then. Will do. |
We've actually discussed this with lkcl a few days ago. There is a certain hazard in learning something by reading its source code, namely that you might not be able to guess the intent correctly, and then you'll be unpleasantly surprised by upstream changes. This is the number one reason why documentation is top priority. |
Right. That's why we need first party documentation. nMigen is a good and useful tool none the less. |
Yep. I'm working on documentation--take a look at the |
Just now seeing this. Good deal. |
I do wonder if we copy the FHDLTestcase class, would that copy break as nmigen progresses. That is, does it depend on non-public components of nMigen? |
|
I assume you won't need |
Will do. Thanks! |
Sby formal would fail before because directory was improperly formed.