[libre-riscv-dev] formal verification

[Jacob Lifshay]

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.

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
>