A SystemVerilog File with many covers statements

[SeddonShen]

I have a .sv files with mant covers in it, but i only want to verify the specified one，such as cover(x2), how can i use sby to do it? Thx!

    if (valid) begin
      cover(x1);
      cover(x2);
      cover(x3);
      cover(x4);
    end

[georgerennie]

You can do this by naming the cover statements, then removing all covers but the ones you want with chformal -remove -cover c:<cover_to_keep> %n. This command removes covers matching the selection, and the selection first selects a cell with name <cover_to_keep>, then inverts the selection (%n), so its all other covers that get removed.

For a small example, if we have in covers.v:

module top(input wire clk);
reg [7:0] count;
initial count = '0;
always @(posedge clk) count <= count + 1'b1;

always @* begin
    cov_count_1: cover(count == 1);
    cov_count_5: cover(count == 5);
    cov_count_9: cover(count == 9);
end

endmodule

The sby file could be like so to only check cov_count_9:

[options]
mode cover

[engines]
smtbmc

[script]
read -formal covers.v
prep -top top
chformal -remove -cover c:cov_count_9 %n

[files]
covers.v