SV Day 17 — Assertions Basics (SVA)

Why Assertions?

Testbenches generate stimuli. But how do you verify the response is correct? You write assertions—temporal logic rules that must never be violated.

✅ Assertions execute in parallel with simulation
✅ Flag violations immediately
✅ Work in simulation AND formal verification
✅ Self-documenting: "What MUST happen"

Immediate vs Concurrent Assertions

Immediate assertions: Execute procedurally (like if statements).

always @(posedge clk) begin
  // Immediate: check synchronously
  assert(data != 8'hXX) $display("OK"); else $error("Data undefined!");

  // Another: read enable must not be high during reset
  assert(~(read_en && reset)) else $error("Protocol violation");
end

Concurrent assertions: Describe temporal properties (multi-cycle rules).

// If req goes high, ack must follow within 3 cycles
property req_ack_timing;
  @(posedge clk) req |-> ##[1:3] ack;
endproperty
assert property(req_ack_timing);

// Once busy, must stay busy until done
property busy_until_done;
  @(posedge clk) busy |-> busy until done;
endproperty
assert property(busy_until_done);

Basic Assertions (Immediate)

// 1. Simple combinational check
assert(~(read && write)) else $error("RW conflict");

// 2. Range check
assert(ptr inside {[0:255]}) else $error("Ptr out of range");

// 3. Conditional
assert((state == IDLE) || (counter > 0)) else $error("Invalid state");

// 4. With message
assert(valid_flag) else $error("Data valid flag not set at %0t", $time);

Sequences & Properties

For multi-cycle rules, use sequences and properties:

// Sequence: temporal pattern
sequence write_sequence;
  write_en && ~ack ##1 ~write_en;  // write, then not-write next cycle
endsequence

// Property: assertion of the sequence
property write_protocol;
  @(posedge clk) write_sequence |-> ##1 write_done;
endproperty

assert property(write_protocol) else $error("Write protocol failed");

// Operators:
// ##N  : N cycles delay
// |->  : implication (if ... then ...)
// |=> : overlapping implication (same cycle)
// ##[1:5] : 1 to 5 cycle range
// and, or, not : logical connectors
// until, s_until : until operator

Disable on Condition

Some assertions should be inactive during reset or certain modes:

// Disable during reset
property data_valid;
  @(posedge clk) disable iff (reset)
    valid_in |-> valid_out;
endproperty
assert property(data_valid);

// Disable during test mode
property protocol_rule;
  @(posedge clk) disable iff (test_mode)
    addr_valid && data_valid |-> ack within 1 cycle;
endproperty
assert property(protocol_rule);

Coverage of Assertions

Assertions pass silently. Add coverage to prove they were tested:

property req_ack;
  @(posedge clk) req |-> ##[1:3] ack;
endproperty

assert property(req_ack);
cover property(req_ack);  // Did we ever see this pattern?

// Check that req was held for different lengths
cover property(@(posedge clk) req ##1 ack);  // 1-cycle
cover property(@(posedge clk) req ##2 ack);  // 2-cycle
cover property(@(posedge clk) req ##3 ack);  // 3-cycle

Key Takeaways

✅ Immediate assertions: Synchronous checks
✅ Concurrent assertions: Temporal properties (sequences + properties)
✅ |-> = implication ("if this, then that")
✅ ##N = N-cycle delay
✅ disable iff (condition) = exceptions
✅ cover property = prove assertions are actually tested

Tomorrow (Day 18): Advanced SVA—complex sequences and assumptions.