Assertions are executable specifications — they describe what your design must do and fire an error the moment it doesn't. SVA gives you two flavors: immediate assertions for point-in-time checks and concurrent assertions for multi-cycle temporal properties, both essential for protocol verification.
An immediate assertion evaluates a boolean expression at the current simulation time. It lives inside procedural blocks — initial, always, tasks, or functions. Think of it as an if statement that fires $error or $fatal when the condition fails:
// Basic immediate assertion — checks a condition now always @(posedge clk) begin // Assert that grant is never asserted without a prior request chk_no_spurious_grant: assert (!grant || request) else $error("GRANT asserted without REQUEST at time %0t", $time); end // $fatal stops simulation immediately (severity 1) initial begin assert (DATA_WIDTH == 32 || DATA_WIDTH == 64) else $fatal(1, "Unsupported DATA_WIDTH=%0d", DATA_WIDTH); end // $warning — non-fatal, prints message and continues always @(valid) begin chk_valid_width: assert ($bits(valid) == 1) else $warning("valid should be 1 bit"); end
chk_no_spurious_grant:) makes the assertion name appear in simulator reports, making failures much easier to trace. Always name important assertions.A concurrent assertion is sampled at clock edges and checks a sequence of values across multiple cycles. It lives in module, interface, or generate scope (not inside procedural blocks). The sampled values come from the Observed simulation region — after the Active region settles:
// Concurrent assertion must be in module/interface scope // or in an always block with no event control // Simplest form: check a combinational expression every clock chk_onehot: assert property ( @(posedge clk) disable iff (!rstn) $onehot0(grant_vec) // at most one grant at a time ) else $error("Multiple grants asserted: %b", grant_vec); // The default clocking can be set once for all assertions: default clocking main_clk @(posedge clk); endclocking default disable iff (!rstn); // Now assertions omit @(posedge clk) and disable iff chk_simple: assert property ($onehot0(grant_vec)) else $error("Multiple grants");
Sequences describe patterns of signal values across time. The clock tick operator ##n means "advance n clock cycles". Combined with repetition operators, you can describe complex temporal patterns concisely:
// ## — exact delay // req high, then exactly 2 cycles later ack goes high sequence req_then_ack; req ##2 ack; endsequence // ##[1:3] — range delay: ack arrives 1 to 3 cycles after req sequence req_ack_range; req ##[1:3] ack; endsequence // [*3] — consecutive repetition exactly 3 times sequence three_valids; valid [*3]; // valid must be high for exactly 3 consecutive cycles endsequence // [+] — one or more consecutive occurrences // [*] — zero or more (use sparingly — can be slow in formal) sequence burst_data; start ##1 valid [+] ##1 done; endsequence // throughout — condition must hold for the entire duration // "while frame is active, valid must stay high" sequence valid_throughout_frame; (frame ##1 valid [+] ##1 !frame) and (valid throughout frame [+]); endsequence // within — first sequence must complete within second sequence sequence ack_within_grant; ack within (grant ##[0:$] !grant); endsequence
| Operator | Meaning | Example |
|---|---|---|
##n | Exactly n clock cycles later | a ##2 b |
##[m:n] | Between m and n cycles later | a ##[1:4] b |
[*n] | Exactly n consecutive cycles true | a[*3] |
[*m:n] | Between m and n consecutive cycles | a[*2:5] |
[+] | One or more consecutive cycles | valid[+] |
throughout | Condition holds during sequence | en throughout seq |
within | Seq1 completes inside Seq2 | s1 within s2 |
A property wraps a sequence (or sequence implication) and attaches clock and reset. The two implication operators differ by where the consequent starts:
// |-> overlapping implication // "If req is high THIS cycle, ack must also be high THIS cycle" property p_req_ack_overlap; @(posedge clk) req |-> ack; endproperty // |=> non-overlapping implication (== ##1 on consequent) // "If req is high this cycle, ack must be high the NEXT cycle" property p_req_ack_next; @(posedge clk) req |=> ack; endproperty // Combining sequence + implication // "If start goes high, done must follow within 4 cycles" property p_start_done; @(posedge clk) disable iff (!rstn) start |-> ##[1:4] done; endproperty // "not" negates a property property p_no_double_grant; @(posedge clk) not (grant_a && grant_b); endproperty // Parameterised property property p_valid_ack(logic vld, logic ack, int max_lat); @(posedge clk) disable iff (!rstn) vld |-> ##[0:max_lat] ack; endproperty
cover property for the antecedent to confirm it was exercised at least once.The same property can be used in three different statement types, each with a distinct role in simulation and formal verification:
// assert property — DUT MUST satisfy this // Simulation: $error on violation // Formal: tool proves (or finds counterexample) assert property (p_req_ack_next) else $error("req→ack latency violated"); // assume property — stimulus CONSTRAINT (formal only) // Formal: tool only considers inputs satisfying this // Simulation: treated as assert (can catch bad TB) assume property (@(posedge clk) req |-> ##[1:$] !req) // req must de-assert eventually // cover property — check REACHABILITY // "Was this scenario ever exercised?" cover property (@(posedge clk) req ##[1:4] ack); // If cover count == 0, the scenario was never hit
| Statement | In Simulation | In Formal Verification |
|---|---|---|
assert property | Error/fatal on violation | Proves property or finds CEX |
assume property | Acts like assert (checks TB) | Constrains input space |
cover property | Counts how often sequence fires | Proves sequence is reachable |
These built-in sampled value functions let you reference signal behavior relative to the clock edge without writing full sequences:
// $rose(sig) — true if sig changed 0→1 at this clock edge // $fell(sig) — true if sig changed 1→0 at this clock edge // $stable(sig) — true if sig did NOT change from last clock edge // $past(sig,n) — value of sig n clock cycles ago // "valid must not de-assert (fall) until ready has been seen" property p_valid_stable_until_ready; @(posedge clk) disable iff (!rstn) $rose(valid) |-> (valid throughout (##[0:$] ready)); endproperty // "If we saw a write 2 cycles ago, wdata must match recorded value" property p_data_stable; @(posedge clk) $past(wen, 2) |-> (rdata == $past(wdata, 2)); endproperty // $fell on reset should cause fsm to return to IDLE property p_reset_to_idle; @(posedge clk) $fell(rstn) |=> (state == IDLE); endproperty assert property (p_valid_stable_until_ready); assert property (p_reset_to_idle) else $error("FSM did not return to IDLE after reset");
The bind keyword instantiates a checker module inside a DUT without modifying the DUT's source. This is the standard way to attach SVA checkers to IP blocks, third-party cores, or any RTL you cannot edit:
// Step 1: write all assertions in a separate checker module module fifo_checker ( input logic clk, rstn, input logic wr_en, rd_en, input logic full, empty ); // Cannot write when full chk_no_write_full: assert property ( @(posedge clk) disable iff (!rstn) full |-> !wr_en ) else $error("Write to full FIFO!"); // Cannot read when empty chk_no_read_empty: assert property ( @(posedge clk) disable iff (!rstn) empty |-> !rd_en ) else $error("Read from empty FIFO!"); endmodule // Step 2: bind into DUT — no DUT source changes needed bind sync_fifo fifo_checker u_fifo_chk ( .clk (clk), .rstn (rst_n), .wr_en (wr_en), .rd_en (rd_en), .full (full), .empty (empty) ); // "sync_fifo" is the module name of the DUT // The checker sees all internal signals of sync_fifo
The AXI4 spec has a strict rule: once VALID is asserted, it must not be de-asserted until the corresponding READY is seen. This is a classic concurrent assertion — it fires the moment a design violates the protocol:
// AXI4 Section A3.2.1 — VALID stability rule // Once AWVALID is high, it cannot go low until AWREADY is seen property p_awvalid_stable; @(posedge clk) disable iff (!aresetn) ($rose(awvalid) || (awvalid && !awready)) |-> awvalid; endproperty // Same rule for WVALID and ARVALID property p_wvalid_stable; @(posedge clk) disable iff (!aresetn) ($rose(wvalid) || (wvalid && !wready)) |-> wvalid; endproperty property p_arvalid_stable; @(posedge clk) disable iff (!aresetn) ($rose(arvalid) || (arvalid && !arready)) |-> arvalid; endproperty // AXI4 also says: READY CAN de-assert any time (no constraint) // But VALID de-assert is only allowed after handshake completes // Bind the checker to the AXI master module axi4_protocol_checker ( input logic clk, aresetn, input logic awvalid, awready, input logic wvalid, wready, input logic arvalid, arready ); chk_awvalid: assert property (p_awvalid_stable) else $error("AXI4: AWVALID de-asserted before AWREADY"); chk_wvalid: assert property (p_wvalid_stable) else $error("AXI4: WVALID de-asserted before WREADY"); chk_arvalid: assert property (p_arvalid_stable) else $error("AXI4: ARVALID de-asserted before ARREADY"); // Cover: ensure handshakes actually happen during simulation cov_aw_handshake: cover property ( @(posedge clk) awvalid && awready ); endmodule bind my_axi_master axi4_protocol_checker u_axi_chk (.*); // .* connects matching port names automatically