Formal Platform Integration

[cr1901]

Right now, the scope of formal is the following, copied directly from IRC:

(11:56:43 AM) whitequark: the entire scope of formal verification in nmigen at the moment is "it can generate verilog or rtlil with assert/assume statements" (11:57:10 AM) whitequark: i do not, at the moment, provide anything beyond that, and doing it requires thinking first and coding second

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 an Elaboratable in nmigen will be of comparable complexity to synthesizing and programming a bitstream via nmigen.build.plat.Platform.build(). Formal (in symbiyosys, 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 a Fragment or Module (Elaboratable). See above.

• Per IRC, a formal Platform is probably desirable. Current approach is to inject platform=formal into rtlil/verilog.convert() or similar instead of using nmigen.build. I have some thoughts here:

  • I think it's reasonable that rtlil/verilog.convert() on it's own either emits or excludes asserts/assumes via an option.
  • My gut feeling tells that building 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:
  • I would still like the ability to easily clean up formal output artifacts without them intermingling with synthesis output artifacts; for instance, invoking via sby -d sby_dir formal.sby.
  • Input artifact mingling should also be kept to a minimum. A minimum set of inputs affected by emitting for both formal ans synthesis might be: the sby file, one set of .il/v input for synthesis w/o asserts/assumes, and another set of .il/v for sby.

• 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:

  reg last_clk = 0;
  
  always @($global_clock) begin
      last_clk <= clk;
      assume(last_clk != clk);
  end

  When we discussed $global_clock last year, we agreed to not expose $global_clock within nmigen, 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 "all n clocks must have ticked at least once in the past n cycles" might work?). I think we should review this.

[whitequark]

• Minimal hassle to invoke symbiyosys that "does the right thing" on a Fragment or Module (Elaboratable).

It's not clear that there is a single "right way" to invoke sby. It has a lot of configuration options and those are not just for show, you actually have to tweak them to get the right kind of proof, to have the proof finish in reasonable time, etc.

• I think it's reasonable that rtlil/verilog.convert() on it's own either emits or excludes asserts/assumes via an option.

This should almost certainly be done before converting for several reasons:

• We have a problem with elaboration speed. The best way to fix it is to not generate something that will be immediately thrown away.
• When you emit an Assert statement you also often emit some supporting logic for it: intermediate signals, control flow, and so on. If this was done in rtlil.convert then all of the supporting logic would remain.

This should be done by interrogating the platform during elaboration, through something like platform.has_assertions.

• My gut feeling tells that building 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.

What do you mean by "mutually exclusive"?

• Multiclock support.

I propose we leave multiclock out of an initial implementation.

[awygle]

It's not clear that there is a single "right way" to invoke sby. It has a lot of configuration options and those are not just for show, you actually have to tweak them to get the right kind of proof, to have the proof finish in reasonable time, etc.

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.

I propose we leave multiclock support out of an initial implementation.

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.

• Per IRC, a formal Platform is probably desirable.

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 FHDLTestCase, which abstracts over the sby interface. At a slightly higher level, it would be cool to have a SafetyPropertyCase and a LivenessPropertyCase which inherit from FHDLTestCase's replacement and perhaps also unittest.UnitTest, where you can set up a DUT once and define formal properties on it as several independent functions which are then managed properly on the backend (with multiple sby calls for Liveness properties and a single sby call for Safety ones). I'm not sure how feasible the above is from a Python standpoint, but it's the sort of interface I wish I had currently.

[whitequark]

I'd like to see this coupled with simulation Platforms as well.

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.

At a slightly higher level, it would be cool to have a SafetyPropertyCase and a LivenessPropertyCase which inherit from FHDLTestCase's replacement and perhaps also unittest.UnitTest,

