yosys

History

Clifford Wolf e275692e84 Verific: Produce errors for instantiating unknown module Because if the unknown module is connected to any constants, Verific will actually break all constants in the same module, even if they have nothing to do structurally with that instance of an unknown module. Signed-off-by: Clifford Wolf <clifford@clifford.at>		2018-07-22 18:44:05 +02: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	Verific: Produce errors for instantiating unknown module	2018-07-22 18:44:05 +02:00
verific.h	Add automatic verific import in hierarchy command	2018-06-20 23:45:01 +02:00
verificsva.cc	Fix handling of eventually properties in verific importer	2018-07-17 12:43:30 +02: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)