[libre-riscv-dev] formal verification

[Jacob Lifshay]

>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

On Sun, Mar 31, 2019 at 8:17 PM Luke Kenneth Casson Leighton
<lkcl at lkcl.net> wrote:
>
> found a tutorial which makes mention of the different options, such as
> bounded model check and prove mode, which does k-induction checks.
>
> https://symbiyosys.readthedocs.io/en/latest/quickstart.html
>
> https://tomverbeure.github.io/rtl/2019/01/04/Under-the-Hood-of-Formal-Verification.html
>
> *click*.... ah.  for full features, it's necessary to link to
> something called "verific".
>
> ah.  okay.
>
> _______________________________________________
> libre-riscv-dev mailing list
> libre-riscv-dev at lists.libre-riscv.org
> http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev