[libre-riscv-dev] formal proof NLnet proposal in

[Luke Kenneth Casson Leighton]

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.