[libre-riscv-dev] formal verification
Luke Kenneth Casson Leighton
lkcl at lkcl.net
Wed Feb 27 13:49:52 GMT 2019
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.
More information about the libre-riscv-dev
mailing list