[libre-riscv-dev] formal verification

[Luke Kenneth Casson Leighton]

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 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.

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

 :)