The Four Layers of SVA

Why a layered model

SVA is not one language feature; it is a stack of four small languages , each consuming the one below. Booleans say what is true at an instant. Sequences arrange booleans across cycles . Properties attach obligation — what must follow from what, under which clock and reset. Directives tell the tool what to do with a property: check it, constrain with it, or count it. Keeping the layers straight tells you instantly why, say, |-> is legal in a property but not inside a sequence operand of ##, or why disable iff belongs to the property layer and not to a sequence.

THE FOUR LAYERS — each consumes the one below

  ┌────────────────────────────────────────────────────────────┐
  │ LAYER 4: VERIFICATION DIRECTIVE                            │
  │   assert property / assume property / cover property /     │
  │   restrict property — label + optional action block        │
  ├────────────────────────────────────────────────────────────┤
  │ LAYER 3: PROPERTY                                          │
  │   clock spec, disable iff, implication |-> |=>,            │
  │   not / and / or / if-else / until / eventually            │
  ├────────────────────────────────────────────────────────────┤
  │ LAYER 2: SEQUENCE                                          │
  │   ##N ##[a:b] delays, [*N] [=N] [->N] repetition,          │
  │   and / or / intersect / throughout / within               │
  ├────────────────────────────────────────────────────────────┤
  │ LAYER 1: BOOLEAN                                           │
  │   req && !busy, $rose(valid), state == IDLE,               │
  │   any expression over sampled values                       │
  └────────────────────────────────────────────────────────────┘

  Each operator belongs to EXACTLY ONE layer.
  "Is |-> legal here?" = "Am I at the property layer here?"

One assertion, fully dissected

// LAYER 1 — booleans (named for readability)
// req && !busy        "a request the DUT can accept"
// gnt                 "grant asserted"

// LAYER 2 — sequence: the temporal shape "grant within 1..4 cycles"
sequence s_gnt_window;
  ##[1:4] gnt;
endsequence

// LAYER 3 — property: clock + reset + obligation
property p_req_gets_gnt;
  @(posedge clk) disable iff (!rst_n)
  (req && !busy) |-> s_gnt_window;
endproperty

// LAYER 4 — directive: check it in simulation, with an action block
ap_req_gets_gnt: assert property (p_req_gets_gnt)
  else $error("request not granted within 4 cycles");

// LAYER 4 again — same property, different directive: count matches
cp_req_gets_gnt: cover property (p_req_gets_gnt);

The same property feeds two directives — one checks, one measures. That reuse is the point of naming: write the temporal behavior once, then decide separately what the tool should do with it. Note also the layering of responsibilities: the clock and disable iff live in the property , not the sequence — sequences describe shape, properties describe context and obligation.

EVALUATION OF p_req_gets_gnt — one passing attempt

  clk      : T0    T1    T2    T3    T4    T5
  req&!busy: 0     1     0     0     0     0
  gnt      : 0     0     0     1     0     0

  T1: antecedent true → s_gnt_window starts
        ##[1:4] gnt:
        T2 (##1): gnt=0 … thread alive
        T3 (##2): gnt=1 → sequence MATCHES → property holds ✓
  T0, T2..T5: antecedent false → attempts pass vacuously (see Implication topic)

Named sequences and properties with arguments

Sequences and properties take formal arguments, which turns one-off checks into a reusable library. Arguments can be signals, expressions, constants — even untyped, so the same sequence works for any compatible operand. This is how real codebases avoid forty copies of the same handshake property with different signal names.

// Reusable parameterized sequence: sig holds for N cycles
sequence s_held (sig, int unsigned n);
  sig [*n];
endsequence

// Reusable handshake property — works for ANY req/ack pair
property p_handshake (clk_e, rst, req_s, ack_s, int unsigned max_lat);
  @(clk_e) disable iff (rst)
  req_s |-> ##[1:max_lat] ack_s;
endproperty

// Instantiate across the design — one definition, many checks
ap_axi_aw : assert property (p_handshake(posedge clk, !rst_n, awvalid, awready, 16))
  else $error("AW channel handshake timeout");
ap_axi_w  : assert property (p_handshake(posedge clk, !rst_n, wvalid,  wready,  16))
  else $error("W channel handshake timeout");
ap_axi_b  : assert property (p_handshake(posedge clk, !rst_n, bvalid,  bready,  16))
  else $error("B channel handshake timeout");

Composition rules worth memorizing

• A sequence can instantiate other sequences — composition is how complex protocols stay readable.

• A property can instantiate sequences and other properties; a sequence can never contain property-layer operators (|->, disable iff, not).

• A boolean is a degenerate one-cycle sequence — anywhere a sequence is required, a boolean works.

• Clock can be inherited: a property without its own @(...) takes the clock from a default clocking block or from the context that uses it.

The four directives at a glance

assert property (p_no_overflow);   // CHECK:  error if it fails
assume property (p_legal_inputs);  // CONSTRAIN: formal treats as given;
                                   //   simulation checks it like assert
cover  property (p_back_to_back);  // MEASURE: count matches, no error
restrict property (p_mode_fixed);  // FORMAL-ONLY constraint; sim ignores

Directive semantics get a full sub-lesson later in this topic; for now, the layer-model takeaway is that all four consume the same property layer — write the behavior once, choose the verb separately.

Interview angle

"Walk me through the structure of a concurrent assertion" is a top-five SVA interview question, and the layered answer is the one interviewers want: boolean expressions, composed into sequences by temporal operators, wrapped in properties that add clock/reset/implication, consumed by a directive. Sketch the four-box diagram if there is a whiteboard.

• Trap question: "Can I write disable iff inside a sequence?" — No; it is a property-layer construct. Same for |->.

• Trap question: "What's the difference between a sequence and a property?" — a sequence describes a pattern that matches or not; a property adds obligation/context (implication, clock, reset) and is what directives consume.

• Strong-signal extra: mention that one named property can feed both assert and cover, and that arguments make sequences/properties a reusable library — interviewers read this as real-project experience.

Key takeaways

• Four layers: boolean → sequence → property → directive; every operator belongs to exactly one.

• Sequences describe temporal shape; properties add clock, reset, and obligation; directives pick the tool action.

• Name and parameterize sequences/properties — one handshake property can check every channel in the design.

• A boolean is a one-cycle sequence; sequences nest into sequences and properties, never the reverse.

Common pitfalls

• Trying to use |-> or disable iff inside a sequence — property-layer operators, compile error.

• Copy-pasting near-identical assertions instead of parameterizing one property — maintenance burden and divergence bugs.

• Putting the clock in the sequence and reusing it under a different clock — keep clocks at the property (or default clocking) level for reuse.

• Forgetting that assert property needs a label for sane log triage — unlabeled failures are needles in regression haystacks.