From 2c13fbefe67adb3a4adb8a6f283b198abb8a43a0 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 7 Mar 2018 23:10:53 +0100 Subject: [PATCH] Extend primegen example Signed-off-by: Clifford Wolf --- docs/examples/demos/.gitignore | 3 +++ docs/examples/puzzles/.gitignore | 4 +++- docs/examples/puzzles/primegen.sby | 12 ++++++++++-- docs/examples/puzzles/primegen.v | 16 ++++++++++++++++ 4 files changed, 32 insertions(+), 3 deletions(-) create mode 100644 docs/examples/demos/.gitignore 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 -- 2.30.2