| This directory contains Verific bindings for Yosys. | |
| See http://www.verific.com/ for details. | |
| 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) | |