Invariants

The simplest and most useful properties are invariants: conditions that must be true in every cycle, whatever happened before. A counter stays in its range, a grant vector has at most one bit set, a FIFO is never full and empty at once. This article shows the common kinds of invariants, the SVA functions that make them short, and a real bug in a priority arbiter that a one-line invariant finds.

9 min read | Beginner to Intermediate

What You'll Learn

• Recognize the common kinds of invariants: range, one-hot, mutual exclusion and consistency
• Use $onehot, $onehot0, $countones and $isunknown
• Find a double-grant bug in a priority arbiter with one invariant
• Write invariants that relate a registered output to the inputs of the previous cycle

What an Invariant Is

An invariant is a property with no time in it. It does not say "after A, then B". It says "this is always true". In SVA it is a concurrent assertion whose body is a plain expression:

a_range: assert property (@(posedge clk) disable iff (rst) count <= 3'd4);

Invariants are the first properties to write for any block, for three reasons. They are easy to state from the specification. They catch a large share of real bugs, because most bugs eventually put the design in a state that should not exist. And, as Chapter 6 shows, they are the building blocks of full proofs.

Common Kinds of Invariants

• Range: a value stays within its legal range. count <= 4, state is one of the defined states, a pointer is below the memory size.
• One-hot: exactly one bit of a vector is set, for example a one-hot state register. $onehot(state).
• At most one: zero or one bit is set, for example the grants of an arbiter or the selects of a multiplexer. $onehot0(gnt).
• Mutual exclusion: two conditions are never true together. !(full && empty), !(rd_en && wr_en) on a single-port memory.
• Consistency: two signals that encode related information agree. empty == (count == 0), or a status bit matches the state it reports.
• No unknown values: outputs are never X after reset. !$isunknown(dout). This one matters in simulation. A formal tool works with 0 and 1 only, so it does not check it.

The system functions do the bit counting for you:

The Design: a Priority Arbiter

An arbiter decides which of several requesters may use a shared resource, such as a bus or a memory port. This one has four requesters with fixed priority: requester 0 wins over 1, 1 over 2, and 2 over 3. The grant is registered, so it appears one cycle after the request:

module prio_arb (input clk, input rst, input [3:0] req, output reg [3:0] gnt);
  wire [3:0] nxt;
  assign nxt[0] = req[0];
  assign nxt[1] = req[1] & ~req[0];
  assign nxt[2] = req[2] & ~req[1];               // bug: forgets req[0]
  assign nxt[3] = req[3] & ~(|req[2:0]);
  always @(posedge clk)
    if (rst) gnt <= 4'b0000;
    else     gnt <= nxt;
endmodule

The grant for requester 2 should be blocked by requesters 0 and 1, but the code only checks requester 1. It is the kind of slip that is easy to make when a pattern is typed by hand.

The Invariants

Three rules come straight from the specification of an arbiter:

// at most one grant
a_onehot: assert property (@(posedge clk) disable iff (rst) $onehot0(gnt));
// no grant to a requester that did not ask in the previous cycle
a_subset: assert property (@(posedge clk) disable iff (rst) ##1 (gnt & ~$past(req)) == 4'b0000);
// some request in one cycle means some grant in the next
a_some:   assert property (@(posedge clk) disable iff (rst) (req != 4'b0000) |=> (gnt != 4'b0000));

The first one is a pure invariant. The other two relate the registered grant to the requests of the previous cycle, so they look one cycle back with $past or forward with |=>. The ##1 at the start of a_subset skips the first cycle, where $past(req) has no earlier value to return. The $past, $rose, $fell and $stable article explains this trap.

None of the three rules says which requester wins. That is deliberate. They hold for any correct arbiter, fixed priority or round robin, so they are cheap to write and can be reused. The exercise adds the priority rule.

Running It in ChipVerify Lab

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // at most one grant
  always @(posedge clk) if (!init) assert ($onehot0(gnt));
  // no grant without a request (in the previous cycle)
  always @(posedge clk) if (!init && !$past(rst)) assert ((gnt & ~$past(req)) == 4'b0000);
  // some grant when there was some request
  always @(posedge clk) if (!init && !$past(rst)) assert (($past(req) != 0) == (gnt != 0));
`endif

The lab engine reads $onehot0 directly. The third assertion is a little stronger than a_some: it also says that no request means no grant.

The run fails at step 3:

Reading it backwards: in step 2 the grant is 0101, two grants at once. In step 1 the requests were 0101: requesters 0 and 2. Requester 0 is granted because it has the highest priority. Requester 2 is granted because its logic checks only requester 1, which was not asking. The other two invariants hold in this trace. Only the one-hot rule sees the problem.

Change the line to assign nxt[2] = req[2] & ~(|req[1:0]); and the run passes.

Invariants and Reachable States

An invariant claims something about every state the design can reach from reset. A bounded run checks this for the states reachable within the depth. For the arbiter, every state is reachable in one cycle, because the grant depends only on the last requests, so a short depth already covers everything. For a counter or a FIFO, deeper states need more cycles. Chapter 6 shows how a full proof covers all reachable states, and why invariants are what makes such a proof work.

Common Mistakes

always @(posedge clk)
  if (!init && !$past(rst))
    assert (gnt == ($past(req) & (~$past(req) + 4'd1)));