assert, assume and cover

A formal check is built from three kinds of statement: assert, assume and cover. They look alike, but the tool treats them in completely different ways. An assertion is a rule to check, an assumption is a rule the tool must obey when it chooses inputs, and a cover asks whether something can happen at all. This article shows all three on a small pulse timer, with real results from the lab engine.

10 min read | Beginner to Intermediate

What You'll Learn

• Explain what the tool does with an assertion, an assumption and a cover
• Use an assumption to rule out input sequences that cannot happen in the real system
• Use a cover to check that a formal run still reaches the situations you care about
• Recognize an over-constrained run, where a too-strong assumption hides everything

Three Kinds of Statement

• assert: "this must always be true". The tool searches for inputs that make it false. If it finds them, you get a counterexample.
• assume: "only consider inputs for which this is true". The tool never breaks an assumption. Every input sequence that violates it is removed from the search.
• cover: "show me that this can happen". The tool searches for inputs that make it true. If it finds them, you get an example trace. If it cannot, the situation is unreachable.

The same condition can be written with any of the three keywords. What changes is the question the tool answers.

The Design: A Pulse Timer

This timer raises busy for 3 cycles after a start pulse, for example to hold off a second request while a memory finishes a write:

module pulse_timer (input clk, input rst, input start, output busy);
  reg [1:0] cnt;
  assign busy = (cnt != 2'd0);
  always @(posedge clk)
    if (rst)             cnt <= 2'd0;
    else if (start)      cnt <= 2'd3;
    else if (cnt != 0)   cnt <= cnt - 2'd1;
endmodule

The rule to check: busy is never high for more than 3 cycles in a row. In SVA, "high for 4 cycles in a row" is the sequence busy [*4], and the property says that it never happens:

a_run: assert property (@(posedge clk) disable iff (rst) not (busy [*4]));

The operator [*4] is a repetition: the expression holds in 4 consecutive cycles. Chapter 3 covers sequences and repetition.

The Assertion Fails Without an Assumption

Run the check with only the assertion. The lab engine fails at step 7 with this counterexample:

The tool pulsed start again while the timer was already busy. Each new start reloads the counter with 3, so busy stays high for 6 cycles. The design does what its code says. The question is whether this input can happen in the real system.

Suppose the specification of the block that drives start says: "never send a new start while the timer is busy". Then this counterexample is impossible in the chip, and the tool must be told so. That is the job of an assumption.

Adding the Assumption

In SVA:

m_start: assume property (@(posedge clk) disable iff (rst) busy |-> !start);

In the form the lab reads, together with the assertion. The rule "never more than 3 cycles" needs a small helper counter, run, that counts how long busy has been high, because the open-source front end does not read [*4]:

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);

  // assumption: no new start while the timer is busy
  always @(*) if (!init && busy) assume (!start);

  // busy is never high for more than 3 cycles in a row
  reg [2:0] run = 3'd0;
  always @(posedge clk) run <= (busy && !rst) ? run + 3'd1 : 3'd0;
  always @(posedge clk) if (!init) assert (run <= 3'd3);
`endif

With the assumption, the run passes at depth 10. The tool still tries every input sequence, except the ones where start arrives during busy.

Assumptions Are Promises About the Environment

Every assumption is a promise that the rest of the system keeps. If the promise is true, the pass is valid. If it is false, the pass is worthless, because the tool never looked at the input sequences that really happen.

That is why assumptions are written with care, kept as few as possible, and each one is traced to the specification. A common practice is to check the same rule as an assertion on the other side of the interface. The block that drives start asserts busy |-> !start, and the timer assumes it. This is called assume-guarantee reasoning, and Chapter 4 covers it.

Cover: Is Anything Still Happening?

An assumption that is too strong can remove every interesting input sequence. The assertions then pass trivially, because nothing happens. A cover statement protects you from this. It asks the tool to find at least one trace in which a situation happens.

For the timer, a useful cover is "a busy period ends": busy was high and is now low. In SVA:

c_end: cover property (@(posedge clk) disable iff (rst) busy ##1 !busy);

The operator ##1 means "one cycle later". In the lab form, using $past for the previous cycle and skipping the cycle right after reset:

always @(posedge clk) if (!init && !$past(rst)) cover ($past(busy) && !busy);

Covers are checked in a separate mode of SymbiYosys, called cover mode, where the tool searches for traces that reach each cover. The formal panel of the lab runs the assertion check only, so it skips cover statements. Here is the cover-mode output of the same engine, for reference:

SBY [run] engine_0: ##   0:00:00  Checking cover reachability in step 0..
...
SBY [run] engine_0: ##   0:00:00  Checking cover reachability in step 6..
SBY [run] engine_0: ##   0:00:00  Reached cover statement in step 6 at pulse_timer: design.sv:20.51-20.79
SBY [run] summary: cover trace: run/engine_0/trace0.vcd
SBY [run] DONE (PASS, rc=0)

The cover is reached in step 6: reset in step 0, a start in step 1, busy high in steps 2 to 4, low in step 5, and the clocked cover reports it at the next edge. The trace is an example of the timer working normally, which is useful in itself as a quick look at the design.

An Over-Constrained Run

Now make the assumption too strong by mistake: "start is never high" instead of "start is not high while busy".

always @(*) if (!init) assume (!start);   // too strong

The assertion check still passes. The timer never starts, so busy is never high, and the rule about busy periods holds trivially. Nothing in the assertion result warns you. The cover does:

SBY [run] engine_0: ##   0:00:00  Checking cover reachability in step 9..
SBY [run] engine_0: ##   0:00:00  Unreached cover statement at pulse_timer: design.sv:20.51-20.79
SBY [run] summary: unreached cover statements:
SBY [run] DONE (FAIL, rc=2)

An unreached cover for a situation that must be possible is a red flag. Either an assumption is too strong, or the design is stuck. Formal engineers write covers for the main activity of every block for exactly this reason.

Running It in ChipVerify Lab

The example below is the pulse timer with the assumption, the assertion and the cover. The lab runs the assertion check and passes. Comment out the assumption line and run again to see the counterexample of this article. The cover line is kept in the file because commercial tools and SymbiYosys cover mode use it, but the lab panel does not report it.

Common Mistakes

// busy rose one cycle ago
always @(posedge clk)
  if (!init && !rst && !$past(rst) && !$past(rst, 2) && $past(busy) && !$past(busy, 2))
    assert (busy);
// busy rose two cycles ago
always @(posedge clk)
  if (!init && !rst && !$past(rst) && !$past(rst, 2) && !$past(rst, 3) && $past(busy, 2) && !$past(busy, 3))
    assert (busy);