yosys

History

Clifford Wolf db323685a4 Add Verific support for SVA nexttime properties Signed-off-by: Clifford Wolf <clifford@clifford.at>		2019-11-22 16:11:56 +01:00
..
Makefile.inc	Move Verific SVA importer to extra C++ source file	2018-02-18 13:52:49 +01:00
README	Fix spelling	2019-03-09 00:43:50 +00: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	Improve handling of verific primitives in "verific -import -V" mode	2019-11-22 16:00:07 +01:00
verific.h	Do not rename VHDL entities to "entity(impl)" when they are top modules	2019-11-20 12:54:10 +01:00
verificsva.cc	Add Verific support for SVA nexttime properties	2019-11-22 16:11:56 +01:00

README


This directory contains Verific bindings for Yosys.
See http://www.verific.com/ for details.


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)