Add primegen example

Signed-off-by: Clifford Wolf <clifford@clifford.at>

diff --git a/docs/examples/puzzles/.gitignore b/docs/examples/puzzles/.gitignore
index ba84fb6232ca5e5e3a63f42010687cb25230274e..02f304249b84536843ada4d2256b6299a5a8ac87 100644 (file)
--- a/docs/examples/puzzles/.gitignore
+++ b/docs/examples/puzzles/.gitignore
@@ -1 +1,2 @@
 /wolf_goat_cabbage
+/primegen

diff --git a/docs/examples/puzzles/primegen.sby b/docs/examples/puzzles/primegen.sby
new file mode 100644 (file)
index 0000000..65df8d3
--- /dev/null
+++ b/docs/examples/puzzles/primegen.sby
@@ -0,0 +1,13 @@
+[options]
+mode cover
+depth 1
+
+[engines]
+smtbmc --dumpsmt2 --stbv z3
+
+[script]
+read_verilog -formal primegen.v
+prep -top primegen
+
+[files]
+primegen.v

diff --git a/docs/examples/puzzles/primegen.v b/docs/examples/puzzles/primegen.v
new file mode 100644 (file)
index 0000000..2c7681a
--- /dev/null
+++ b/docs/examples/puzzles/primegen.v
@@ -0,0 +1,11 @@
+module primegen;
+       wire [31:0] prime = $anyconst;
+       wire [15:0] factor = $allconst;
+
+       always @* begin
+               if (1 < factor && factor < prime)
+                       assume((prime % factor) != 0);
+               assume(prime > 1000000000);
+               cover(1);
+       end
+endmodule