Mutation Coverage with MCY

Change the Design, Watch the Properties

A mutation is the design with one small change: a bit forced, an operator's output inverted, a mux input flipped. Run the whole property set against it. If some property fails, the mutation is killed. If all pass, it survives.

Most kills here come from a_level (11) and a_bound (5). Count and flags see every mutation of the bookkeeping logic.

Harmless or a Hole

A survivor is one of two things. Either the change makes no difference to the outputs, or the properties cannot see a real change. A second test on each survivor, an equivalence check against the original, sorts them.

Here 1 survivor was equivalent: #29 forces bit 0 of the constant 16 in full = count == 16 to 0, which it already is. A matched-flop LEC run proved it in seconds. The other 14 are holes.

Of the holes, 5 corrupt the write data (#5, #7, #11, #23, #39). Most of the rest stop writes or reads from happening. In #17 the write request is tied to 0 inside the accept logic, and a FIFO that never accepts a write breaks none of the six properties.

Name the Missing Property

assert property (@(posedge clk) disable iff (rst)
  tracking && do_rd && t_ahead == 0 |-> rdata == t_data);

With it added, all 14 holes are killed, by a_order or its helper a_ahead (the followed entry is still inside the count). The rate goes from 24 of 38 (63 %) to 38 of 38 (100 %) of the mutations that change the design. This is the end-to-end property F3.4 argued for.

Cost and Practice

The campaign above took 49.4 s and 30.3 s on a laptop: one full formal run per mutation, plus an equivalence check per survivor. That is why teams build a fixed list once, rerun it when the properties change, and leave it out of every commit's regression.

Mutating a flop changes the clocking the engine can model, so flops and memories were excluded here. Commercial tools offer the same idea as a coverage view beside cone-of-influence and proof-core coverage (F7.1).

Asked in Interviews

Try It

  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  // registered copies: primary-input history is kept in flops
  reg past = 0, wr_q = 0, rd_q = 0, full_q = 0, empty_q = 0;
  reg [4:0] count_q = 0;
  always @(posedge clk) begin
    past <= !rst; wr_q <= wr; rd_q <= rd; full_q <= full; empty_q <= empty; count_q <= count;
  end
  always @(posedge clk) if (!rst) begin
    a_bound: assert(count <= 5'd16);
    a_level: assert(count == wr_ptr - rd_ptr);
    a_full:  assert(full == (count == 5'd16));
    a_empty: assert(empty == (count == 5'd0));
    if (past && wr_q && full_q && !rd_q) a_nopush: assert(count == count_q);
    if (past && rd_q && empty_q && !wr_q) a_nopop: assert(count == count_q);
  end

[options]
size 40
seed 1
select t:$dff t:$mem_v2 %u %n
tags KILLED SURVIVED EQUIV

[script]
read_verilog -sv fifo16.sv
prep -top fifo16

[files]
fifo16.sv

[logic]
if result("test_props") == "FAIL":
    tag("KILLED")
elif result("test_eq") == "PASS":
    tag("EQUIV")
else:
    tag("SURVIVED")

[report]
print("Killed %d, survived %d, equivalent %d" % (tags("KILLED"), tags("SURVIVED"), tags("EQUIV")))

[test test_props]
expect PASS FAIL
run bash $PRJDIR/test_props.sh

[test test_eq]
expect PASS FAIL
run bash $PRJDIR/test_eq.sh

1. Run the sample

   As loaded, the runner draws four entries (an unmutated control and three mutations) and proves each: COMPLETED: 2 killed, 2 survived, in 2.9 s. The control is one of the survivors.

2. Read the full table

   Find the survivors on the write-data path. Which property would have to fail for each?

3. Change the file, change the sample

   Add the order property (the order block in the shared source) and the runner draws a different sample, because it samples the cells of the file you give it: COMPLETED: 2 killed, 2 survived. Compare rates only on a fixed list.

Check Yourself

module fifo16(input clk, rst, wr, rd, input [7:0] wdata, input pick,
  output [7:0] rdata, output empty, full);
  reg [7:0] mem [0:15];
  reg [4:0] wr_ptr=0, rd_ptr=0, count=0;
  assign empty = count == 5'd0;
  assign full  = count == 5'd16;
  wire do_wr = wr && !full, do_rd = rd && !empty;
  assign rdata = mem[rd_ptr[3:0]];
  always @(posedge clk)
    if (rst) begin wr_ptr <= 0; rd_ptr <= 0; count <= 0; end
    else begin
      if (do_wr) begin mem[wr_ptr[3:0]] <= wdata; wr_ptr <= wr_ptr + 5'd1; end
      if (do_rd) rd_ptr <= rd_ptr + 5'd1;
      count <= count + do_wr - do_rd;
    end
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  // registered copies: primary-input history is kept in flops
  reg past = 0, wr_q = 0, rd_q = 0, full_q = 0, empty_q = 0;
  reg [4:0] count_q = 0;
  always @(posedge clk) begin
    past <= !rst; wr_q <= wr; rd_q <= rd; full_q <= full; empty_q <= empty; count_q <= count;
  end
  always @(posedge clk) if (!rst) begin
    a_bound: assert(count <= 5'd16);
    a_level: assert(count == wr_ptr - rd_ptr);
    a_full:  assert(full == (count == 5'd16));
    a_empty: assert(empty == (count == 5'd0));
    if (past && wr_q && full_q && !rd_q) a_nopush: assert(count == count_q);
    if (past && rd_q && empty_q && !wr_q) a_nopop: assert(count == count_q);
  end
`endif
endmodule