Assertions state what must hold. Immediate checks run with procedural code, clocked checks span cycles, and cover and assume complete the sign-off story.
Construct | Job | Where it runs |
|---|---|---|
| Flags a violation when the design breaks a rule | Simulation and formal |
| Records that a scenario was exercised | Simulation and formal |
| Promises environment behavior to constrain a proof | Formal (constraint); simulation checks it like an assertion on the stimulus |
4 lessons, about 23 min
Cover the exact antecedent to see whether the obligation was exercised. A stricter response-sequence cover can miss even when requests occurred. Simulation evidence, property proof and reachability are separate results.
The whole topic on one page, taken from each lesson's Remember box. Read it before an interview, or print it.
Immediate vs concurrent assertions
Immediate checks the values when execution reaches it; concurrent samples on the clock and reasons across cycles.
req |-> ##[1:3] gnt opens a window at the request and accepts a grant on any of the next three edges.
Use a deferred assertion in always_comb so only settled values are checked.
Rule of thumb: sample grants before updates, and observe registered violation flags after updates.
assert, cover, and assume roles
Assert states a design obligation. Cover shows a scenario is exercised or reachable. Assume constrains the environment.
An implication is vacuous where its antecedent never triggers; cover the antecedent to see it.
Keep assumes to input rules, such as cancel never riding with a request.
Rule of thumb: grant timing is an assert, where a violation is evidence; an assume would hide it.
Common RTL property templates
Handshake, mutex, reset exit and stability are the four templates; each row names what a violation means.
Check reset state at the first active edge, before that edge's nonblocking assignments.
##[1:3] excludes the request edge; use ##[0:3] if the interface allows same-edge service.
Rule of thumb: a service-window check shows an opportunity was met, not that starvation cannot happen.
SVA Cheat Sheet and Bug Hunt
|-> checks at the same edge, |=> at the next edge, ##[m:n] at the first match from m to n edges later.
A |=> failure is reported at the consequent edge; the antecedent held one edge earlier. Convert the printed time from the precision unit first.
Count the antecedent of every important property, and fail the test when the count is zero.
Rule of thumb: an assertion that never triggered has checked nothing; cover its antecedent.
Mini project: a reusable FIFO IP with package, interface, assertions and a formal check
Code lab: Immediate assert
Code lab: SVA cover wrapper
Practice question: AXI protocol checker with coverage and assertions
Practice question: Inline RTL checkers: X detection, handshake liveness and bindable monitors
Interview: run a mock interview on this topic
The finite simulation benches in this topic were executed with Icarus Verilog 13.0 (2026-10-16): each prints PASS. They use local 1ns/1ps time units, FAIL diagnostics with $fatal(1, ...), and $finish only after PASS. The course runner also recognizes FAIL text through its log parser; standalone simulator exit status needs failing termination explicitly.