I think we really shouldn't tie ourselves to unittest. Like many other things in the standard library, it's not all that good (unittest is just a straight port from Java and it doesn't even follow PEP8!), and there are multiple replacements downstream. It should be easy enough to write formal test cases with any testing framework, though of course we can provide a premade adapter for unittest.

[awygle]

It's not entirely clear what a formal/simulation platform would do.

I think the goal should be that simulations and proofs should Just Work, even if the DUT in question uses platform. Before any of the changes discussed here, this basically means giving you whatever I/O you request, no questions asked, in a usefully simulable way, to the greatest extent possible. The current situation where platform is passed to every Elaboratable, but I can't use it if I want to do simulations so I have to either pass Signals into __init__ or have a bunch of if platform:s to do a purely mechanical translation to sim constructs, seems kind of odd. This honestly has almost nothing to do with formal though so maybe not the best fit for this issue.

I think we really shouldn't tie ourselves to unittest

That's fine, I have no dog in that race, I just want it to run when I do python3 -m pytest tests/.

[whitequark]

Before any of the changes discussed here, this basically means giving you whatever I/O you request, no questions asked, in a usefully simulable way, to the greatest extent possible.

There are two issues here:

• I don't understand how this can happen as described because the result of request completely depends on the resources added to the platform, and the resource mechanism is tied to packages and pins. So we'll have to come up with something substantially different.
• If I'm simulating or verifying a FIFO I definitely do not want any sort of I/O to be involved. So a simulation/formal platform shouldn't always involve I/O, which means that it can't rely on I/O being present, which means it can't e.g. optimize out everything not transitively connected to I/O.

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.

[cr1901]

What do you mean by "mutually exclusive"?

What I meant by this is: pretend for a second that in addition to platform.has_assertions you have platform.has_synthesis. The property would describe whether the build method for that platform generated artifacts for synthesis (as well as running the synth toolchain if do_build is True, etc).

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.

[whitequark]

if a platform has assertions, then that platform can't be used for synthesis

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.

[cr1901]

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 sby and a synthesis toolchain- you must pick one or the other".

[whitequark]

a single platform cannot generate input files for sby and a synthesis toolchain- you must pick one or the other

So this isn't inherently unreasonable, but nmigen.build doesn't generate files. It generates build plans, which are just Python objects (essentially a dictionary). Those can be extracted into files and run locally or remotely. You've mentioned that you want to avoid artifact mingling, but there isn't any in first place, any more than there is artifact mingling when you synthesize two different designs (using two different toolchains, even) in a single build directory. It just happens that the default build directory is build.

[cr1901]

You've mentioned that you want to avoid artifact mingling, but there isn't any in first place, any more than there is artifact mingling when you synthesize two different designs (using two different toolchains, even) in a single build directory.

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 nmigen is calling sby via subprocess, but that's a bikeshed I'm not particularly attached to.

[cr1901]

As for your other points:

It's not clear that there is a single "right way" to invoke sby. It has a lot of configuration options and those are not just for show, you actually have to tweak them to get the right kind of proof, to have the proof finish in reasonable time, etc.

I'll let others chime in with what they want. FWIW, the assertFormal function, minus the hybrid mode, essentially does what I would consider to be "the right thing" with minimal tweaking. But indeed my experience not typical.

I think it's reasonable that rtlil/verilog.convert() on it's own either emits or excludes asserts/assumes via an option. This should almost certainly be done before converting for several reasons:

We have a problem with elaboration speed. The best way to fix it is to not generate something that will be immediately thrown >away. When you emit an Assert statement you also often emit some supporting logic for it: intermediate signals, control flow, and so >on. If this was done in rtlil.convert then all of the supporting logic would remain.

Ack. This approach still gives users the option to use the convert functions and get asserts/assumes if they so desire.

I propose we leave multiclock out of an initial implementation.

Ack.

[anuejn]

Just as a side note: We probably want to be able to use the new formal method in parallel unit tests. The current implementation does not always allow that which can be fixed with a dirty hack for the nmigen codebase but not for the general case (see #511). Only to keep parallelism in mind when designing a new formal test helper.

[cr1901]

I propose we leave multiclock out of an initial implementation.

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" assumes, even if nmigen can't/shouldn't generate these assumes automatically¹. If your design's FSM has any loops² that are unreachable from the initial state, the SMT solver will be able to generate a counterexample of arbitrary length during k-induction.

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.

1. multiclock being the exception, since AFAIK $global_clock still shouldn't be exposed.
2. Such as returning to the same state for the next time step, equivalent to "do nothing".

[whitequark]

I'm not entirely sure why CXXRTL would be involved?

[cr1901]

I'm not entirely sure why CXXRTL would be involved?

Incomplete thought, not important. Meant to edit it out.