Improve docs for verific bindings, add simply sby example

5 files changed, 89 insertions, 48 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)
+
diff --git a/frontends/verific/build_amd64.txt b/frontends/verific/build_amd64.txt
deleted file mode 100644
index 95d618ecc..000000000
--- a/frontends/verific/build_amd64.txt
+++ /dev/null
@@ -1,30 +0,0 @@
-
-Notes on building yosys with verific support on amd64 when you
-only have the i386 eval version of Verific:
-
-
-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 frontends/verific/test_navre.ys
-
diff --git a/frontends/verific/example.sby b/frontends/verific/example.sby
new file mode 100644
index 000000000..ffbf33cab
--- /dev/null
+++ b/frontends/verific/example.sby
@@ -0,0 +1,16 @@
+# Simple SymbiYosys example job utilizing Verific
+
+[options]
+mode prove
+depth 10
+
+[engines]
+smtbmc yices
+
+[script]
+verific -sv example.sv
+verific -import top
+prep -top top
+
+[files]
+example.sv
diff --git a/frontends/verific/example.sv b/frontends/verific/example.sv
new file mode 100644
index 000000000..21a5d42c8
--- /dev/null
+++ b/frontends/verific/example.sv
@@ -0,0 +1,18 @@
+module top (
+  input clk, rst,
+  output reg [3:0] cnt
+);
+  initial cnt = 0;
+
+  always @(posedge clk) begin
+    if (rst)
+      cnt <= 0;
+    else
+      cnt <= cnt + 4'd 1;
+  end
+
+  always @(posedge clk) begin
+    assume (cnt != 10);
+    assert (cnt != 15);
+  end
+endmodule
diff --git a/frontends/verific/test_navre.ys b/frontends/verific/test_navre.ys
deleted file mode 100644
index a56b725ac..000000000
--- a/frontends/verific/test_navre.ys
+++ /dev/null
@@ -1,18 +0,0 @@
-verific -vlog2k ../yosys-bigsim/softusb_navre/rtl/softusb_navre.v
-verific -import softusb_navre
-
-memory softusb_navre
-flatten softusb_navre
-rename softusb_navre gate
-
-read_verilog ../yosys-bigsim/softusb_navre/rtl/softusb_navre.v
-cd softusb_navre; proc; opt; memory; opt; cd ..
-rename softusb_navre gold
-
-expose -dff -shared gold gate
-miter -equiv -ignore_gold_x -make_assert -make_outputs -make_outcmp gold gate miter
-
-cd miter
-flatten; opt -undriven
-sat -verify -maxsteps 5 -set-init-undef -set-def-inputs -prove-asserts -tempinduct-def \
-    -seq 1 -set-at 1 in_rst 1 # -show-inputs -show-outputs