tests/aim_vs_smt2_nonzero_start_offset.sby

   1 [tasks]
   2 bmc
   3 prove
   4
   5 [options]
   6 bmc: mode bmc
   7 prove: mode prove
   8 expect fail
   9 wait on
  10
  11 [engines]
  12 bmc: abc bmc3
  13 bmc: abc sim3
  14 prove: aiger avy
  15 prove: aiger suprove
  16 prove: abc pdr
  17
  18 [script]
  19 read -sv test.sv
  20 prep -top test
  21
  22 [file test.sv]
  23 module test (
  24     input clk,
  25     input [8:1] nonzero_offset
  26 );
  27     reg [7:0] counter = 0;
  28
  29     always @(posedge clk) begin
  30         if (counter == 3) assert(nonzero_offset[1]);
  31         counter <= counter + 1;
  32     end
  33 endmodule