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

[Michael Pham]

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