mirror of
https://github.com/YosysHQ/yosys.git
synced 2026-10-06 10:03:36 +02:00
Jannis Harder
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.
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 [email protected] 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)