Video 1 of 4 · ~11 minutes
Dr. Mike Borowczak · Electrical & Computer Engineering · CECS · UCF
Every CPU verification team at every tier-1 company lives in assertions. Modern designs have more lines of assertion code than RTL. An Arm A-series CPU has tens of thousands of assertions monitoring every interface, every handshake, every invariant. Formal verification tools (Jasper, VC Formal, Questa) literally prove assertions hold for all inputs — catching bugs no testbench could reach. The “Design Verification” engineer role exists because of this.
Today you add assertions to your UART and FSM designs. Your testbench catches explicit output values; assertions catch invariant violations continuously. By end of Day 14.1 your UART has protocol-level checks that no amount of input variation can silently violate.
“I already write testbenches. They check my outputs. Assertions are just a different way to do the same thing.”
Testbench = “apply these inputs, check these outputs.” Narrow and specific. Assertion = “at all times, this invariant must hold.” Broad and continuous. Your testbench runs a finite sequence of test cases; assertions watch every cycle of every simulation and fail the moment the DUT violates the contract. They're complementary, not overlapping.
module counter_with_assertions (
input logic clk, rst, en,
output logic [7:0] count
);
always_ff @(posedge clk) begin
if (rst) count <= 0;
else if (en) count <= count + 1'b1;
end
// Immediate assertion — checked at the moment it's reached
always_ff @(posedge clk) begin
assert (count !== 8'hXX)
else $error("Counter went X-valued at time %0t", $time);
assert (count < 8'hFF || rst || !en)
else $warning("Counter about to wrap");
end
endmoduleif statement with teeth. “At this clock edge, count should not be X.” If it is, the simulator fires $error and typically halts. Lightweight. Lives inside RTL or TB. Classic uses: check for uninitialized state, check for bound violations.
property)// Concurrent assertion — a rule about sequences across cycles
// "When valid asserts, ready must arrive within 10 cycles."
property p_handshake;
@(posedge clk) disable iff (rst)
valid |-> ##[1:10] ready;
endproperty
a_handshake: assert property (p_handshake)
else $error("Handshake violation: valid at %0t without ready", $time);
// "tx_busy must go low exactly one cycle after tx_start"
property p_start_then_busy;
@(posedge clk) $rose(tx_start) |=> tx_busy;
endproperty
a_start_then_busy: assert property (p_start_then_busy);|-> (overlapping): “if LHS, then RHS must hold this cycle”|=> (non-overlapping): “if LHS, then RHS must hold next cycle”##N: exactly N cycles later; ##[1:10]: 1 to 10 cycles later$rose / $fell / $stable: signal edge / stability checksdisable iff (rst): don't check during resetYour Day 11 UART TX has signals i_valid, o_busy, and o_tx_line. Write a concurrent assertion: “Once the TX asserts busy, tx_line must stay low for exactly CLKS_PER_BIT cycles (the start bit).”
property p_start_bit_length;
@(posedge clk) disable iff (rst)
$rose(o_busy) |=> (!o_tx_line) [*CLKS_PER_BIT];
endproperty
a_start_bit: assert property (p_start_bit_length)
else $error("Start bit was not %0d cycles long", CLKS_PER_BIT);o_busy rises, the next CLKS_PER_BIT cycles must have o_tx_line == 0. If the TX breaks the start-bit timing (e.g., off-by-one in the counter), the assertion fires immediately. The bug is caught even if no testbench case happened to measure the start bit.
~6 minutes
▸ COMMANDS
cd labs/week4_day14/ex1_assertions/
# DUT with off-by-one bug injected
make sim # testbench alone might not notice
# now add assertions:
iverilog -g2012 -o sim tb.sv uart_tx.sv \\
uart_assertions.sv
./sim # assertion fires immediately▸ EXPECTED STDOUT
Without assertions:
Test PASSES (by luck)
With assertions:
** ASSERT FAIL **
a_start_bit at time 2172:
Start bit was not 217 cycles
long (was 216)
$error halt▸ THE INSIGHT
The off-by-one bug produced a 216-cycle start bit instead of 217. The testbench didn't measure bit-length and passed. The assertion caught it instantly with exact context (which cycle, which value). This is the case for assertions in one demo.
An assertion is a contract. A simulator checks it against the stimulus you provide. A formal tool goes further: it proves the assertion holds for every possible input sequence — or produces a counterexample.
| Tool | What it does | Cost |
|---|---|---|
| iverilog / Verilator + SVA | Checks assertions during simulation | Open source, free |
| Cadence Jasper / Synopsys VC Formal | Formally proves assertions over all inputs | Commercial, expensive |
| SymbiYosys / Yices | Open-source formal verification | Free, smaller scale |
Ask AI: “For my UART TX with CLKS_PER_BIT parameter, write 5 concurrent assertions that verify protocol correctness — start bit timing, data bit stability, stop bit, busy/valid handshake, and no back-to-back frames without a gap.”
TASK
AI writes a UART assertion suite.
BEFORE
Predict: 5 properties with |->, |=>, [*N], disable iff rst.
AFTER
Strong AI writes named properties + disable-iff. Weak AI writes only immediate assert() inside tb.
TAKEAWAY
AI is fluent in SVA. Excellent accelerator for verification engineers.
① Assertions are executable specifications. Testbenches check specific cases; assertions monitor invariants.
② Immediate (assert()) for single-cycle checks; concurrent (property ... assert property) for multi-cycle rules.
③ SVA operators: |-> same cycle, |=> next cycle, ##N N cycles, [*N] N repeats.
④ Same syntax powers formal verification. Assertion-writing is a career-long skill.
🔗 Transfer
Video 2 of 4 · ~11 minutes
▸ WHY THIS MATTERS NEXT
You've seen “Check the Machine” sidebars all semester — moments where AI assists specific tasks. Video 2 turns that into a workflow: how to use LLMs as a verification co-pilot for generating testbenches, assertions, and stimulus. The real skill isn't asking AI — it's knowing what to verify independently and what to trust.