[libre-riscv-dev] formal verification

[Luke Kenneth Casson Leighton]

On Wed, Apr 17, 2019 at 5:42 AM Jacob Lifshay <programmerjake at gmail.com> wrote:

> From what I saw, verific is an optional requirement. According to [1],
> only Yosys, SymbiYosys, and Z3 are required.
>
> [1]: https://github.com/YosysHQ/SymbiYosys/blob/master/docs/source/quickstart.rst#installing

 ok good find, i've cross-referenced to the (new as of yesterday)
formal mathematical proof bug (#61), should see some messages come
through... can we keep this discussion going through the bugtracker,
on this one?

l.