mirror of
https://github.com/YosysHQ/sby.git
synced 2025-04-12 16:28:17 +00:00
Add primegen example
Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
parent
35a5fb94f1
commit
0f21d01460
1
docs/examples/puzzles/.gitignore
vendored
1
docs/examples/puzzles/.gitignore
vendored
|
@ -1 +1,2 @@
|
||||||
/wolf_goat_cabbage
|
/wolf_goat_cabbage
|
||||||
|
/primegen
|
||||||
|
|
13
docs/examples/puzzles/primegen.sby
Normal file
13
docs/examples/puzzles/primegen.sby
Normal file
|
@ -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
|
11
docs/examples/puzzles/primegen.v
Normal file
11
docs/examples/puzzles/primegen.v
Normal file
|
@ -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
|
Loading…
Reference in a new issue