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

[Luke Kenneth Casson Leighton]

On Monday, September 23, 2019, 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 is surprisingly straightforward for simple cases.
Google "symbiyosys" the example is pretty obvious.


> 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.


It's not - it is milestone based. We get to decide the milestones.


>
> 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


>
Yes. Exactly.



> . Still, the text provided
> gives little information about what its various provers actually do.


>
And I am not hugely concerned :) They exist, we use them. Z3, yices, etc.

Install them all, pick one later.



> 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.


Ok this is because they are not heavily optimised.

Some will take far longer than others, which, clearly, if that means "2
weeks" @ 100% CPU we have a problem.


> 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.
>
>
It is just not very commonly used except in certain industries, all under
ND. Sigh.


> I have a 16G RAM on my Purism laptop (yes, likely the same Purism that has
> showed interest in our project).


Cool!


>
> Unfortunately it has an intel processor,
> so it cannot be secure.


I am *not* going down the road of worrying about attacks on the computers.
Replicability is easy as a libre project.  A some random person runs the
tests B soneone runs the tests later on alternative hardware (e.g Tobias).



> 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.
>
>
50mb space should easily be enough. Maybe 100mb including all deoendencies.


> Or is there a system elsewhere I should be using for this?
>
>
Nope, sby is it. It is called automatically from nmigen

L.



-- 
---
crowd-funded eco-conscious hardware: https://www.crowdsupply.com/eoma68