[libre-riscv-dev] formal verification

[Hendrik Boom]

On Wed, Feb 27, 2019 at 01:49:52PM +0000, Luke Kenneth Casson Leighton wrote:
> 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.


Formal verification means to produce a machine-checked mathematical 
proof of correctness.

It's not trivial to do.

But I'll start looking at what you've linked me to in order to 
familiarise myself with it.

-- hendrik

> 
>  if you can take a look that alone would be really helpful.
> 
> l.
> 
> _______________________________________________
> libre-riscv-dev mailing list
> libre-riscv-dev at lists.libre-riscv.org
> http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev