tests/junit_assert.sby

   1 [tasks]
   2 pass
   3 fail
   4 preunsat
   5
   6 [options]
   7 mode bmc
   8 depth 1
   9
  10 pass: expect pass
  11 fail: expect fail
  12 preunsat: expect error
  13
  14 [engines]
  15 smtbmc boolector
  16
  17 [script]
  18 fail: read -define FAIL
  19 preunsat: read -define PREUNSAT
  20 read -sv test.sv
  21 prep -top top
  22
  23 [file test.sv]
  24 module test(input foo);
  25 always @* assert(foo);
  26 `ifdef FAIL
  27 always @* assert(!foo);
  28 `endif
  29 `ifdef PREUNSAT
  30 always @* assume(!foo);
  31 `endif
  32 endmodule
  33
  34 module top();
  35 test test_i (
  36 .foo(1'b1)
  37 );
  38 endmodule