yosys/frontends/verific
Clifford Wolf 50b09de033 Fix VerificImporter asymmetric memories error message
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-01-02 15:05:23 +01:00
..
Makefile.inc Move Verific SVA importer to extra C++ source file 2018-02-18 13:52:49 +01:00
README Update Verific README 2017-10-13 17:11:53 +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 Fix VerificImporter asymmetric memories error message 2019-01-02 15:05:23 +01: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 Fix typographical and grammatical errors and inconsistencies. 2019-01-02 13:12:17 +00:00

README


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


Building Yosys with the 32 bit Verific eval library on amd64:
=============================================================

1.) Use a Makefile.conf like the following one:

--snip--
CONFIG := gcc
ENABLE_TCL := 0
ENABLE_PLUGINS := 0
ENABLE_VERIFIC := 1
CXXFLAGS += -m32
LDFLAGS += -m32
VERIFIC_DIR = /usr/local/src/verific_lib_eval
--snap--


2.) Install the necessary multilib packages

Hint: On debian/ubuntu the multilib packages have names such as
libreadline-dev:i386 or lib32readline6-dev, depending on the
exact version of debian/ubuntu you are working with.


3.) Build and test

make -j8
./yosys -p 'verific -sv frontends/verific/example.sv; verific -import top'


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)