[libre-riscv-dev] formal verification

[Jacob Lifshay]

On Sun, Mar 3, 2019, 10:53 Luke Kenneth Casson Leighton <lkcl at lkcl.net>
wrote:

> On Sat, Mar 2, 2019 at 4:10 PM Hendrik Boom <hendrik at topoi.pooq.com>
> wrote:
> >
> > 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.
>
>  well the important thing to appreciate here is: the hardware is
> written *as* a software program, with a full simulation environment as
> part of nmigen.  therefore you would in effect be verifying a
> *software* program.
>
>  the next phase would obviously be to do a formal verification of
> nmigen's simulation technology being a direct one-to-one
> correspondance with actual hardware, however that can be tackled as a
> *separate* task.
>

I was thinking we'd convert to verilog then formally verify the verilog
using yosys. I'd assume that the verilog compiler is correct.

>
> > 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.
>
>  only?? pffh.
>
I have a laptop that has 8MB of ram and a 486 (haven't been able to boot
Linux on it due to OOM and only a floppy drive for removable storage,
though I did get a 3D renderer running on FreeDOS using djgpp), though my
laptop that I actually use has 16G and my desktop has 24G.

Btw, was looking at servers on ebay recently and there are some with 8
cores and 32G of ram for less than $100. was thinking it would make a good
CI build server.

>
> > Not sure how long what I'm reading needs to stew in my unconscious to
> feel
> > comfortable with it.
>
>  :)
>
> _______________________________________________
> libre-riscv-dev mailing list
> libre-riscv-dev at lists.libre-riscv.org
> http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev
>