mirror of
https://github.com/YosysHQ/yosys
synced 2026-05-26 03:46:22 +00:00
a0cbe1a334
May not be the best approach, insofar as it uses empty memory elements for padding out the alignment, but it does avoid costly address arithmetic. Still needs to adjust ascii init val addresses, but should work fine for read/write accesses. |
||
|---|---|---|
| .. | ||
| 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)