diff options
Diffstat (limited to 'examples/smtbmc/demo9.v')
| -rw-r--r-- | examples/smtbmc/demo9.v | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/examples/smtbmc/demo9.v b/examples/smtbmc/demo9.v new file mode 100644 index 000000000..f0b91e2ca --- /dev/null +++ b/examples/smtbmc/demo9.v @@ -0,0 +1,13 @@ +module demo9; + (* maximize *) wire[7:0] h = $anyconst; + wire [7:0] i = $allconst; + + wire [7:0] t0 = ((i << 8'b00000010) + 8'b00000011); + wire trigger = (t0 > h) && (h < 8'b00000100); + + always @* begin + assume(trigger == 1'b1); + cover(1); + end +endmodule + |