Concurrent Assertions and Temporal Logic

The previous article checked a fact at one instant. This one checks a rule across several clock cycles.

Go back to the request/acknowledge handshake in Section 7.5. The rule that protocol is supposed to guarantee is not a single-instant fact but a temporal one: if req is asserted, ack must rise within some bounded number of cycles. An immediate assertion, evaluated at one moment, has no way to say “and then, some cycles later, this other thing happens”. Concurrent assertions, the core of SystemVerilog Assertions (SVA), exist to close that gap.

The ## operator: a fixed number of cycles

The building block of every temporal expression is ##N, N clock cycles later:

// "req is true on some cycle, and exactly 2 cycles after that, ack is true"
sequence req_then_ack_2;
    req ##2 ack;
endsequence

Read req ##2 ack as a sequence: req true on one cycle, then ack true two cycles later. A concurrent assertion needs a clocking event, @(posedge clk), to define what “one cycle” means, the same clocking idea used everywhere since Module 3, now applied to a check rather than a design.

The implication operators: |-> and |=>

A bare sequence like req ##2 ack would be checked unconditionally every cycle, which is usually not what you want. You want “whenever req happens, ack must follow”. The implication operators say exactly that. The left side, the antecedent, is a trigger; the right side, the consequent, is what must then hold.

// Overlapping implication: if req is true THIS cycle, the consequent starts
// being evaluated on this same cycle, so ##2 ack means ack two cycles later
property req_ack_implication;
    @(posedge clk) req |-> ##2 ack;
endproperty

assert property (req_ack_implication);

There are two forms, and the difference is one clock cycle:

• a |-> b is the overlapping implication. The consequent is evaluated starting on the same cycle the antecedent matched. a |-> b with no delay means b must be true on the very cycle a is true.
• a |=> b is the non-overlapping implication. The consequent starts one cycle after the antecedent. a |=> b is exactly a |-> ##1 b.

// req |=> ack means: if req is true this cycle, ack must be true NEXT cycle
property ack_next_cycle;
    @(posedge clk) req |=> ack;
endproperty

Figure 1 shows both. For “something must follow on a later cycle”, either form works as long as you count the delay correctly: req |=> ##1 ack and req |-> ##2 ack both mean ack two cycles after req.

A realistic example: the FIFO’s own contract

Recall the synchronous FIFO from Section 7.4. Once full asserts, it should stay asserted at least until a read happens; a full flag that flickers on and off within a cycle would indicate a miscalculated comparison. A concurrent assertion can check that continuously, in every simulation that exercises the module:

// Once full rises, it must still be true on the next cycle unless a read
// was accepted in between
property full_is_stable;
    @(posedge clk) $rose(full) && !rd_en |=> full;
endproperty

assert property (full_is_stable)
else $error("full dropped without a read: FIFO flag logic suspect");

$rose(full) is an SVA built-in, true exactly on the cycle full goes from 0 to 1. With |=>, the property reads as English: whenever full has just risen and nobody is reading, it must still be true on the next cycle. That is a multi-cycle claim an immediate assertion has no way to express.

Bus protocol specifications, AXI, PCIe, USB, are in practice substantially expressed and checked as libraries of exactly these assertions, often supplied by the standards body or an IP vendor as a ready-made protocol checker you drop into the testbench. When you write your own protocol, as you will for the UART and SPI projects in Module 10, hand-writing a few of these for your own timing guarantees catches integration bugs long before a functional test would.

Practice Exercise

For the SPI-style protocol in Module 10, write a concurrent assertion checking that when cs_n (active-low chip select) falls, sclk does not toggle on the following cycle, a common settling-time requirement. Assume a signal cs_n_falling is true exactly on the cycle cs_n goes low.

property cs_settle_before_clock;
    @(posedge clk) cs_n_falling |=> $stable(sclk);
endproperty

assert property (cs_settle_before_clock)
else $error("sclk toggled immediately after cs_n fell: settling time violated");

Concurrent assertions check relationships that span clock cycles, which an immediate assertion bound to one instant cannot. ##N counts cycles, |-> and |=> express “whenever this happens, that must follow”, differing by whether the consequent starts on the same cycle or the next, and built-ins like $rose, $fell and $stable give the vocabulary for edge-based temporal behaviour. In the next article, the last in this module, we make sequence and property named, reusable declarations, the structure every real assertion library is built from.