From: Clifford Wolf <clifford@clifford.at>
Date: Sat, 3 Mar 2018 18:58:35 +0000 (+0100)
Subject: Add primegen example
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0f21d0146010287d2221c50ae49c9be56793aa8a;p=SymbiYosys.git

Add primegen example

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

diff --git a/docs/examples/puzzles/.gitignore b/docs/examples/puzzles/.gitignore
index ba84fb6..02f3042 100644
--- 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
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
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