[libre-riscv-dev] formal verification

[Hendrik Boom]

On Sun, Mar 03, 2019 at 01:16:53PM -0800, Jacob Lifshay wrote:
> 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 was starting to think in this direction too.  Still lots to read.

What are you using now that needs to be converted to verilog?
Des it make sense to verify *that* instead?  Or are there just no tools 
available for that?

-- hendrik