[libre-riscv-dev] formal verification

[Luke Kenneth Casson Leighton]

On Wed, Feb 27, 2019 at 11:48 AM Hendrik Boom <hendrik at topoi.pooq.com> wrote:

> I've been wondering whether to voluntee here, because
>
> * I don't have any hardware experience

 it's python.  this was very deliberate so that software people stand
a chance of understanding.  the main thing to remember is, m.d.comb
means "it gets calculated straight away" and m.d.sync means "it gets
assigned on the next clock cycle".

> * I haven't done any work in formal verification recently (but I was
>   developing a type-theory verifier three decades ago)
> * I probably haven't the time to do it,

 :)

>   * let alone time to get up-to-date on proofs about hardware
> * And even if I succeed, waiting for me would delay the project
>   significantly

 unit tests can always be added which mitigate a definitive need for
formal proofs.... i'd still like them to be added / available, however
there's no critical dependence.

> * And I do't know if the tools I can use are compatible with the tools
>   you use
>
> but ...
>
> would it be helpful if I were to look into formal verification of any
> of this RISC-V architecture under development?

 sure!

> And what do I need to get familiar with any of it?  (links to documents
> and software, please)

 ok so.. it *might* be as simple as writing a 20-line verilog script,
using riscv-formal as the test suite.

 https://github.com/SymbioticEDA/riscv-formal
 https://www.semiwiki.com/forum/content/7850-verifying-risc-v-1-page-code-e.html

 i really am not sure of the difference between "formal verification"
and "running the riscv-isa-tests" to confirm compliance.  perhaps they
are considered to be the same, i really don't know.

 if you can take a look that alone would be really helpful.

l.