[libre-riscv-dev] formal verification
hendrik at topoi.pooq.com
Sat Mar 2 16:10:31 GMT 2019
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
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.
> On Wed, Feb 27, 2019, 08:05 Luke Kenneth Casson Leighton <lkcl at lkcl.net>
> > ---
> > 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
More information about the libre-riscv-dev