Added examples/aiger/

diff --git a/examples/aiger/.gitignore b/examples/aiger/.gitignore
new file mode 100644 (file)
index 0000000..3524e93
--- /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 (file)
index 0000000..4e7694e
--- /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 (file)
index 0000000..caaa447
--- /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 (file)
index 0000000..bb54ba4
--- /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