Skip to content
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

Closed
wants to merge 1 commit into from
Closed

Fix directory for formal. #399

wants to merge 1 commit into from

Conversation

BracketMaster
Copy link

@BracketMaster BracketMaster commented Jun 3, 2020

Sby formal would fail before because directory was improperly formed.

@whitequark
Copy link
Member

whitequark commented Jun 3, 2020

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.

@BracketMaster
Copy link
Author

BracketMaster commented Jun 3, 2020

Hello WQ, Yehowshua from LibreSOC.
I have a Mac, and four other LS devs have Linux machines
from Ubuntu, Debian, to Arch.

I think we all had the same issue and had manually been applying
the patch for a few months now.

@BracketMaster
Copy link
Author

BracketMaster commented Jun 3, 2020

I can give you a gist test case where it failed for me if that helps.

@codecov
Copy link

codecov bot commented Jun 3, 2020

Codecov Report

Merging #399 into master will not change coverage.
The diff coverage is n/a.

Impacted file tree graph

@@           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     
Impacted Files Coverage Δ
nmigen/build/run.py 31.25% <0.00%> (ø)

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 9c80c32...f001612. Read the comment docs.

@whitequark
Copy link
Member

whitequark commented Jun 3, 2020

Are you just unable to run nMigen tests? Or were you using nmigen.test.utils in your own code?

@BracketMaster
Copy link
Author

BracketMaster commented Jun 3, 2020

OK so here's a toy file test.py

python3 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()

@BracketMaster
Copy link
Author

BracketMaster commented Jun 3, 2020

Are you just unable to run nMigen tests? Or were you using nmigen.test.utils in your own code?

Only formal tests derived from the FHDLTestCase class fail.
Regular pysim is fine - if that's what you're referring to.

@BracketMaster
Copy link
Author

BracketMaster commented Jun 3, 2020

Its quite possible this isn't the way formal was meant to be done in nMigen(referring to the example toy code from above)?

@whitequark
Copy link
Member

whitequark commented Jun 3, 2020

Right so everything under nmigen.test was never intended as a public API, and in particular FHDLTestCase is an internal class that I didn't realize anyone uses. I've removed tests from the PyPI packages in commit 9c80c32 to make it harder to accidentally depend on them.

@whitequark
Copy link
Member

whitequark commented Jun 3, 2020

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.

@BracketMaster
Copy link
Author

BracketMaster commented Jun 3, 2020

Oh! ok - so how are we supposed to do formal with nMigen haha.
I didn't see an official example

@whitequark
Copy link
Member

whitequark commented Jun 3, 2020

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 sby and friends, so you're supposed to do it yourself. This will improve of course.

@BracketMaster
Copy link
Author

BracketMaster commented Jun 3, 2020

This makes sense. Well, we do have several hundred lines of proof written using FHDLTestCase. I think that provides some weight to its utility.

Given that only one line needs to be fixed, do you think a merge is still possible?

@whitequark
Copy link
Member

whitequark commented Jun 3, 2020

Given that only one line needs to be fixed, do you think a merge is still possible?

Please copy the implementation of FHDLTestCase into your own code. It is not a public API, I will change it in the future without warning, and it will not be present in the PyPI packages of the next release. Having your own implementation also lets you fix any bugs you encounter, or, for example, use different solver engines.

@BracketMaster
Copy link
Author

BracketMaster commented Jun 3, 2020

Ok then. Will do.

@whitequark
Copy link
Member

whitequark commented Jun 3, 2020

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.

@BracketMaster
Copy link
Author

BracketMaster commented Jun 3, 2020

Right. That's why we need first party documentation. nMigen is a good and useful tool none the less.

@whitequark
Copy link
Member

whitequark commented Jun 3, 2020

Yep. I'm working on documentation--take a look at the doc branch. It's pretty unfinished though at the moment and not very usable yet.

@BracketMaster
Copy link
Author

BracketMaster commented Jun 3, 2020

Just now seeing this. Good deal.

@BracketMaster
Copy link
Author

BracketMaster commented Jun 3, 2020

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?

@whitequark
Copy link
Member

whitequark commented Jun 3, 2020

require_tool("sby") is also a part of the private API but you can just replace that with "sby". The rest only uses public APIs. Oh and please ditch assertRaises, assertRaisesRegex and assertWarns, the reason those methods exist is because I didn't read the unittest docs...

@whitequark
Copy link
Member

whitequark commented Jun 3, 2020

I assume you won't need assertRepr either but that one is fine.

@BracketMaster
Copy link
Author

BracketMaster commented Jun 4, 2020

Will do.

Thanks!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants