blob: b4c436a3ae1d4b33983c6cdaa5066b20031a6b38 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
|
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)
|
