From 0f21d0146010287d2221c50ae49c9be56793aa8a Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 3 Mar 2018 19:58:35 +0100 Subject: [PATCH] Add primegen example Signed-off-by: Clifford Wolf --- docs/examples/puzzles/.gitignore | 1 + docs/examples/puzzles/primegen.sby | 13 +++++++++++++ docs/examples/puzzles/primegen.v | 11 +++++++++++ 3 files changed, 25 insertions(+) create mode 100644 docs/examples/puzzles/primegen.sby create mode 100644 docs/examples/puzzles/primegen.v 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 -- 2.30.2