From 5033b51947a6ef02cb785b5622e993335efa750a Mon Sep 17 00:00:00 2001 From: Ruben Undheim Date: Thu, 30 Aug 2018 20:46:20 +0200 Subject: New upstream version 0.7+20180830git0b7a184 --- frontends/verific/README | 62 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 62 insertions(+) create mode 100644 frontends/verific/README (limited to 'frontends/verific/README') diff --git a/frontends/verific/README b/frontends/verific/README new file mode 100644 index 00000000..b4c436a3 --- /dev/null +++ b/frontends/verific/README @@ -0,0 +1,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) + -- cgit v1.2.3