Improve docs for verific bindings, add simply sby example

1 files changed, 55 insertions, 0 deletions

diff --git a/frontends/verific/README b/frontends/verific/README
new file mode 100644
index 000000000..e747255db
--- /dev/null
+++ b/frontends/verific/README
@@ -0,0 +1,55 @@
+
+
+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)
+