3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-07-25 05:37:02 +00:00
yosys/frontends/verific
2020-06-30 12:13:13 +02:00
..
example.sby
example.sv
Makefile.inc
README
verific.cc Update verific API version check 2020-06-30 12:13:13 +02:00
verific.h verific: recover wiretype/enum attr as part of import_attributes() 2020-04-27 08:43:54 -07:00
verificsva.cc

This directory contains Verific bindings for Yosys.

Use Symbiotic EDA Suite if you need Yosys+Verifc.
https://www.symbioticeda.com/seda-suite

Contact office@symbioticeda.com for free evaluation
binaries of Symbiotic EDA 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)