Added examples/aiger/

examples/aiger/.gitignore

@@ -0,0 +1,5 @@
+demo.aig
+demo.aim
+demo.aiw
+demo.smt2
+demo.vcd

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.

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

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