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

[Hendrik Boom]

On Mon, Sep 23, 2019 at 10:06:59AM -0400, Michael Pham wrote:
> On Mon, Sep 23, 2019 at 7:32 AM Hendrik Boom <hendrik at topoi.pooq.com> wrote:
> >
> > On Mon, Sep 23, 2019 at 03:58:54AM +0100, Luke Kenneth Casson Leighton wrote:
> > > https://libre-riscv.org/nlnet_2019_formal/
> > >
> > > submitted.  this is a proposal that we adopt formal mathematical
> > > proofs as the "default" unit test, exactly as samuel falvo did.  does.
> > > and receive funds for doing so.
> >
> > I'm not familiar with current work on hardware verification, but I find
> > myself doubtful of this project.  My experience with formal verification
> > (admittedly dating back to the late 80's) indicates that it is very
> > difficult.
> >
> > It's possible that SymbiYosys takes advantage of typical hardware coding
> > patterns to greatly simplify and automate the entire process, but I'd be
> > wary of committing to a project of this scale for pay if the pay is only
> > available when the entire project is finished.
> >
> > That said, I'm willing to have a look at the problem and see what I can do
> > in my so-called spare time.
> >
> > The links in the project proposal give me somewhat more information about
> > the SymbiYosys.  It appears to be a framework for xressing assertions and
> > calling on independently written theorem provers. Still, the text provided
> > gives little information about what its various provers actually do.  It
> > suggests trying them out on sample problems to get a feeling for them.
> > "Trial and error can also be a useful method for evaluating engines."
> > (https://symbiyosys.readthedocs.io/en/latest/quickstart.html#selecting-the-right-engine)
> >
> > But I do have doubts about using "feelings" when doing formal verification.
> >
> > The links I see to code repositories for these provers don't seem to reach
> > much in the way of documentation.  But maybe that's because I'm unfmiliar
> > with bitbucket and I have to actually install them before I see any.
> >
> > I have a 16G RAM on my Purism laptop (yes, likely the same Purism that has
> > showed interest in our project).  Unfortunately it has an intel processor,
> > so it cannot be secure.
> >
> > Sometime in the next few weeks I'll try installing this stuff and see what
> > happens.  I'll get a larger hard drive if necessary.
> >
> > Or is there a system elsewhere I should be using for this?
> >
> > -- hendrik
> >
> 
> Hi Hendrik,
> 
> I found a few resources for hardware formal verification. You and Luke
> and Jacob and others might be interested in using these to learn how
> others in the RISC-V community are doing it.
> 
> http://zipcpu.com/tutorial/
> ^^^ This one is the most comprehensive one. Actually it's an entire
> course on how to do formal verification! Tutorials, exercises, quizzes
> are provided for free (make sure to look to at the 400+ page pdf that
> teaches you from start to end the process). I recommend checking out
> the rest of the website on a desktop browser because there are some
> formatting issues on my phone.
> 
> https://tomverbeure.github.io/
> ^^^ I also came across this blog that has some posts on formally
> verifying Western Digital's SweRV CPU.
> 
> https://tomverbeure.github.io/risc-v/2018/11/19/A-Bug-Free-RISC-V-Core-without-Simulation.html
> 
> https://tomverbeure.github.io/rtl/2019/01/04/Under-the-Hood-of-Formal-Verification.html
> 
> There might be more similar posts on the rest of the blog.
> 
> Hope this helps you!
> 
> -- Michael

Thank you.  It does.  I've started going through those links.

The current technology seems to be to translate the entire circuit and 
assertions to be verified/falsified into the input for a SAT solver.  
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.)

There seems to be no mechanism for proving theorems about components 
and using those theorems later without having to reprove them in 
context.

I will proceed further.

Which of these design languages is our project actually using?

-- hendrik

> 
> _______________________________________________
> libre-riscv-dev mailing list
> libre-riscv-dev at lists.libre-riscv.org
> http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev