Assertions: Immediate and Concurrent Assertions (SVA Basics)

So far, checking whether a result is correct has meant hand-writing procedural code like if (...) $display(...);. Assertions offer a more direct way: declare "this condition should hold," and let the tool check it automatically, reporting when it doesn't. This chapter covers two kinds: immediate assertions, which check a condition at a single point in time, and concurrent assertions, which check temporal relationships spanning multiple clock cycles.

Immediate assertions: a built-in check statement

task automatic check_result(int actual, int expected);
  assert (actual == expected)
    else $error("mismatch: expected=%0d actual=%0d", expected, actual);
endtask

assert (condition) statement-if-true; else statement-if-false; — both the else branch and the "if true" statement are optional. An immediate assertion evaluates right when execution reaches that line (like an ordinary statement, completing in zero simulation time) — functionally the same as if (!(actual == expected)) $error(...);, but writing it as assert communicates "this is a checkpoint" more clearly. In a real tool flow, assertion failures are also tracked and reported separately, instead of getting buried in ordinary $display output.

Concurrent assertions: checking relationships across clock cycles

An immediate assertion can only check a condition "right now." Many verification scenarios need to check a temporal relationship instead — for example, "once a request signal goes high, an acknowledgment must arrive within a few cycles." That's exactly what concurrent assertions are for: they sample repeatedly on a clock, checking a pattern that spans multiple cycles:

property req_ack_p;
  @(posedge clk) req |-> ##[1:3] ack;
endproperty
 
assert property (req_ack_p)
  else $error("ack did not follow req within 3 cycles");

Breaking this down:

• @(posedge clk): this property is sampled and checked on every rising clock edge.
• req |-> ##[1:3] ack: |-> is the "implication" operator, meaning "if req is true this cycle, then..."; ##[1:3] means "within the next 1 to 3 clock cycles." Together: "whenever req is true, ack must become true within 1 to 3 cycles afterward" — a very typical check in protocol handshake scenarios.

sequence: extracting a reusable temporal pattern

If the same temporal pattern needs to be used across multiple propertys, sequence names and extracts it:

sequence ack_within_3_cycles;
  ##[1:3] ack;
endsequence
 
property req_ack_p;
  @(posedge clk) req |-> ack_within_3_cycles;
endproperty
 
assert property (req_ack_p)
  else $error("ack did not follow req within 3 cycles");

A sequence describes "a signal pattern spanning time"; a property builds on a sequence (or a plain boolean expression), adding structure like implication and clock sampling, turning it into a complete declaration that assert property (...) can check.

Immediate vs. concurrent: which do I use?

Assertions check — they don't fix anything

An assertion's only job is to notice a problem and report it — it never changes any behavior itself. This lines up with chapter 1's "design code vs. verification code" mental model: assertions belong to the verification half, continuously checking whether the design behaves as expected, without implementing any functionality themselves. Assertions answer "did something that shouldn't happen, happen" — a related but different question, "have the scenarios that should be tested actually been tested," has its own dedicated tool (covergroup) and its own systematic methodology, covered from scratch in the dv-methodology track rather than here.

Summary

• An immediate assertion assert (cond) else ...; checks a condition right now, in zero simulation time — a clearer alternative to if (!cond) $error(...); that tools can track separately.
• A concurrent assertion is built on property, sampled on a clock via @(posedge clk), and can express relationships spanning multiple cycles; |-> means implication, and ##[m:n] means "within the next m to n cycles."
• sequence extracts a reusable temporal pattern that multiple propertys can reference.
• Assertions only check — they don't fix anything — and are part of verification code, not design code.
• Assertions answer "did something go wrong"; a separate tool, covergroup, answers "was testing thorough enough" — full treatment, syntax included, is in the dv-methodology track.