Property Completeness

Check a property set against the spec, then measure it by mutation: count what it kills, group what survives, and read each group as the property you have not written.

Lesson: F7.2
Time: 25 min
Runs on: SymbiYosys
Check: 5 questions

The spine FIFO had four proven checks and a green dashboard. A mutation run made 36 edits to its RTL that change what a user sees, and 16 of them passed every check. Most of the survivors corrupted data, the one thing a FIFO exists to keep.

Start from the Spec

Spec sentence	Kind	Property in the glue set
The FIFO never holds more than four entries	bound	`a_count`
`empty` and `full` agree with the pointers	bookkeeping	`a_empty`, `a_full`, `a_level`
A pop returns the oldest entry, unchanged	data, order	none
A push into a FIFO with room is accepted	handshake	none
`rdata` while empty	undefined by the spec	none needed

One row per sentence of the spec, filled before any tool runs. Two empty cells are two holes you can see on paper.

Completeness starts with the spec, not the RTL. Write each rule as a row: handshakes, data, order, reset values, errors, bounds. A row with no property is a hole. A row the spec leaves undefined needs none, and the table records that choice.

Mutation Turns the Question Around

One Fault, Two QuestionsMCY edits the RTL once per run, then asks the property set whether it noticed. If it did not, a second run asks whether the edit changed anything a user can see.

Read the diagram as text

fifo4.sv: the RTL only; the bench is never edited
One edit: invert a signal, tie a bit, swap a mux input
Property set, abc pdr: does any check fail?
Killed: a check caught the fault
Miter, abc pdr: do the outputs differ from the original?
Survived: a real fault the set accepts
No change: equal at every output: not a fault

fifo4.sv → One edit
One edit → Property set, abc pdr
Property set, abc pdr → Killed: FAIL
Property set, abc pdr → Miter, abc pdr: PASS
Miter, abc pdr → Survived: differ
Miter, abc pdr → No change: equal

Forty runs per property set, seed 7, register and memory cells excluded. The first run is the unedited design, a control. Each campaign took about 33.3 s.

A property set is good if it fails when the design is wrong. MCY (F6.5) makes one small edit to the RTL and runs the set. A fault the set rejects is killed. One it accepts is a survivor, unless the miter shows the edit changed nothing visible.

The Score, Three Times

Same forty edits, property set	Killed	Survived	No change	Score
Glue set (four checks, F3.4)	20	16	4	56 %
Plus the end-to-end check	34	2	4	94 %
Plus the acceptance check	36	0	4	100 %

Score = killed / (killed + survived). The "no change" column is the control plus 3 edits the miter proved invisible at the outputs.

Survivors grouped by what the edit broke	Glue set	Plus end-to-end	Plus acceptance
accepting a push or a pop	3, 4, 11, 12, 19, 27, 34, 37, 38	12, 19	none
the register update	39	none	none
the data written	6, 16, 21, 23, 26, 30	none	none

Fault numbers from the measured table. Each group names the property that kills it.

The score is a number; the survivors are the finding. Group them by behaviour and each group names a missing property. The data group says "check what comes out": the end-to-end check of F3.4 kills all of it.

The Fault That Outlived the End-to-End Check

Glue + end-to-end

assert property (@(posedge clk) disable iff (rst) pop && !empty |-> rdata == sb0);

Write path that never accepts: Prove PASS (abc pdr).

Plus the acceptance check

assert property (@(posedge clk) disable iff (rst) push && !full |=> !empty);

Same fault: FAIL at reported step 3.

Faults 12 and 19 stop every write. The FIFO stays empty, so a pop of a non-empty FIFO never happens and the end-to-end check never fires. Every check passes because none is ever tested. The covers say so: on this design 4 of four are unreached (F3.2).

Covers do not kill faults; only checks do. The fix is a rule that demands progress: a push into a FIFO with room must leave it non-empty.

Three Measures and One Sample

Measure	The question it answers	Spine, glue set
Cone map (F7.1)	Which logic do the properties read?	memory white
Spec checklist	Which rules have a property?	two empty rows
Mutation score	Would the properties notice a fault?	56 %

Three measures, three questions. A review asks for all three.

A score of 100 % means all 36 of these edits, chosen by one seed. A fault class the tool never makes, such as a missing feature or a two-cycle protocol slip, is unmeasured. Quote the score with its sample.

Asked in Interviews

Question	Answer
How do you know your properties are good enough?	Three checks: a spec checklist with a property per rule, the cone map against the design, and a mutation score with its sample. The survivors matter more than the score.
What is a surviving fault?	An edit to the RTL that changes the outputs and still passes every property. Grouped by behaviour, survivors name the properties you have not written.
Does a 100 % mutation score mean the set is complete?	Complete for that sample of edits. Say how many, which kinds, and which seed; faults the tool cannot make are not measured.

