sbysrc/demo2.sby

   1 [options]
   2 mode prove
   3 wait on
   4
   5 [engines]
   6 aiger suprove
   7 aiger avy
   8
   9 [script]
  10 read_verilog -formal demo.v
  11 prep -top top
  12
  13 [file demo.v]
  14 module top(input clk, input up, down);
  15   reg [4:0] counter = 0;
  16   always @(posedge clk) begin
  17     if (up && counter != 10) counter <= counter + 1;
  18     if (down && counter != 0) counter <= counter - 1;
  19   end
  20   assert property (counter != 15);
  21 endmodule