[libre-riscv-dev] formal verification
programmerjake at gmail.com
Sun Mar 3 21:16:53 GMT 2019
On Sun, Mar 3, 2019, 10:53 Luke Kenneth Casson Leighton <lkcl at lkcl.net>
> On Sat, Mar 2, 2019 at 4:10 PM Hendrik Boom <hendrik at topoi.pooq.com>
> > 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
> > > 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
> > comfortable with it.
> libre-riscv-dev mailing list
> libre-riscv-dev at lists.libre-riscv.org
More information about the libre-riscv-dev