tests/cover_fail.sby

   1 [options]
   2 mode cover
   3 depth 5
   4 expect pass,fail
   5
   6 [engines]
   7 smtbmc boolector
   8
   9 [script]
  10 read -sv test.v
  11 prep -top test
  12
  13 [file test.v]
  14 module test(
  15 input clk,
  16 input rst,
  17 output reg [3:0] count
  18 );
  19
  20 initial assume (rst == 1'b1);
  21
  22 always @(posedge clk) begin
  23 if (rst)
  24   count <= 4'b0;
  25 else
  26   count <= count + 1'b1;
  27
  28 cover (count == 0 && !rst);
  29 cover (count == 4'd11 && !rst);
  30 end
  31 endmodule