[libre-riscv-dev] formal proof NLnet proposal in
hendrik at topoi.pooq.com
Tue Oct 29 02:31:35 GMT 2019
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
> 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
Or are there better places? Do we use our own modified versions?
> we will *not* be using N.E. Other "design language", unless absolutely
> forced to.
> libre-riscv-dev mailing list
> libre-riscv-dev at lists.libre-riscv.org
More information about the libre-riscv-dev