yosys

History

N. Engelhardt 21686f0d9d verific: import src attribute on $memrd/$memwr cells		2023-06-23 19:41:36 +02:00
..
Makefile.inc	Option to disable verific VHDL support	2021-10-20 10:02:58 +02: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: import src attribute on $memrd/$memwr cells	2023-06-23 19:41:36 +02:00
verific.h	For case select values use Sa instead of Sx and Sz	2023-02-08 09:22:48 +01: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)