tests/junit_timeout_error.sby

   1 [tasks]
   2 syntax error
   3 solver error
   4 timeout
   5
   6 [options]
   7 mode cover
   8 depth 1
   9 timeout: timeout 1
  10 error: expect error
  11 timeout: expect timeout
  12
  13 [engines]
  14 ~solver: smtbmc --dumpsmt2 --progress --stbv z3
  15 solver: smtbmc foo
  16
  17 [script]
  18 read -noverific
  19 syntax: read -define SYNTAX_ERROR
  20 read -sv primes.sv
  21 prep -top primes
  22
  23 [file primes.sv]
  24 module primes;
  25         parameter [8:0] offset = 7;
  26         (* anyconst *) reg [8:0] prime1;
  27         wire [9:0] prime2 = prime1 + offset;
  28         (* allconst *) reg [4:0] factor;
  29
  30 `ifdef SYNTAX_ERROR
  31         foo
  32 `endif
  33
  34         always @* begin
  35                 if (1 < factor && factor < prime1)
  36                         assume ((prime1 % factor) != 0);
  37                 if (1 < factor && factor < prime2)
  38                         assume ((prime2 % factor) != 0);
  39                 assume (1 < prime1);
  40                 cover (1);
  41         end
  42 endmodule