[libre-riscv-dev] formal verification

[Luke Kenneth Casson Leighton]

On Mon, Mar 4, 2019 at 2:58 AM Jacob Lifshay <programmerjake at gmail.com> wrote:

> On Sun, Mar 3, 2019 at 4:17 PM Hendrik Boom <hendrik at topoi.pooq.com> wrote:
>
> > What are you using now that needs to be converted to verilog?
> >
> We're using nmigen.
>
> > Des it make sense to verify *that* instead?  Or are there just no tools
> > available for that?
> >
> It could be done either way, I was thinking that if we can prove that the
> code that ends up in a verilog module won't magically change because of an
> unrelated change in a different part of the processor (eg, alu changes
> because we added another serial port), we could verify those verilog
> modules directly since tooling already exists for formal verification of
> verilog, and that way we wouldn't have to formally verify all of nmigen as
> well.

 ... what jacob said :)

l.