2. SVA Guide - Concurrent Assertions

Concurrent assertions check temporal relationships between signals over multiple clock cycles. Unlike immediate assertions that execute procedurally, concurrent assertions are evaluated continuously throughout simulation based on a sampling clock.

Concurrent vs Immediate Assertions

Aspect	Immediate	Concurrent
Evaluation	Procedural, single point in time	Continuous, across clock cycles
Syntax	assert(expression)	assert property(...)
Clock	Not required	Required (sampling event)
Use case	Combinational checks	Protocol/timing checks

Basic Structure

Concurrent assertions use sequences and properties:

// Sequence: defines a pattern of signals over time
sequence req_ack_seq;
  req ##[1:3] ack;  // ack within 1-3 cycles after req
endsequence

// Property: adds temporal context (clock, disable conditions)
property req_ack_prop;
  @(posedge clk) disable iff (reset)
  req |-> req_ack_seq;
endproperty

// Assertion: activates the property check
assert property (req_ack_prop) else $error("Protocol violation");

Implication Operators

Implication defines a cause-effect relationship: "if antecedent is true, then consequent must follow."

Overlapping Implication |->

Consequent evaluation starts at the same cycle where antecedent matches.

property req_grant;
  @(posedge clk) req |-> ##2 grant;  // grant 2 cycles after req
endproperty

{ "signal": [
  { "name": "clk",   "wave": "p.....|..." },
  { "name": "req",   "wave": "0.1...|0.." },
  { "name": "grant", "wave": "0...1.|0..", "node": "....a" }
], "edge": [], "head": { "text": "Overlapping |->: grant checked 2 cycles from req" } }

Non-overlapping Implication |=>

Consequent evaluation starts at the next cycle after antecedent matches.

property req_grant_next;
  @(posedge clk) req |=> ##1 grant;  // grant 2 cycles after req (1+1)
endproperty

a |=> b is equivalent to a |-> ##1 b

Temporal Operators

Operator	Meaning	Example
##n	Delay of n cycles	req ##2 ack
##[m:n]	Delay range m to n cycles	req ##[1:3] ack
##[0:$]	Eventually (0 to infinity)	req ##[0:$] ack
[*n]	Consecutive repetition n times	busy[*3]
[*m:n]	Repetition m to n times	busy[*1:4]
[->n]	Goto repetition (non-consecutive)	ack[->2]
[=n]	Non-consecutive repetition	ack[=2]

Common Patterns

Request-Acknowledge

property req_ack;
  @(posedge clk) disable iff (reset)
  req |-> ##[1:4] ack;  // ack within 1-4 cycles
endproperty
assert property (req_ack);

Signal Stability

property data_stable;
  @(posedge clk) disable iff (reset)
  valid |-> $stable(data) [*1:$] ##1 !valid;
endproperty

One-Hot Check

property onehot_state;
  @(posedge clk) $onehot(state);
endproperty

No Back-to-Back Requests

property no_b2b_req;
  @(posedge clk) disable iff (reset)
  req |=> !req;  // req cannot be high in consecutive cycles
endproperty

System Functions in Assertions

Function	Description
$rose(sig)	True on 0→1 transition
$fell(sig)	True on 1→0 transition
$stable(sig)	True if value unchanged
$changed(sig)	True if value changed
$past(sig, n)	Value of sig n cycles ago
$onehot(sig)	True if exactly one bit is 1
$onehot0(sig)	True if at most one bit is 1
$countones(sig)	Number of 1s in vector

Binding Assertions to Modules

Use bind to attach assertions to RTL without modifying it:

module apb_protocol_checker (input clk, psel, penable, pready);
  
  property apb_setup_phase;
    @(posedge clk) $rose(psel) |-> !penable;
  endproperty
  
  property apb_access_phase;
    @(posedge clk) (psel && !penable) |=> penable;
  endproperty
  
  assert property (apb_setup_phase) else $error("APB setup violation");
  assert property (apb_access_phase) else $error("APB access violation");
  
endmodule

// Bind to DUT
bind apb_master apb_protocol_checker chk (
  .clk(pclk), .psel(psel), .penable(penable), .pready(pready)
);

Cover Directive

Use cover to track if a scenario occurred during simulation:

cover property (@(posedge clk) req ##[1:2] ack);
// Reports how many times req was followed by ack in 1-2 cycles

Key Points

• Concurrent assertions sample signals at clock edges (preponed region)
• Use disable iff for reset conditions
• Vacuous pass: if antecedent is false, assertion passes trivially
• Assertions can be placed in modules, interfaces, or bound externally
• Use $assertoff/$asserton to control assertion evaluation