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

[Hendrik Boom]

On Mon, Oct 28, 2019 at 08:58:01PM +0000, Luke Kenneth Casson Leighton wrote:
> 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)

So I should get myself a copy of nmigen and yosys.
An maybe a passel of SAT solvers.

nmigen from https://github.com/m-labs/nmigen

yosys from https://github.com/YosysHQ/
or following instructions in
   https://symbiyosys.readthedocs.io/en/latest/quickstart.html#installing

Or are there better places?  Do we use our own modified versions?

-- hendrik

> 
> we will *not* be using N.E. Other "design language", unless absolutely
> forced to.
> 
> l.
> 
> _______________________________________________
> libre-riscv-dev mailing list
> libre-riscv-dev at lists.libre-riscv.org
> http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev