yosys/frontends/verific
Miodrag Milanovic af94123730 verific: expose library name as module attribute 2024-04-15 17:01:07 +02:00
..
Makefile.inc Verific support for VHDL 2019 2024-03-28 13:21:55 +01:00
README Update README 2022-07-28 12:32:19 +02:00
example.sby Improve docs for verific bindings, add simply sby example 2017-07-22 11:58:51 +02:00
example.sv Improve docs for verific bindings, add simply sby example 2017-07-22 11:58:51 +02:00
verific.cc verific: expose library name as module attribute 2024-04-15 17:01:07 +02:00
verific.h verific: Fixes incorrect aldff inference in verific importer 2024-02-05 07:10:25 +00:00
verificsva.cc verific: Handle non-seq properties with VerificClocking conditions 2023-04-21 17:19:42 +02:00

README

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)