Day 105: SVA II: concurrent assertions, |-> vs |=>, sequences
SVA II: concurrent assertions and sequences
Concurrent assertions check temporal properties across clock cycles. They use an antecedent → consequent form: |-> (overlapping — consequent checked the same cycle the antecedent completes) and |=> (non-overlapping — checked the *next* cycle). Sequences describe multi-cycle patterns with delays (##n) and repetition. Together they express rules like 'every request is acknowledged within 1–3 cycles'.
// after a request, ack must arrive within 1 to 3 cycles
property p_req_ack;
@(posedge clk) disable iff (!rst_n)
req |-> ##[1:3] ack;
endproperty
assert property (p_req_ack) else $error("ack missing after req");
// a two-cycle handshake sequence
sequence s_handshake;
req ##1 gnt ##1 done;
endsequence
assert property (@(posedge clk) start |=> s_handshake);|-> vs |=> is a guaranteed question
'Write a concurrent SVA for a req→ack protocol with a max-latency bound, cold' is a named Stage-3 exit criterion, and '|-> vs |=>' is asked constantly. Crisp answer: |-> checks the consequent on the same cycle the antecedent matches; |=> checks it the following cycle (equivalent to |-> ##1). Know it and the ##[1:3] bounded-response idiom cold.
Key terms
- Concurrent assertion
- A clocked assertion checking a temporal property across cycles.
- |-> (overlapping)
- Implication where the consequent is checked the same cycle the antecedent completes.
- |=> (non-overlapping)
- Implication where the consequent is checked the next cycle (|-> ##1).
- Sequence
- A multi-cycle temporal pattern using ##n delays and repetition operators.
- disable iff
- A guard that voids an assertion during reset or other conditions.
Before moving on, you should be able to
In SVA, how do |-> and |=> differ?
