Sequences and Implication

Most interesting rules span several clock cycles: "after a start, done comes within 3 cycles", "a request is held until it is granted", "busy is never high for more than 4 cycles in a row". SVA describes such behavior with sequences, built from cycle delays and repetitions, and with implication, which says when a sequence must hold. This article explains the operators you will use every day and checks a latency rule on a small job unit with a real bug.

11 min read | Beginner to Intermediate

What You'll Learn

• Build sequences with ##N, ##[m:n] and the repetition [*N]
• Use the implications |-> and |=> and explain the difference
• Write a latency rule with a window, such as "done within 1 to 3 cycles"
• Express the same rules in the lab with helper counters and $past

Sequences

A sequence is a pattern of conditions over consecutive clock cycles. The basic operator is the cycle delay ##:

• a ##1 b: a in one cycle and b in the next.
• a ##2 b: b two cycles after a. The cycle in between can hold anything.
• a ##[1:3] b: b one, two or three cycles after a. The range is inclusive.
• a ##[1:$] b: b at some point after a, with no upper limit.

Repetition says that a condition holds over several cycles in a row:

• a [*3]: a in three consecutive cycles, the same as a ##1 a ##1 a.
• a [*2:4]: a in two to four consecutive cycles.

A sequence on its own is not a rule. It describes a pattern that may or may not happen. To turn it into a property, you either say it must never happen, as in not (busy [*5]), or you use an implication.

Implication

Implication connects a trigger to a consequence. It is written trigger |-> consequence or trigger |=> consequence:

• a |-> b is the overlapping implication: whenever a holds, b must hold in the same cycle.
• a |=> b is the non-overlapping implication: whenever a holds, b must hold in the next cycle. It is the same as a |-> ##1 b.

Both sides can be sequences. When the trigger is a sequence, the consequence starts in the last cycle of the trigger (for |->) or the cycle after it (for |=>). For example, req ##1 !ack |=> req says: if there is a request and no acknowledge in the next cycle, the request must still be there one cycle later.

The most important property of implication: if the trigger does not happen, the property passes in that cycle without checking anything. This is called a vacuous pass. It is what you want most of the time, but it also means that a trigger that never happens makes the whole property meaningless. Chapter 4 covers vacuity and how covers protect you from it.

The Design: a Job Unit With Two Latencies

This unit accepts a job on start and signals done when it is finished. A short job takes 1 cycle and a long job, marked by long, takes 3. It is the kind of timing a memory controller has for a hit and a miss. The counter is loaded with the remaining time and done is high when it reaches 1:

module delay_unit (input clk, input rst, input start, input long, output done, output busy);
  reg [2:0] cnt;
  assign busy = (cnt != 3'd0);
  assign done = (cnt == 3'd1);
  always @(posedge clk)
    if (rst)                 cnt <= 3'd0;
    else if (start && !busy) cnt <= long ? 3'd4 : 3'd1;   // bug: a long job should load 3
    else if (busy)           cnt <= cnt - 3'd1;
endmodule

The long job loads 4, so it takes one cycle more than the specification allows.

The Properties

The specification says: a new job only starts when the unit is idle, and every job is done within 1 to 3 cycles.

m_nostart: assume property (@(posedge clk) disable iff (rst) busy |-> !start);
a_lat:     assert property (@(posedge clk) disable iff (rst) start |-> ##[1:3] done);

The assumption keeps the tool from starting a job while one is running, which the unit does not support. The assertion is a latency window. It does not care whether the job is short or long, only that it finishes in time. You can also state each latency exactly:

a_short: assert property (@(posedge clk) disable iff (rst) start && !long |=> done);
a_long:  assert property (@(posedge clk) disable iff (rst) start && long |=> !done [*2] ##1 done);

a_long reads: after a long start, done is low for two cycles and then high. The window rule is looser and easier to keep when the design changes. The exact rules catch more bugs, as the exercise shows.

Running It in ChipVerify Lab

The lab engine has no ##. Multi-cycle rules are written with a small helper counter that measures time, plus an ordinary assertion on the counter. For the latency window, the counter waited counts the cycles since the start, and the rule says it never passes 3:

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(*) if (busy) assume (!start);           // no new job while busy
  // start |-> ##[1:3] done, written with a helper counter: cycles waited since the start
  reg [2:0] waited = 3'd0;
  always @(posedge clk)
    if (rst || done)           waited <= 3'd0;
    else if (start || waited)  waited <= waited + 3'd1;
  always @(posedge clk) if (!init) assert (waited <= 3'd3);
  // done never comes without a job
  always @(posedge clk) if (!init && done) assert (waited != 3'd0);
`endif

This pattern, a counter that measures time and an assertion on its value, is how bounded multi-cycle rules are written in any language without sequences. Commercial tools build the same kind of monitor internally from the SVA. The second assertion checks the other direction: a done with no job waiting is also a bug.

The run fails at step 6:

A long job starts in step 1. The counter is loaded with 4, counts down, and reaches 1 in step 5, so done comes four cycles after the start. waited is 4 in step 5, and the assertion reports it in step 6. Load 3 instead of 4 and the run passes.

Translating Other Operators

The same idea works for the other operators:

Remember the reset guard for every $past: a check that looks back n cycles must skip cycles whose history includes a reset or the start of the trace.

Common Mistakes

// a short job is done exactly 1 cycle after the start
always @(posedge clk)
  if (!init && !rst && !$past(rst) && $past(start) && !$past(long))
    assert (done);
// a long job is done exactly 3 cycles after the start, and not before
always @(posedge clk)
  if (!init && !rst && !$past(rst) && !$past(rst, 2) && !$past(rst, 3) && $past(start, 3) && $past(long, 3))
    assert (done);
always @(posedge clk)
  if (!init && !rst && !$past(rst) && $past(start) && $past(long))
    assert (!done);