diff options
Diffstat (limited to 'examples/smtbmc/demo8.v')
| -rw-r--r-- | examples/smtbmc/demo8.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/examples/smtbmc/demo8.v b/examples/smtbmc/demo8.v new file mode 100644 index 00000000..c4c396cd --- /dev/null +++ b/examples/smtbmc/demo8.v @@ -0,0 +1,12 @@ +// Simple exists-forall demo + +module demo8; + wire [7:0] prime = $anyconst; + wire [3:0] factor = $allconst; + + always @* begin + if (1 < factor && factor < prime) + assume((prime % factor) != 0); + assume(prime > 1); + end +endmodule |