Cover Properties as a Sanity Check

Assertions ask "can anything go wrong?". Covers ask the opposite question: "can this good or interesting thing happen at all?". A formal setup without covers can be blind and you would not know it. A setup with a cover for every state, every important event and every corner case of the specification shows that the search really contains the behavior the assertions are about. This article shows how to write such covers, how to read their results, and how to get cover traces from the lab, whose panel runs assertions only.

9 min read | Intermediate

What You'll Learn

• Write cover properties for states, events and corner cases
• Read reached and unreached cover results and decide what an unreached cover means
• Use cover traces as quick examples of how a design behaves
• Get a cover trace from the lab by asserting the negation

What Covers Are For

A cover property describes a situation and asks the tool for a trace that reaches it:

c_full: cover property (@(posedge clk) disable iff (rst) full);
c_wrap: cover property (@(posedge clk) disable iff (rst) full ##1 !full ##[1:4] full);

The answer is either a trace, often the shortest one, or the statement that the situation is unreachable within the depth. Covers have three jobs:

• Sanity: show that the setup is not over-constrained and that the triggers of the assertions happen. This is the job from the vacuity article.
• Specification check: every situation the specification allows should be reachable. An unreachable one is a bug in the design, the assumptions or the specification.
• Examples: a cover trace is a waveform of the design doing something, produced without a testbench. Designers use them to see a new block work before any simulation exists.

What to Cover

• Every state of every state machine, and the important transitions.
• Every output event: a grant to each requester, a full and an empty FIFO, an error response.
• The trigger of every implication.
• Corner cases from the specification: two events in the same cycle, an event right after reset, the maximum count.

The Design: a Controller With an Error State

This state machine runs a job and can end it in DONE or in FAIL. The specification says: if stop and err arrive in the same cycle, the error wins.

module fsm_cover (input clk, input rst, input start, input stop, input err,
                  output reg [1:0] state);
  localparam IDLE = 2'd0, RUN = 2'd1, DONE = 2'd2, FAIL = 2'd3;
  always @(posedge clk)
    if (rst) state <= IDLE;
    else case (state)
      IDLE: if (start)      state <= RUN;
      RUN:  if (stop)       state <= DONE;
            else if (err)   state <= FAIL;   // bug: stop has priority, but the spec says err wins
      DONE:                 state <= IDLE;
      FAIL: if (!err)       state <= IDLE;
    endcase
endmodule

The covers: one per state, and one for the collision from the specification.

c_run:  cover property (@(posedge clk) disable iff (rst) state == RUN);
c_done: cover property (@(posedge clk) disable iff (rst) state == DONE);
c_fail: cover property (@(posedge clk) disable iff (rst) state == FAIL);
c_coll: cover property (@(posedge clk) disable iff (rst) state == RUN && err && stop ##1 state == FAIL);

Reading the Results

SymbiYosys in cover mode reports each cover separately (shortened, with the covered condition added in brackets):

Reached cover statement in step 3 at fsm_cover: design.sv:21  (state == RUN)
Reached cover statement in step 4 at fsm_cover: design.sv:22  (state == DONE)
Reached cover statement in step 4 at fsm_cover: design.sv:23  (state == FAIL)
Unreached cover statement at fsm_cover: design.sv:24          (err and stop together -> FAIL)
DONE (FAIL, rc=2)

Every state is reachable, so the setup is not blind. But the collision case is unreachable: with err and stop together, the machine goes to DONE, never to FAIL. No assertion was written for the priority rule, so only the cover finds the mismatch with the specification. Swap the two branches so err is tested first, and all four covers are reached.

An unreached cover has three possible causes, and the fix depends on which:

• A design bug, as here: the design cannot do what the specification requires.
• An over-constraint: an assumption removes the inputs needed. Remove assumptions one by one to find it.
• Too little depth: the situation needs more cycles. Increase the depth and run again.

Running It in ChipVerify Lab

The lab panel runs only the assertion check. To ask a reachability question there, assert the negation of the cover: "this never happens". If the situation is reachable, the assertion fails, and the counterexample is exactly the cover trace you wanted.

The trace above comes from assert (!(state == FAIL)): the lab engine "fails" at step 4 and shows the machine starting a job in step 1 and taking an error in step 2. For the collision case, the example uses:

// the same question for the lab panel: meant to fail if the collision case is reachable
always @(posedge clk)
  if (!init && !$past(rst))
    assert (!($past(state) == RUN && $past(err) && $past(stop) && state == FAIL));   // meant to fail

On the buggy design this passes, which means the collision case is unreachable. After the fix it fails at step 4, with a trace that shows err and stop arriving together and the machine going to FAIL. Mark such checks clearly in comments, so that nobody "fixes" them later.

Common Mistakes

RUN:  if (err)        state <= FAIL;
      else if (stop)  state <= DONE;

always @(posedge clk)
  if (!init && !rst && !$past(rst) && $past(state) == RUN && $past(err))
    assert (state == FAIL);