docs/examples/demos/up_down_counter.sby

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