mirror of https://github.com/YosysHQ/yosys.git
56 lines
1.6 KiB
Plaintext
56 lines
1.6 KiB
Plaintext
|
|
||
|
|
|
||
|
|
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'
|
||
|
|
|
||
|
|
|
||
|
|
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)
|
||
|
|
|