The short answer: SystemVerilog assertions (SVA) check design behaviour while it simulates, and can be proven by formal tools. Immediate assertions check a condition at one point in procedural code. Concurrent assertions are clocked and describe behaviour over time with sequences (##n delays, [*n] repetition), implication (|-> same cycle, |=> next cycle) and functions like $rose, $fell, $stable and $past. Put protocol checks on interfaces and invariants inside the RTL, and always disable them during reset.
Assertions are the best value-for-effort verification tool I know. A one-line property placed next to the RTL catches a bug at the cycle it happens, instead of hundreds of cycles later in a scoreboard. And the same property can be proven by a formal tool.
This post replaces my older posts on SystemVerilog assertions, assertion-based formal verification and assertions in Verilog.
- What an assertion checks
- Immediate vs concurrent
- The operators you’ll use most
- Assertions I add to almost every design
- assert, assume and cover
- Assertions and formal verification
- Habits that keep assertions useful
Table of Contents
Part 1: What an assertion checks
property p_req_ack;
@(posedge clk) disable iff (!rst_n)
req |-> ##[1:3] ack;
endproperty
a_req_ack: assert property (p_req_ack)
else $error("req at %0t not acknowledged within 3 cycles", $time);Part 2: Immediate vs concurrent
// immediate: like an if, in procedural code
always_comb
a_onehot: assert ($onehot0(grant)) else $error("grant not one-hot");
// concurrent: clocked, can describe sequences over time
a_no_ovf: assert property (@(posedge clk) disable iff (!rst_n)
!(push && full));Part 3: The operators you’ll use most
| Operator | Meaning | Example |
|---|---|---|
| ##n | n clock cycles later | a ##2 b |
| ##[m:n] | between m and n cycles later | a ##[1:3] b |
| [*n] | repeat n times (consecutive) | busy [*4] |
| [->n] | n occurrences, not necessarily consecutive | ack [->2] |
| |-> | overlapping implication (same cycle) | req |-> gnt |
| |=> | non-overlapping implication (next cycle) | req |=> gnt |
| throughout | condition holds during a sequence | en throughout (a ##3 b) |
| $rose / $fell | 0→1 / 1→0 since the last clock | $rose(start) |=> busy |
| $stable / $past | unchanged / value n cycles ago | valid && !ready |=> $stable(data) |
Part 4: Assertions I add to almost every design
// valid/ready: hold valid and data until accepted
a_hold: assert property (@(posedge clk) disable iff (!rst_n)
valid && !ready |=> valid && $stable(data));
// FIFO: never push when full, never pop when empty
a_full: assert property (@(posedge clk) disable iff (!rst_n) !(push && full));
a_empty: assert property (@(posedge clk) disable iff (!rst_n) !(pop && empty));
// FSM: never reach an illegal state
a_state: assert property (@(posedge clk) disable iff (!rst_n)
state inside {IDLE, RUN, DONE});
// no X on key control signals after reset
a_known: assert property (@(posedge clk) disable iff (!rst_n) !$isunknown(valid));Part 5: assert, assume and cover
- assert: this must always be true; report a failure if not.
- assume: a constraint on the inputs. In simulation it behaves like an assertion; in formal it limits the inputs the tool explores.
- cover: report when this sequence happens. Cover properties show that interesting scenarios were actually exercised.
c_back_to_back: cover property (@(posedge clk) push ##1 push ##1 push);Part 6: Assertions and formal verification
Formal tools (like Jasper, VC Formal or Questa Formal) take the same properties and prove them for every possible input sequence, using assume properties to rule out illegal inputs. They’re excellent for arbiters, FIFOs, handshakes and control logic, and they return a short counter-example waveform when a property fails. Writing good assertions is the first step towards using formal.
Part 7: Habits that keep assertions useful
- Always use
disable iff (!rst_n)so assertions don’t fire during reset. - Name every assertion (
a_hold:) so failures are easy to find. - Put interface protocol checks in the interface, and invariants next to the RTL they protect.
- Bind assertion modules to a design with
bindwhen you can’t edit the RTL. - Write a cover for every important assertion, so you know it was actually triggered.
Practise this on VLSI Forge
I built VLSI Forge so you can write RTL in your browser, run it on a real simulator and check every signal in the waveform. Free, nothing to install.
Design Verification problems · SVA and constraints problems
Previous in my SystemVerilog series: Threads and inter-process communication. Next: Functional coverage.
FAQ
What is the difference between |-> and |=>?
|-> checks the consequent in the same cycle the antecedent matches; |=> checks it in the next cycle. a |=> b equals a |-> ##1 b.
What is the difference between immediate and concurrent assertions?
Immediate assertions check a condition at one point in procedural code. Concurrent assertions are clocked and check behaviour across cycles.
Are assertions synthesisable?
No, synthesis ignores them. Some emulation and FPGA prototyping flows can compile a subset into hardware checkers.
What is disable iff used for?
To turn an assertion off while a condition is true, usually reset, so it doesn’t report false failures.