Try It

The lab runs the site's mutation mode on the spine with its glue set: 1 killed, 3 survived, in 2.8 s. It draws four edits, the first a control, from the whole design, and proves each with k-induction at depth 4.

Edit drawn by the lab	Result
Control: no edit	passes, as it must
a mux in the memory write (line 13)	survived
a mux in the count update (line 15)	killed
bit 6 of `wdata` into the memory write (line 13)	survived

Measured. Both survivors touch the data written; the forty-edit campaign above shows the same split.

Run the glue set
Run as it is and read the killed and survived counts. Which spec row do the survivors belong to?
Fill the checklist
Write the property for each empty row of the checklist in concurrent SVA before you look at the twins.
Break the write path
Change wr_en to push && full, add the end-to-end check, set mode prove with abc pdr, and run. Then add the acceptance check.

Top moduleModeDepthEngine

design.sv

props.sv

Use assert property (@(posedge clk) ...);. Leave blank for immediate assertions in the design.

Inputs are free unless constrained. Run to find a counterexample or check a proof.

Model: one positive-edge clock, binary data. Sampled history requires declaration-initialized variables; primary-input history is unsupported.

SBY summary and log

Enable JavaScript to edit and run. The original design and properties follow.

module fifo4sb(input clk, rst, push, pop, input [7:0] wdata,
  output [7:0] rdata, output full, empty);
  reg [7:0] mem [0:3];
  reg [1:0] wr_ptr=0, rd_ptr=0;
  reg [2:0] count=0;
  assign full  = count == 3'd4;
  assign empty = count == 3'd0;
  wire wr_en = push && !full, rd_en = pop && !empty;
  assign rdata = mem[rd_ptr];
  always @(posedge clk)
    if (rst) begin wr_ptr <= 0; rd_ptr <= 0; count <= 0; end
    else begin
      if (wr_en) begin mem[wr_ptr] <= wdata; wr_ptr <= wr_ptr + 2'd1; end
      if (rd_en) rd_ptr <= rd_ptr + 2'd1;
      count <= count + wr_en - rd_en;
    end
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  wire [1:0] f_ptr_diff = wr_ptr - rd_ptr;   // entries between the pointers, modulo 4
  // Modelling code: a shadow copy of the FIFO's contents, in order, oldest in sb0.
  reg [7:0] sb0=0, sb1=0, sb2=0, sb3=0;
  reg [2:0] sb_n=0;
  wire [2:0] slot = sb_n - (rd_en ? 3'd1 : 3'd0);   // where an accepted push lands
  always @(posedge clk)
    if (rst) sb_n <= 0;
    else begin
      if (rd_en) begin sb0 <= sb1; sb1 <= sb2; sb2 <= sb3; end
      if (wr_en) case (slot)
        3'd0: sb0 <= wdata;  3'd1: sb1 <= wdata;  3'd2: sb2 <= wdata;  default: sb3 <= wdata;
      endcase
      sb_n <= sb_n + wr_en - rd_en;
    end
  always @(posedge clk) if (!rst) begin
    if (empty) assert(wr_ptr == rd_ptr);   // glue
    if (full)  assert(wr_ptr == rd_ptr);   // glue
    assert(count <= 3'd4);                 // glue
    assert(count == f_ptr_diff || count == 3'd4 && f_ptr_diff == 2'd0);   // glue
  end
`endif
endmodule

Check Yourself

Predict the outputThe spine with glue and end-to-end checks, and wr_en = push && full (writes never accepted). mode prove, abc pdr, reset assumed in step 0. The verdict is:

module fifo4sb(input clk, rst, push, pop, input [7:0] wdata,
  output [7:0] rdata, output full, empty);
  reg [7:0] mem [0:3];
  reg [1:0] wr_ptr=0, rd_ptr=0;
  reg [2:0] count=0;
  assign full  = count == 3'd4;
  assign empty = count == 3'd0;
  wire wr_en = push && full,      // fault: the full test is inverted
       rd_en = pop && !empty;
  assign rdata = mem[rd_ptr];
  always @(posedge clk)
    if (rst) begin wr_ptr <= 0; rd_ptr <= 0; count <= 0; end
    else begin
      if (wr_en) begin mem[wr_ptr] <= wdata; wr_ptr <= wr_ptr + 2'd1; end
      if (rd_en) rd_ptr <= rd_ptr + 2'd1;
      count <= count + wr_en - rd_en;
    end
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  wire [1:0] f_ptr_diff = wr_ptr - rd_ptr;   // entries between the pointers, modulo 4
  // Modelling code: a shadow copy of the FIFO's contents, in order, oldest in sb0.
  reg [7:0] sb0=0, sb1=0, sb2=0, sb3=0;
  reg [2:0] sb_n=0;
  wire [2:0] slot = sb_n - (rd_en ? 3'd1 : 3'd0);   // where an accepted push lands
  always @(posedge clk)
    if (rst) sb_n <= 0;
    else begin
      if (rd_en) begin sb0 <= sb1; sb1 <= sb2; sb2 <= sb3; end
      if (wr_en) case (slot)
        3'd0: sb0 <= wdata;  3'd1: sb1 <= wdata;  3'd2: sb2 <= wdata;  default: sb3 <= wdata;
      endcase
      sb_n <= sb_n + wr_en - rd_en;
    end
  always @(posedge clk) if (!rst) begin
    if (empty) assert(wr_ptr == rd_ptr);   // glue
    if (full)  assert(wr_ptr == rd_ptr);   // glue
    assert(count <= 3'd4);                 // glue
    assert(count == f_ptr_diff || count == 3'd4 && f_ptr_diff == 2'd0);   // glue
    if (pop && !empty) assert(rdata == sb0);   // end-to-end
  end
`endif
endmodule

Predict the outputThe same faulty design with push && !full |=> !empty added (as a registered copy), mode prove, abc pdr, reset assumed in step 0. At which step does SBY report the failure?

module fifo4sb(input clk, rst, push, pop, input [7:0] wdata,
  output [7:0] rdata, output full, empty);
  reg [7:0] mem [0:3];
  reg [1:0] wr_ptr=0, rd_ptr=0;
  reg [2:0] count=0;
  assign full  = count == 3'd4;
  assign empty = count == 3'd0;
  wire wr_en = push && full,      // fault: the full test is inverted
       rd_en = pop && !empty;
  assign rdata = mem[rd_ptr];
  always @(posedge clk)
    if (rst) begin wr_ptr <= 0; rd_ptr <= 0; count <= 0; end
    else begin
      if (wr_en) begin mem[wr_ptr] <= wdata; wr_ptr <= wr_ptr + 2'd1; end
      if (rd_en) rd_ptr <= rd_ptr + 2'd1;
      count <= count + wr_en - rd_en;
    end
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  wire [1:0] f_ptr_diff = wr_ptr - rd_ptr;   // entries between the pointers, modulo 4
  // Modelling code: a shadow copy of the FIFO's contents, in order, oldest in sb0.
  reg [7:0] sb0=0, sb1=0, sb2=0, sb3=0;
  reg [2:0] sb_n=0;
  wire [2:0] slot = sb_n - (rd_en ? 3'd1 : 3'd0);   // where an accepted push lands
  always @(posedge clk)
    if (rst) sb_n <= 0;
    else begin
      if (rd_en) begin sb0 <= sb1; sb1 <= sb2; sb2 <= sb3; end
      if (wr_en) case (slot)
        3'd0: sb0 <= wdata;  3'd1: sb1 <= wdata;  3'd2: sb2 <= wdata;  default: sb3 <= wdata;
      endcase
      sb_n <= sb_n + wr_en - rd_en;
    end
  reg acc_q = 0;   // registered copy: a push into a FIFO with room
  always @(posedge clk) acc_q <= !rst && push && !full;
  always @(posedge clk) if (!rst) begin
    if (empty) assert(wr_ptr == rd_ptr);   // glue
    if (full)  assert(wr_ptr == rd_ptr);   // glue
    assert(count <= 3'd4);                 // glue
    assert(count == f_ptr_diff || count == 3'd4 && f_ptr_diff == 2'd0);   // glue
    if (pop && !empty) assert(rdata == sb0);   // end-to-end
    if (acc_q) assert(!empty);   // accepted
  end
`endif
endmodule

ConceptWhy does one surviving fault say more than the number of properties?

It is a concrete wrong design that every property accepts.It shows that the original, unedited design has a bug in it.More properties would always have raised the score further.It shows that the solver failed to finish one of its proofs.

ConceptWhich statement about a mutation score is wrong?

The sample of edits is fixed by a seed and is reported.A 100 % score proves the property set is complete.An edit with no visible effect must not count as a miss.A survivor names a behaviour that no property checks.

ConceptWith the end-to-end check added, faults 12 and 19 still survive. What do they share?

Both are invisible at the outputs, so they are no faults.Both change the outputs only after twenty cycles.The FIFO never accepts a write, so no check ever fires.Both corrupt the data on its way into the memory.

Remember

Completeness starts with a spec checklist: one row per rule, an empty property cell is a visible hole.
Mutation measures whether the properties would notice a fault; the survivors, grouped by behaviour, name the missing properties.
A check that never fires kills nothing: a FIFO that accepts no data passes every end-to-end check.
Quote a mutation score with its sample: how many edits, which kinds, which seed.

Find Your Next Track

Put Your Skills to Work

Prepare to Explain Your Thinking

An Idea to Try? Pick a Tool.