Assertion-Based Verification (SVA)

Assertion-based verification (ABV) embeds the specification directly in the design as checks that fire the instant a rule is broken. An assertion is a formal statement — “request must be followed by grant within 3 cycles” — that the simulator (or a formal tool) continuously enforces, pinpointing the exact cycle and signal when it fails.

Immediate vs concurrent

Immediate assertions are procedural checks (assert(cond)) inside a block — good for simple invariants. Concurrent assertions (property / assert property) describe behaviour over time using SystemVerilog Assertions (SVA): clocked sequences with the implication operator |-> and delay ##n. These are the workhorse of protocol checking and are also what a formal tool proves exhaustively. The SVA form (reference — run in the Verification/Formal Lab):

// "every req is granted within 1..3 cycles"
property p_req_grant;
  @(posedge clk) disable iff (!rst_n)
  req |-> ##[1:3] gnt;
endproperty
a_req_grant : assert property (p_req_grant)
              else $error("req not granted within 3 cycles");

// a simple immediate assertion
always @(posedge clk)
  if (state == BUSY) assert (!idle) else $error("idle high while BUSY");

Assertions shine because they are always on (every test benefits), they localise failures to the exact rule and cycle, and they double as coverage (cover property) and as the properties a formal engine proves. The runnable example checks a req→grant-within-3 rule in plain Verilog, failing loudly if the latency is violated:

module tb;
  reg clk=0, rst_n=0, req=0, gnt=0; integer waited=0, fails=0;
  always #5 clk=~clk;
  // model: grant arrives 2 cycles after req
  always @(posedge clk) if (req && !gnt) begin
    if (waited==2) gnt<=1; else waited<=waited+1;
  end
  // checker: req must be granted within 3 cycles
  integer since=0; reg watching=0;
  always @(posedge clk) begin
    if (req && !gnt) begin watching<=1; since<=since+1;
      if (since>3) begin fails=fails+1; $display("ASSERT FAIL: no grant in 3 cyc"); end
    end
    if (gnt) begin watching<=0; since<=0; end
  end
  initial begin
    #3 rst_n=1; @(posedge clk); req<=1;
    repeat(6) @(posedge clk);
    $display("req->grant assertion failures = %0d %s", fails, fails?"FAIL":"PASS (granted in <=3)");
    $finish;
  end
endmodule

req->grant assertion failures = 0 PASS (granted in <=3)

Check yourself

What does a concurrent assertion express that an immediate assertion cannot?

Behaviour over time. A concurrent assertion is clocked and uses sequences, the implication operator |-> and cycle delays ##n to state temporal rules like ‘req is followed by grant within 3 cycles’. Immediate assertions only check a condition at the instant they execute.

Give three reasons assertions are valuable beyond a one-off check.

They are always-on so every test benefits; they localise a failure to the exact rule, signal and cycle; and they serve double duty as functional coverage (cover property) and as the properties a formal tool proves exhaustively.

Have questions about this topic?
Share your question in comments or talk to our mentor team for batch guidance.

Need Fee, Duration, or Demo Class Details?

Talk to our admin team for the latest batch plan and career guidance.

Contact Admin Team

▶ Try it in the ChipXpert Lab

Compile and simulate this in the browser — no install. Edit the code and re-run instantly.

Open in Verification Lab

Learn Verilog with mentors, labs and placement support

This free series is maintained by the ChipXpert training team in Hyderabad & Bengaluru. Go deeper with instructor-led courses on real EDA tools.

Explore VLSI Courses