yosys

History

Clifford Wolf cda37830b0 Add hack for handling SVA labels via Verific Signed-off-by: Clifford Wolf <clifford@clifford.at>		2019-03-07 10:52:44 -08:00
..
Makefile.inc	Move Verific SVA importer to extra C++ source file	2018-02-18 13:52:49 +01:00
README	Remove -m32 Verific eval lib build instructions	2019-01-04 15:03:49 +01: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 "read" error msg	2019-02-28 20:34:42 -08:00
verific.h	Improve src tagging (using names and attrs) of cells and wires in verific front-end	2018-12-18 16:01:22 +01:00
verificsva.cc	Add hack for handling SVA labels via Verific	2019-03-07 10:52:44 -08: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 outpout. 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)