From 105b6374ae8d8f3892f907ca61bb62d35b8d7d4d Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Thu, 1 Dec 2016 13:42:17 +0100
Subject: [PATCH] Added examples/aiger/

---
 examples/aiger/.gitignore |  5 +++++
 examples/aiger/README     | 22 ++++++++++++++++++++++
 examples/aiger/demo.sh    | 14 ++++++++++++++
 examples/aiger/demo.v     | 12 ++++++++++++
 4 files changed, 53 insertions(+)
 create mode 100644 examples/aiger/.gitignore
 create mode 100644 examples/aiger/README
 create mode 100644 examples/aiger/demo.sh
 create mode 100644 examples/aiger/demo.v

diff --git a/examples/aiger/.gitignore b/examples/aiger/.gitignore
new file mode 100644
index 000000000..3524e9362
--- /dev/null
+++ b/examples/aiger/.gitignore
@@ -0,0 +1,5 @@
+demo.aig
+demo.aim
+demo.aiw
+demo.smt2
+demo.vcd
diff --git a/examples/aiger/README b/examples/aiger/README
new file mode 100644
index 000000000..4e7694e95
--- /dev/null
+++ b/examples/aiger/README
@@ -0,0 +1,22 @@
+AIGER is a format for And-Inverter Graphs (AIGs).
+See http://fmv.jku.at/aiger/ for details.
+
+AIGER is used in the Hardware Model Checking Competition (HWMCC),
+therefore all solvers competing in the competition have to support
+the format.
+
+The example in this directory is using super_prove as solver. Check
+http://downloads.bvsrc.org/super_prove/ for the lates release. (See
+https://bitbucket.org/sterin/super_prove_build for sources.)
+
+The "demo.sh" script in this directory expects a "super_prove" executable
+in the PATH. E.g. extract the release to /usr/local/libexec/super_prove
+and then create a /usr/local/bin/super_prove file with the following
+contents (and "chmod +x" that file):
+
+	#!/bin/bash
+	exec /usr/local/libexec/super_prove/bin/super_prove.sh "$@"
+
+The "demo.sh" script also expects the "z3" SMT2 solver in the PATH for
+converting the witness file generated by super_prove to VCD using
+yosys-smtbmc. See https://github.com/Z3Prover/z3 for install notes.
diff --git a/examples/aiger/demo.sh b/examples/aiger/demo.sh
new file mode 100644
index 000000000..caaa44761
--- /dev/null
+++ b/examples/aiger/demo.sh
@@ -0,0 +1,14 @@
+#!/bin/bash
+set -ex
+yosys -p '
+	read_verilog -formal demo.v
+	prep -flatten -nordff -top demo
+	write_smt2 -wires demo.smt2
+	miter -assert demo
+	memory_map; opt -full
+	techmap; opt -fast
+	abc -fast -g AND; opt_clean
+	write_aiger -miter -zinit -map demo.aim demo.aig
+'
+super_prove demo.aig > demo.aiw
+yosys-smtbmc --dump-vcd demo.vcd --aig demo demo.smt2
diff --git a/examples/aiger/demo.v b/examples/aiger/demo.v
new file mode 100644
index 000000000..bb54ba4ef
--- /dev/null
+++ b/examples/aiger/demo.v
@@ -0,0 +1,12 @@
+module demo(input clk, reset, ctrl);
+  localparam NBITS = 10;
+  reg [NBITS-1:0] counter;
+  initial counter[NBITS-2] = 0;
+  initial counter[0] = 1;
+  always @(posedge clk) begin
+    counter <= reset ? 0 : ctrl ? counter + 1 : counter - 1;
+    assume(counter != 0);
+    assume(counter != 1 << (NBITS-1));
+    assert(counter != (1 << NBITS)-1);
+  end
+endmodule
-- 
2.30.2