[libre-riscv-dev] formal verification

Jacob Lifshay programmerjake at gmail.com
Mon Mar 4 02:58:08 GMT 2019


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


More information about the libre-riscv-dev mailing list