[libre-riscv-dev] formal verification

[Jacob Lifshay]

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.

Jacob Lifshay