Why a layered model

SVA 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 add obligation with a clock and reset, and directives tell the tool what to do.

The same property feeds every directive. The table below is the one-line version; the Directives and Severity lesson gives the full simulation-versus-formal semantics.

One assertion dissected

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29

module req_gnt_props (
  input logic clk,
  input logic rst_n,
  input logic req,
  input logic busy,
  input logic gnt
);
  // LAYER 1: booleans, named in comments for readability
  // req && !busy   "a request the DUT can accept"
  // gnt            "grant asserted"

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

  // LAYER 3: property, clock plus reset plus 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
  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);
endmodule

The same property feeds two directives: one checks, one measures. The clock and disable iff live in the property. disable iff must, because it is property-only. A clock could also be attached to the sequence, but keeping it in the property leaves the sequence a reusable shape.

Reusable libraries

Sequences and properties take arguments, which turns one-off checks into a library. One handshake property with formal signal and latency arguments can check every channel in the design.

The library below runs. Its first version had a reusable sequence s_held(sig, n) written as sig [*n], which Verilator 5.048 rejects (a formal used as a repetition count); a formal used as a delay bound, ##[1:max_lat], works. The checks count failures so the bench can plant one.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20

module handshake_lib (
  input logic clk,
  input logic rst_n,
  input logic awvalid, awready,
  input logic wvalid,  wready,
  input logic bvalid,  bready,
  output int  aw_fails, w_fails, b_fails
);
  // Reusable property: fixed clock and reset, signals and latency as arguments.
  property p_handshake(req_s, ack_s, int max_lat);
    @(posedge clk) disable iff (!rst_n)
    req_s |-> ##[1:max_lat] ack_s;
  endproperty

  // One definition, three checks with different budgets.
  ap_axi_aw: assert property (p_handshake(awvalid, awready, 2)) else aw_fails++;
  ap_axi_w:  assert property (p_handshake(wvalid,  wready,  4)) else w_fails++;
  ap_axi_b:  assert property (p_handshake(bvalid,  bready,  4)) else b_fails++;
  initial begin aw_fails = 0; w_fails = 0; b_fails = 0; end
endmodule

answered after 2 cycles: AW 0, W 0, B 0 failures
answered after 3 cycles: AW 1, W 0, B 0 failures
PASS: the 2-cycle AW instance caught the 3-cycle answer, and the 4-cycle W and B instances accepted both

Memorize the composition rules. A sequence instantiates other sequences, and a property instantiates sequences and other properties. Implication, not and disable iff are property-only, while and and or exist at both layers. A clock may be attached to a sequence or to a property. A boolean is a degenerate one-cycle sequence, so it fits anywhere a sequence is required.

The bench pulses all three channels together, answered after 2 cycles and then after 3. Only the AW instance, with a 2-cycle budget, may fail, and only on the second pulse.

Common mistakes

Related topics

• Protocol assertions

• Sequences