SVA cheat sheet

Content coming soon. This page will contain Pedro's SVA reference material.

Sequences

// Basic sequence
sequence s_req_ack;
  req ##[1:4] ack;
endsequence

// Sequence with repetition
sequence s_burst;
  valid [*4];  // exactly 4 consecutive cycles
endsequence

// Sequence with goto repetition
sequence s_eventually_ack;
  req ##1 (!ack [*0:$] ##1 ack);
endsequence

Properties

// Implication (overlapping)
property p_req_implies_ack;
  @(posedge clk) disable iff (rst)
  req |-> ##[1:4] ack;
endproperty

// Implication (non-overlapping)
property p_req_then_ack;
  @(posedge clk) disable iff (rst)
  req |=> ##[0:3] ack;
endproperty

Assertion directives

// Assert — must hold
assert_req_ack: assert property (p_req_implies_ack);

// Cover — reachability
cover_req_ack: cover property (p_req_implies_ack);

// Assume — constrain inputs (formal)
assume_valid_req: assume property (
  @(posedge clk) $rose(req) |-> !req [*1:3]
);

Clocking blocks

// Default clocking (applies to all properties in scope)
default clocking cb @(posedge clk); endclocking
default disable iff (rst);

Auxiliary code patterns

Auxiliary variables keep assertions simple without polluting RTL.

// Track a value at the time of a request
logic [7:0] aux_req_data;
always_ff @(posedge clk)
  if (req) aux_req_data <= data_in;

// Use it in the property
property p_data_preserved;
  @(posedge clk)
  req |-> ##[1:4] (ack && data_out == aux_req_data);
endproperty