2017-07-22 04:58:51 -05:00
|
|
|
|
|
|
|
|
This directory contains Verific bindings for Yosys.
|
2019-12-18 06:06:34 -06:00
|
|
|
|
2021-03-04 09:43:30 -06:00
|
|
|
Use Tabby CAD Suite from YosysHQ if you need Yosys+Verifc.
|
|
|
|
|
https://www.yosyshq.com/
|
2019-12-18 06:06:34 -06:00
|
|
|
|
2021-03-04 09:43:30 -06:00
|
|
|
Contact YosysHQ at contact@yosyshq.com for free evaluation
|
|
|
|
|
binaries of Tabby CAD Suite.
|
2017-07-22 04:58:51 -05:00
|
|
|
|
|
|
|
|
|
2017-10-13 10:11:46 -05:00
|
|
|
Verific Features that should be enabled in your Verific library
|
|
|
|
|
===============================================================
|
|
|
|
|
|
|
|
|
|
database/DBCompileFlags.h:
|
|
|
|
|
DB_PRESERVE_INITIAL_VALUE
|
|
|
|
|
|
|
|
|
|
|
2017-07-22 04:58:51 -05:00
|
|
|
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
|
|
|
|
|
|
2019-03-08 18:43:50 -06:00
|
|
|
This will generate approximately one page of text output. The last lines
|
2017-07-22 04:58:51 -05:00
|
|
|
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)
|
|
|
|
|
|
