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 (file)
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 02f304249b84536843ada4d2256b6299a5a8ac87..0d917a79a3ff7fec5d6a7171de84f863bd5f9a7d 100644 (file)
--- 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 65df8d3c9f4f7c8333ffb3a709449d7dcda00208..53b005edf9b52d603c9baa5bfed0c2f6ebd39cc9 100644 (file)
--- 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 2c7681acce153c970958a1d40e2cea437be60373..95d6ddcc693f44509f6ba31bc332f494e2e198a4 100644 (file)
--- 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