[libre-riscv-dev] formal proof NLnet proposal in
hendrik at topoi.pooq.com
Mon Sep 23 16:03:25 BST 2019
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.
Thank you. This list looks very useful.
My previous experience (in the 80's) was with implementing a proof checker
for constructive type theory. I'm pretty sure I have the math and the
software experience I'll need to understand this stuff. The only question
is time and attention.
> ^^^ 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.
> ^^^ I also came across this blog that has some posts on formally
> verifying Western Digital's SweRV CPU.
> There might be more similar posts on the rest of the blog.
> Hope this helps you!
> -- Michael
> libre-riscv-dev mailing list
> libre-riscv-dev at lists.libre-riscv.org
More information about the libre-riscv-dev