From: Clifford Wolf <clifford@clifford.at>
Date: Wed, 7 Mar 2018 22:10:53 +0000 (+0100)
Subject: Extend primegen example
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2c13fbefe67adb3a4adb8a6f283b198abb8a43a0;p=SymbiYosys.git

Extend primegen example

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

diff --git a/docs/examples/demos/.gitignore b/docs/examples/demos/.gitignore
new file mode 100644
index 0000000..9efd362
--- /dev/null
+++ b/docs/examples/demos/.gitignore
@@ -0,0 +1,3 @@
+/fib_cover
+/fib_prove
+/fib_live
diff --git a/docs/examples/puzzles/.gitignore b/docs/examples/puzzles/.gitignore
index 02f3042..0d917a7 100644
--- a/docs/examples/puzzles/.gitignore
+++ b/docs/examples/puzzles/.gitignore
@@ -1,2 +1,4 @@
 /wolf_goat_cabbage
-/primegen
+/primegen_primegen
+/primegen_primes_pass
+/primegen_primes_fail
diff --git a/docs/examples/puzzles/primegen.sby b/docs/examples/puzzles/primegen.sby
index 65df8d3..53b005e 100644
--- a/docs/examples/puzzles/primegen.sby
+++ b/docs/examples/puzzles/primegen.sby
@@ -1,13 +1,21 @@
+[tasks]
+primegen
+primes_fail
+primes_pass
+
 [options]
 mode cover
 depth 1
+primes_fail: expect fail
 
 [engines]
-smtbmc --dumpsmt2 --stbv z3
+smtbmc --dumpsmt2 --progress --stbv z3
 
 [script]
 read_verilog -formal primegen.v
-prep -top primegen
+primes_fail: chparam -set offset 7 primes
+primegen: prep -top primegen
+~primegen: prep -top primes
 
 [files]
 primegen.v
diff --git a/docs/examples/puzzles/primegen.v b/docs/examples/puzzles/primegen.v
index 2c7681a..95d6ddc 100644
--- a/docs/examples/puzzles/primegen.v
+++ b/docs/examples/puzzles/primegen.v
@@ -9,3 +9,19 @@ module primegen;
 		cover(1);
 	end
 endmodule
+
+module primes;
+	parameter [8:0] offset = 500;
+	wire [8:0] prime1 = $anyconst;
+	wire [9:0] prime2 = prime1 + offset;
+	wire [4:0] factor = $allconst;
+
+	always @* begin
+		if (1 < factor && factor < prime1)
+			assume((prime1 % factor) != 0);
+		if (1 < factor && factor < prime2)
+			assume((prime2 % factor) != 0);
+		assume(1 < prime1);
+		cover(1);
+	end
+endmodule