[libre-riscv-dev] formal verification
Luke Kenneth Casson Leighton
lkcl at lkcl.net
Sun Mar 3 18:52:52 GMT 2019
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
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
> 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.
More information about the libre-riscv-dev