[libre-riscv-dev] formal proof NLnet proposal in
Luke Kenneth Casson Leighton
lkcl at lkcl.net
Mon Oct 28 20:58:01 GMT 2019
On Mon, Oct 28, 2019 at 8:43 PM Hendrik Boom <hendrik at topoi.pooq.com> wrote:
> The current technology seems to be to translate the entire circuit and
> assertions to be verified/falsified into the input for a SAT solver.
... or "other" solver, yes. it's all handled by yosis (or, symbiyosis
more specifially). symbiyosis itself does *not* do any actual formal
verification: it is *purely* a conduit through to the various back-end
solvers.
some of these are no more basic than "let's run the actual verilog for
the specified duration and check that an assert didn't happen"
> That leads to enormous SAT problems, but fortunately, they can be
> solved with current technology, usually quickly (though there was a
> mention of a formal verification that took four months! An outlier.
> Most seem to get somved in a few seconds.)
yes. four months would be someone not designing their "asserts"
properly. either that or there really was no other way.
> There seems to be no mechanism for proving theorems about components
> and using those theorems later without having to reprove them in
> context.
yep, pretty much.
so here, what we do is either:
* have a SEPARATE class (module) which contains the formal proof OR
* actually add the formal proof *TO* each module, with an "if platform
== "formal" " check.
this latter will, when that module is used inside another module,
result in the cascade-of-reproofs, creating a much larger formal proof
that *will* need to be re-run.
the former technique will of course just use the [previously-proven]
module as an [otherwise-unproven] "block". if you don't actually run
the test on the sub-modules, you're screwed.
> Which of these design languages is our project actually using?
none of them.
we are *only* using nmigen.
* nmigen gets translated from python to yosys ILANG (including Assert
and Assume statements)
* yosys takes ILANG and through symbiyosis translates and connects to
SAT solvers (multiple thereof)
we will *not* be using N.E. Other "design language", unless absolutely
forced to.
l.
More information about the libre-riscv-dev
mailing list