aboutsummaryrefslogtreecommitdiffstats
path: root/examples
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2016-12-01 13:42:17 +0100
committerClifford Wolf <clifford@clifford.at>2016-12-01 13:42:17 +0100
commit105b6374ae8d8f3892f907ca61bb62d35b8d7d4d (patch)
tree6455eede1117cd95344ac0698b27f7e9580b4588 /examples
parent88b9733253c587eba45d488355e73f1879091fff (diff)
downloadyosys-105b6374ae8d8f3892f907ca61bb62d35b8d7d4d.tar.gz
yosys-105b6374ae8d8f3892f907ca61bb62d35b8d7d4d.tar.bz2
yosys-105b6374ae8d8f3892f907ca61bb62d35b8d7d4d.zip
Added examples/aiger/
Diffstat (limited to 'examples')
-rw-r--r--examples/aiger/.gitignore5
-rw-r--r--examples/aiger/README22
-rw-r--r--examples/aiger/demo.sh14
-rw-r--r--examples/aiger/demo.v12
4 files changed, 53 insertions, 0 deletions
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