[libre-riscv-dev] formal verification

[Hendrik Boom]

On Wed, Feb 27, 2019 at 10:08:50AM -0800, Jacob Lifshay wrote:
> I was planning on formally verifying the FP alus, then we can use
> riscv-formal to help us formally verify the whole core. Help would
> definitely be appreciated as I have no experience in formal verification of
> hardware. I was thinking of trying to use yosys to do formal verification
> as, if I recall correctly, it integrates with the Z3 solver.

I've been reading links.  It's starting to look like fun.
But I have no experience either in formal verification of hardware.
I did do some formal verification of a lazy-evaluation language, but that
was three decades ago on a machine with an enormous mamory -- a full 5 
megabytes!

Now i have only 16 gig on my laptop.  How times have changed.

Not sure how long what I'm reading needs to stew in my unconscious to feel 
comfortable with it.

-- hendrik

>
> Jacob
> 
> On Wed, Feb 27, 2019, 08:05 Luke Kenneth Casson Leighton <lkcl at lkcl.net>
> wrote:
> 
> > ---
> > crowd-funded eco-conscious hardware: https://www.crowdsupply.com/eoma68
> >
> > On Wed, Feb 27, 2019 at 2:46 PM Hendrik Boom <hendrik at topoi.pooq.com>
> > wrote:
> >
> > > Formal verification means to produce a machine-checked mathematical
> > > proof of correctness.
> > >
> > > It's not trivial to do.
> >
> >  indeed.  it's why bluespec decided to write a formal spec in BSV,
> > which as you no doubt know is written in haskell.  valid programs
> > written in BSV that compile successfully to verilog are formally
> > *guaranteed* mathematically 100% to be synthesiseable.
> >
> >  honestly don't know the answer here: therefore, your help really
> > appreciated.
> >
> > l.
> >
> > _______________________________________________
> > libre-riscv-dev mailing list
> > libre-riscv-dev at lists.libre-riscv.org
> > http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev
> >
> _______________________________________________
> libre-riscv-dev mailing list
> libre-riscv-dev at lists.libre-riscv.org
> http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev