This directory contains Verific bindings for Yosys.
Use Tabby CAD Suite from YosysHQ if you need Yosys+Verific.
https://www.yosyshq.com/
Contact YosysHQ at contact@yosyshq.com for free evaluation
binaries of Tabby CAD Suite.
Verific Features that should be enabled in your Verific library
===============================================================
database/DBCompileFlags.h:
DB_PRESERVE_INITIAL_VALUE
Testing Verific+Yosys+SymbiYosys for formal verification
========================================================
Install Yosys+Verific, SymbiYosys, and Yices2. Install instructions:
http://symbiyosys.readthedocs.io/en/latest/quickstart.html#installing
Then run in the following command in this directory:
sby -f example.sby
This will generate approximately one page of text output. The last lines
should be something like this:
SBY [example] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY [example] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY [example] summary: engine_0 (smtbmc yices) returned PASS for basecase
SBY [example] summary: engine_0 (smtbmc yices) returned PASS for induction
SBY [example] summary: successful proof by k-induction.
SBY [example] DONE (PASS, rc=0)
4bb4b6c662