tests/unsorted/allconst.sby

   1 [tasks]
   2 yices
   3 z3
   4
   5 [options]
   6 mode cover
   7 depth 1
   8
   9 [engines]
  10 yices: smtbmc --stbv yices
  11 z3: smtbmc --stdt z3
  12
  13 [script]
  14 read -noverific
  15 read -formal primegen.sv
  16 prep -top primegen
  17
  18 [file primegen.sv]
  19
  20 module primegen;
  21         (* anyconst *) reg [9:0] prime;
  22         (* allconst *) reg [4:0] factor;
  23
  24         always @* begin
  25                 if (1 < factor && factor < prime)
  26                         assume ((prime % factor) != 0);
  27                 assume (prime > 800);
  28                 cover (1);
  29         end
  30 endmodule