mirror of
https://github.com/YosysHQ/yosys
synced 2026-02-17 06:11:47 +00:00
390d1c583a
This uses the same constant parsing for enum_values and for attributes and extends it to handle signed values as those are used for enums that implicitly use the int type. |
||
|---|---|---|
| .. | ||
| example.sby | ||
| example.sv | ||
| Makefile.inc | ||
| README | ||
| verific.cc | ||
| verific.h | ||
| verificsva.cc | ||
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)