-
Notifications
You must be signed in to change notification settings - Fork 177
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
Formal Platform Integration #505
Comments
It's not clear that there is a single "right way" to invoke
This should almost certainly be done before converting for several reasons:
This should be done by interrogating the platform during elaboration, through something like
What do you mean by "mutually exclusive"?
I propose we leave multiclock out of an initial implementation. |
I think a reasonable default isn't too hard to come by - mode, engine, steps would handle everything I've ever done and would make a decent initial pass, IMO.
It's hard not to agree with this, but I do want to say that multiclock is going to be required in a lot of use cases, and ideally we wouldn't leave it cooking for too long after the MVP.
I'd like to see this coupled with simulation Platforms as well. In imagining what would be a nice interface to formal in nmigen, in particular in the testing context, I picture three components. At the base level, something akin to |
It's not entirely clear what a formal/simulation platform would do. Currently, the main job of a platform is to handle I/O and toolchain integration. With sby formal as well as pysim/cxxsim, toolchain integration is built into nMigen itself, and there's no I/O to speak of.
I think we really shouldn't tie ourselves to |
I think the goal should be that simulations and proofs should Just Work, even if the DUT in question uses
That's fine, I have no dog in that race, I just want it to run when I do |
There are two issues here:
In general people request a simulation/formal platform very often but I've yet to see any coherent idea of how it would actually work. |
What I meant by this is: pretend for a second that in addition to I think those two should be mutually-exclusive (if a platform has assertions, then that platform can't be used for synthesis). I don't know why you would want to do both at the same time, but it was something on my mind as I wrote the original issue. |
Oh. But it would actually be really nice if assertions could be used for synthesis, because then it could guide synthesis (the way assertions in Rust code allow the compiler to eliminate bounds checks). Unfortunately I don't think any existing synthesizer can do it, but it seems strange to specifically exclude it in principle. |
Hmmm, that's fair, and it doesn't really conflict with my desire to avoid an explosion of input/output files generated. Maybe my above comment could be modified to: "a single platform cannot generate input files for |
So this isn't inherently unreasonable, but |
Yea, I see this now/I forgot that build plan was kept in memory (and it has to be for stuff like remote builds to work). I'm fine w/ nmigen's behavior. I still think I'd like sby to be invoked with a build dir argument if |
As for your other points:
I'll let others chime in with what they want. FWIW, the
Ack. This approach still gives users the option to use the
Ack. |
Just as a side note: We probably want to be able to use the new formal method in parallel unit tests. |
Recently, I've been running into similar problems with the SMT solver "holding the circuit in a single state to force a counterexample" in designs with a single clock domain. I also mentioned in a follow up comment that "it's not a guarantee that you'll need assumes to 'force-forward progress'" in multiclock designs (well, single clock designs now too :)). I think it might be possible for nmigen to detect when you'll need "force-forward progress" How difficult would it be to generate the set of all possible FSM transitions in an nmigen design (I don't specify how this should be done), find all reachable states from the initial state, and detect loops outside of this set? nmigen could then warn "k-induction is likely to fail no matter what induction length you use", before you waste time trying to debug this.
|
I'm not entirely sure why CXXRTL would be involved? |
Incomplete thought, not important. Meant to edit it out. |
Right now, the scope of formal is the following, copied directly from IRC:
This is a pre-RFC to discuss what other functionality we'd want out of formal integration. Specifically, I'm assuming an end goal will be something along the lines of:
Given a test harness w/
assert
/assume
and a design w/assert
/assume
statements, running a formal verification flow of anElaboratable
innmigen
will be of comparable complexity to synthesizing and programming a bitstream vianmigen.build.plat.Platform.build()
. Formal (insymbiyosys
, either Bounded Model Check (BMC) and/or k-induction)To start, I can think of at least three things I want:
Minimal hassle to invoke
symbiyosys
that "does the right thing" on aFragment
orModule
(Elaboratable
). See above.Per IRC, a formal
Platform
is probably desirable. Current approach is to injectplatform=formal
intortlil/verilog.convert()
or similar instead of usingnmigen.build
. I have some thoughts here:rtlil/verilog.convert()
on it's own either emits or excludesassert
s/assume
s via an option.build
ing for a platform which has assertions and synthesizing a bitstream should be mutually exclusive because synth and formal are meant to do two different tasks. Failing that:sby -d sby_dir formal.sby
.sby
file, one set of.il
/v
input for synthesis w/oassert
s/assume
s, and another set of.il
/v
forsby
.Multiclock support. This one is tougher, it's easy to make a design w/ multiclock fail because the solver will hold one of the clocks steady to prevent forward progress (when a constraint violation is imminent) until
n
timesteps have elapsed. One way around this is to utilize the$global_clock
clock and do something like this for each clock to force each clock to eventually tick:When we discussed
$global_clock
last year, we agreed to not expose$global_clock
withinnmigen
, but we couldn't come up with a good set of constraints that should be autogenerated for formal testbenches with multiple clocks to force forward progress (I think "alln
clocks must have ticked at least once in the pastn
cycles" might work?). I think we should review this.The text was updated successfully, but these errors were encountered: