[libre-riscv-dev] formal verification
programmerjake at gmail.com
Wed Apr 17 05:42:26 BST 2019
>From what I saw, verific is an optional requirement. According to ,
only Yosys, SymbiYosys, and Z3 are required.
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.
> *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
More information about the libre-riscv-dev