Comprehensive Assertions Tutorial with Examples
Table of Contents
- Introduction to SVA
- Immediate Assertions
- Concurrent Assertions Basics
- Sequence Operators
- Property Declaration
- Implication Operators
- Repetition Operators
- Temporal Operators
- Local Variables
- Assertion Severity Levels
- Assertion System Tasks
- Advanced Assertions
- Protocol Assertions
- UVM Integration
- Best Practices
1. Introduction to SVA
What are SystemVerilog Assertions?
Assertions are declarative statements that specify design behavior. They continuously monitor signals and report violations.
Types of Assertions:
- Immediate Assertions: Execute like procedural statements
- Concurrent Assertions: Monitor signals over time
Why Use Assertions?
- Detect bugs early in simulation
- Document design intent
- Enable formal verification
- Provide better debug information
- Reusable across projects
Assertion vs Coverage:
- Assertions: Check correctness (what MUST happen)
- Coverage: Measure completeness (what DID happen)
2. Immediate Assertions
2.1 Basic Immediate Assertions
module immediate_assertions;
logic clk;
logic [7:0] data;
logic valid;
always @(posedge clk) begin
// Simple assertion
assert (data < 256);
// Assertion with message
assert (valid == 1)
else $error("Valid signal not asserted!");
// Assertion with severity levels
assert (data != 0)
else $fatal("Data is zero - critical error!");
// Assertion with pass/fail actions
assert (data inside {[10:20]})
$display("PASS: Data in range");
else
$error("FAIL: Data out of range, data=%0d", data);
end
endmodule
2.2 Immediate Assertion with if-else
module immediate_with_conditions;
logic clk, reset_n;
logic [7:0] counter;
always @(posedge clk) begin
if (!reset_n) begin
// Check counter resets to 0
assert (counter == 0)
else $error("Counter did not reset!");
end
else begin
// Check counter increments correctly
assert (counter == $past(counter) + 1)
else $error("Counter increment failed!");
end
end
endmodule
2.3 Assert, Assume, Cover
module assertion_types;
logic req, ack, gnt;
always_comb begin
// ASSERT: Check design correctness
assert (req || !ack)
else $error("Ack without request!");
// ASSUME: Constrain inputs (for formal verification)
assume (gnt -> req)
else $error("Grant without request!");
// COVER: Check if condition occurs (for coverage)
cover (req && ack && gnt)
$display("All signals high simultaneously");
end
endmodule
3. Concurrent Assertions Basics
3.1 Simple Concurrent Assertions
module concurrent_basic;
logic clk, reset_n;
logic req, gnt;
logic valid, ready;
// Basic concurrent assertion
property req_followed_by_gnt;
@(posedge clk) req |=> gnt;
// |=> means "on next clock cycle"
endproperty
assert property (req_followed_by_gnt)
else $error("Request not followed by grant!");
// Handshake protocol assertion
property valid_ready_handshake;
@(posedge clk) valid |-> ready;
// |-> means "on same clock cycle"
endproperty
assert property (valid_ready_handshake)
else $error("Valid without ready!");
// Reset assertion
property reset_behavior;
@(posedge clk) !reset_n |=> (req == 0) && (gnt == 0);
endproperty
assert property (reset_behavior)
else $error("Signals not cleared on reset!");
endmodule
3.2 Assertion with Disable iff
module assertion_disable_iff;
logic clk, reset_n;
logic req, ack;
// Disable assertion during reset
property req_ack_protocol;
@(posedge clk) disable iff (!reset_n)
req |=> ack;
endproperty
assert property (req_ack_protocol)
else $error("Request not acknowledged!");
// Multiple conditions in disable iff
property data_valid;
@(posedge clk) disable iff (!reset_n || test_mode)
valid |-> (data != 0);
endproperty
assert property (data_valid);
endmodule
4. Sequence Operators
4.1 Delay Operators
module sequence_delays;
logic clk;
logic req, gnt, done;
// ##N - Delay by N clock cycles
property fixed_delay;
@(posedge clk) req |-> ##3 gnt;
// Grant must come exactly 3 cycles after request
endproperty
assert property (fixed_delay)
else $error("Grant did not arrive in 3 cycles!");
// ##[m:n] - Delay range
property range_delay;
@(posedge clk) req |-> ##[1:5] gnt;
// Grant must come between 1 and 5 cycles after request
endproperty
assert property (range_delay)
else $error("Grant did not arrive within 1-5 cycles!");
// ##[1:$] - Delay 1 or more cycles (eventually)
property eventual_response;
@(posedge clk) req |-> ##[1:$] done;
// Done must eventually happen (within simulation)
endproperty
assert property (eventual_response)
else $error("Done never occurred!");
endmodule
4.2 Sequence AND/OR
module sequence_and_or;
logic clk;
logic a, b, c, d;
// Sequence AND (both must occur)
property seq_and;
@(posedge clk) a ##1 b and c ##1 d;
// Both sequences must match:
// Seq1: a followed by b
// Seq2: c followed by d
endproperty
assert property (seq_and);
// Sequence OR (either can occur)
property seq_or;
@(posedge clk) (a ##1 b) or (c ##1 d);
// Either sequence can match
endproperty
assert property (seq_or);
// Intersection (both sequences with same timing)
property seq_intersect;
@(posedge clk) (a ##2 b) intersect (c ##2 d);
// a and c at T0, b and d at T2
endproperty
assert property (seq_intersect);
endmodule
4.3 Sequence Throughout
module sequence_throughout;
logic clk;
logic busy, transfer, valid;
// Signal must stay high throughout sequence
property busy_during_transfer;
@(posedge clk)
busy throughout (transfer ##[1:10] valid);
// busy must be high from transfer until valid
endproperty
assert property (busy_during_transfer)
else $error("Busy dropped during transfer!");
// Example: Reset must stay low during initialization
property reset_during_init;
@(posedge clk)
!reset_n throughout (init_start ##[1:100] init_done);
endproperty
assert property (reset_during_init);
endmodule
5. Property Declaration
5.1 Named Properties
module named_properties;
logic clk, reset_n;
logic req, gnt, done;
// Define reusable properties
property request_grant;
@(posedge clk) disable iff (!reset_n)
req |=> gnt;
endproperty
property grant_done;
@(posedge clk) disable iff (!reset_n)
gnt |-> ##[1:10] done;
endproperty
property full_transaction;
@(posedge clk) disable iff (!reset_n)
req |=> gnt ##[1:10] done;
endproperty
// Use properties in assertions
assert property (request_grant)
else $error("Request not granted!");
assert property (grant_done)
else $error("Grant not completed!");
assert property (full_transaction)
else $error("Full transaction failed!");
// Cover property (for coverage)
cover property (full_transaction)
$display("Full transaction completed at %0t", $time);
endmodule
5.2 Parameterized Properties
module parameterized_properties;
logic clk;
logic req, ack;
logic [7:0] data;
// Property with parameters
property delayed_response(signal, response, int delay);
@(posedge clk) signal |-> ##delay response;
endproperty
// Use with different delays
assert property (delayed_response(req, ack, 1))
else $error("Ack not in 1 cycle!");
assert property (delayed_response(req, ack, 3))
else $error("Ack not in 3 cycles!");
// Property with range parameter
property value_in_range(val, int min_val, int max_val);
@(posedge clk) (val >= min_val) && (val <= max_val);
endproperty
assert property (value_in_range(data, 0, 255))
else $error("Data out of range!");
endmodule
6. Implication Operators
6.1 Overlapping Implication (|->)
module overlapping_implication;
logic clk;
logic valid, ready, accept;
// |-> : Overlapping implication (same cycle)
property same_cycle_check;
@(posedge clk) valid |-> ready;
// If valid is high, ready must be high in SAME cycle
endproperty
assert property (same_cycle_check)
else $error("Ready not asserted with valid!");
// Multiple conditions
property handshake;
@(posedge clk) (valid && ready) |-> accept;
// If both valid and ready, then accept must be high
endproperty
assert property (handshake);
endmodule
6.2 Non-Overlapping Implication (|=>)
module non_overlapping_implication;
logic clk;
logic req, gnt, ack;
// |=> : Non-overlapping implication (next cycle)
property next_cycle_check;
@(posedge clk) req |=> gnt;
// If req is high, gnt must be high in NEXT cycle
endproperty
assert property (next_cycle_check)
else $error("Grant not in next cycle!");
// Chain of implications
property request_grant_ack;
@(posedge clk) req |=> gnt |=> ack;
// T0: req
// T1: gnt (must be high)
// T2: ack (must be high)
endproperty
assert property (request_grant_ack)
else $error("Request-Grant-Ack chain broken!");
endmodule
6.3 Implication with Sequences
module implication_sequences;
logic clk;
logic start, busy, done;
logic [7:0] count;
// Overlapping: antecedent and consequent in same cycle
property start_implies_busy;
@(posedge clk) start |-> busy;
endproperty
assert property (start_implies_busy);
// Non-overlapping: consequent starts next cycle
property start_then_busy;
@(posedge clk) start |=> busy;
endproperty
assert property (start_then_busy);
// Complex consequent
property start_sequence;
@(posedge clk)
start |=> busy ##[1:10] done;
// After start, busy must come next cycle,
// then done within 1-10 cycles
endproperty
assert property (start_sequence);
endmodule
7. Repetition Operators
7.1 Consecutive Repetition [*n]
module consecutive_repetition;
logic clk;
logic busy, ready;
// [*n] - Exactly n consecutive times
property busy_3_cycles;
@(posedge clk) busy[*3];
// busy must be high for exactly 3 consecutive cycles
endproperty
assert property (busy_3_cycles);
// [*m:n] - Between m and n consecutive times
property busy_range;
@(posedge clk) busy[*2:5];
// busy high for 2 to 5 consecutive cycles
endproperty
assert property (busy_range);
// [*] - Zero or more times
property optional_busy;
@(posedge clk) busy[*] ##1 ready;
// busy for 0+ cycles, then ready
endproperty
assert property (optional_busy);
// [+] - One or more times
property at_least_one_busy;
@(posedge clk) busy[+] ##1 ready;
// busy for 1+ cycles, then ready
endproperty
assert property (at_least_one_busy);
endmodule
7.2 Goto Repetition [->n]
module goto_repetition;
logic clk;
logic req, ack;
// [->n] - Non-consecutive repetition (goto)
property req_ack_3times;
@(posedge clk) req[->3] |=> ack;
// req occurs 3 times (not necessarily consecutive),
// then ack must follow
endproperty
assert property (req_ack_3times)
else $error("Ack not after 3 requests!");
// Example timeline:
// T0: req=1 (1st occurrence)
// T1: req=0
// T2: req=1 (2nd occurrence)
// T3: req=0
// T4: req=1 (3rd occurrence)
// T5: ack=1 (must be high)
// [->m:n] - Occurs m to n times
property req_range;
@(posedge clk) req[->2:4] |=> ack;
// req occurs 2 to 4 times, then ack
endproperty
assert property (req_range);
endmodule
7.3 Non-Consecutive Repetition [=n]
module non_consecutive_repetition;
logic clk;
logic event_sig, done;
// [=n] - Non-consecutive, ends when nth match occurs
property event_3_times;
@(posedge clk) event_sig[=3] |=> done;
// event_sig goes high 3 times (any pattern),
// done must be high on next cycle after 3rd occurrence
endproperty
assert property (event_3_times);
// Difference between [->] and [=]:
// [->3]: Match on cycle when 3rd occurrence happens
// [=3]: Match on cycle AFTER 3rd occurrence
// Example with range
property event_range;
@(posedge clk) event_sig[=2:5] ##1 done;
// event occurs 2-5 times, then done 1 cycle later
endproperty
assert property (event_range);
endmodule
8. Temporal Operators
8.1 Eventually Operator (s_eventually)
module eventually_operator;
logic clk;
logic start, done;
logic error;
// s_eventually - Must happen sometime in the future
property eventually_done;
@(posedge clk) start |-> s_eventually done;
// After start, done must eventually become high
endproperty
assert property (eventually_done)
else $error("Done never occurred!");
// With time limit
property bounded_eventually;
@(posedge clk) start |-> ##[1:100] done;
// Done must occur within 100 cycles
endproperty
assert property (bounded_eventually);
endmodule
8.2 Always and Until Operators
module always_until_operators;
logic clk, reset_n;
logic busy, idle;
logic start, stop;
// s_until - First holds until second occurs
property busy_until_stop;
@(posedge clk) disable iff (!reset_n)
start |-> busy s_until stop;
// busy must stay high from start until stop
endproperty
assert property (busy_until_stop)
else $error("Busy dropped before stop!");
// s_until_with - First holds until and including when second occurs
property busy_until_with_stop;
@(posedge clk)
start |-> busy s_until_with stop;
// busy high from start through stop
endproperty
assert property (busy_until_with_stop);
endmodule
8.3 Next-Time Operators
module nexttime_operators;
logic clk;
logic enable, ready, valid;
// nexttime - Must be true next cycle
property next_ready;
@(posedge clk) enable |-> nexttime ready;
// If enable now, ready must be true next cycle
endproperty
assert property (next_ready);
// nexttime[n] - Must be true in nth cycle
property ready_in_3;
@(posedge clk) enable |-> nexttime[3] ready;
// ready must be high exactly 3 cycles after enable
endproperty
assert property (ready_in_3);
// s_nexttime - Strong version (checks up to end of simulation)
property strong_next;
@(posedge clk) enable |-> s_nexttime valid;
endproperty
assert property (strong_next);
endmodule
9. Local Variables
9.1 Local Variables in Assertions
module local_variables;
logic clk;
logic start, done;
logic [7:0] addr_in, addr_out;
logic [31:0] data_in, data_out;
// Capture value at start and check at end
property address_preserved;
logic [7:0] captured_addr;
@(posedge clk)
(start, captured_addr = addr_in) |->
##[1:10] (done && (addr_out == captured_addr));
// Capture addr_in when start, verify addr_out matches when done
endproperty
assert property (address_preserved)
else $error("Address not preserved!");
// Multiple local variables
property data_integrity;
logic [31:0] expected_data;
logic [7:0] expected_addr;
@(posedge clk)
(start, expected_data = data_in, expected_addr = addr_in) |=>
##[1:$] (done &&
(data_out == expected_data) &&
(addr_out == expected_addr));
endproperty
assert property (data_integrity);
endmodule
9.2 Local Variables with Sequences
module local_vars_sequences;
logic clk;
logic wr_en, rd_en;
logic [7:0] wr_addr, rd_addr;
logic [31:0] wr_data, rd_data;
// Write-Read coherency check
property write_read_coherency;
int addr;
int data;
@(posedge clk)
(wr_en, addr = wr_addr, data = wr_data) ##[1:$]
(rd_en && (rd_addr == addr)) |-> (rd_data == data);
// If write to addr with data, later read from same addr
// must return same data
endproperty
assert property (write_read_coherency)
else $error("Read data mismatch!");
// FIFO depth tracking
property fifo_depth_check;
int depth = 0;
@(posedge clk)
(wr_en && !rd_en, depth = depth + 1) or
(!wr_en && rd_en, depth = depth - 1) or
(wr_en && rd_en, depth = depth) |->
(depth >= 0) && (depth <= 16);
// Track FIFO depth, must stay in bounds
endproperty
assert property (fifo_depth_check)
else $error("FIFO depth violation!");
endmodule
10. Assertion Severity Levels
10.1 Severity System Tasks
module assertion_severity;
logic clk;
logic [7:0] data;
logic critical, warning_sig, info_sig;
// $fatal - Terminates simulation
property critical_error;
@(posedge clk) !critical;
endproperty
assert property (critical_error)
else $fatal(1, "CRITICAL: Fatal error occurred at %0t", $time);
// $fatal(0) - No diagnostic, $fatal(1) - Full diagnostic
// $error - Report error, continue simulation
property data_range;
@(posedge clk) data inside {[0:200]};
endproperty
assert property (data_range)
else $error("ERROR: Data=%0d out of range [0:200]", data);
// $warning - Report warning
property recommended_range;
@(posedge clk) data inside {[10:100]};
endproperty
assert property (recommended_range)
else $warning("WARNING: Data=%0d outside recommended range", data);
// $info - Informational message
property info_check;
@(posedge clk) info_sig |-> data != 0;
endproperty
assert property (info_check)
else $info("INFO: Data is zero when info_sig active");
endmodule
10.2 Custom Severity Actions
module custom_severity;
logic clk;
logic req, ack;
int error_count = 0;
property req_ack;
@(posedge clk) req |=> ack;
endproperty
assert property (req_ack)
else begin
error_count++;
if (error_count < 10) begin
$warning("Ack missing (count=%0d)", error_count);
end
else if (error_count < 100) begin
$error("Too many ack misses (count=%0d)", error_count);
end
else begin
$fatal("ABORT: Error count exceeded limit!");
end
end
endmodule
11. Assertion System Tasks
11.1 Assertion Control
module assertion_control;
logic clk;
logic req, gnt;
property req_gnt;
@(posedge clk) req |=> gnt;
endproperty
a_req_gnt: assert property (req_gnt)
else $error("Grant missing!");
initial begin
// Disable assertion
$assertoff(0, a_req_gnt);
// Run some initialization
#100ns;
// Enable assertion
$asserton(0, a_req_gnt);
// Normal operation
#1000ns;
// Disable all assertions in module
$assertoff;
// Kill all active assertions
$assertkill;
end
endmodule
11.2 Assertion Pass/Fail Actions
module assertion_actions;
logic clk;
logic valid, ready;
int pass_count = 0;
int fail_count = 0;
property handshake;
@(posedge clk) valid |-> ready;
endproperty
assert property (handshake)
begin
// Pass action
pass_count++;
if (pass_count % 100 == 0)
$display("Handshake passed %0d times", pass_count);
end
else
begin
// Fail action
fail_count++;
$error("Handshake failed (total failures=%0d)", fail_count);
// Detailed debug info
$display(" valid=%b, ready=%b at time %0t", valid, ready, $time);
end
endmodule
12. Advanced Assertions
12.1 First_match Operator
module first_match_example;
logic clk;
logic req, ack;
// Without first_match - all possible matches checked
property multi_match;
@(posedge clk) req[->3] |=> ack;
// Checks all ways req can occur 3 times
endproperty
// With first_match - only first occurrence checked
property single_match;
@(posedge clk) first_match(req[->3]) |=> ack;
// Checks only the first way req occurs 3 times
endproperty
assert property (first_match);
endmodule
12.2 Ended and Matched Functions
module ended_matched;
logic clk;
logic start, stop, check;
sequence start_stop_seq;
start ##[1:10] stop;
endsequence
// Check if sequence ended
property check_after_sequence;
@(posedge clk)
start_stop_seq.ended |-> check;
// When start_stop_seq completes, check must be high
endproperty
assert property (check_after_sequence);
// Check if sequence matched
property verify_match;
@(posedge clk)
start_stop_seq.matched |-> check;
endproperty
assert property (verify_match);
endmodule
12.3 Recursive Properties
module recursive_properties;
logic clk;
logic req, gnt;
// Recursive property example
property req_eventually_gnt;
@(posedge clk)
req |-> (gnt or (##1 req_eventually_gnt));
// If req, then either gnt now OR req persists and check again
endproperty
assert property (req_eventually_gnt)
else $error("Grant never came!");
endmodule
12.4 Multi-Clock Assertions
module multi_clock_assertions;
logic clk_a, clk_b;
logic sig_a, sig_b;
// Assertion on clock A
property check_on_clk_a;
@(posedge clk_a) sig_a |=> sig_a;
endproperty
assert property (check_on_clk_a);
// Assertion on clock B
property check_on_clk_b;
@(posedge clk_b) sig_b |=> sig_b;
endproperty
assert property (check_on_clk_b);
// Clock domain crossing check (advanced)
property cdc_check;
@(posedge clk_a)
sig_a |-> ##[1:5] @(posedge clk_b) sig_b;
// sig_a on clk_a, then sig_b on clk_b within 5 clk_a cycles
endproperty
assert property (cdc_check)
else $error("CDC transfer failed!");
endmodule
13. Protocol Assertions
13.1 APB Protocol Assertions
module apb_protocol_assertions(
input logic pclk,
input logic preset_n,
input logic psel,
input logic penable,
input logic pready,
input logic pwrite,
input logic [31:0] paddr,
input logic [31:0] pwdata
);
//==========================================================================
// APB Protocol Assertions
//==========================================================================
// Rule 1: PSEL and PENABLE cannot be high without prior setup
property apb_setup_access;
@(posedge pclk) disable iff (!preset_n)
(psel && !penable) |=> (psel && penable);
// Setup phase (psel=1, penable=0) must be followed by
// Access phase (psel=1, penable=1)
endproperty
a_apb_setup_access: assert property (apb_setup_access)
else $error("APB: Setup not followed by access!");
// Rule 2: PENABLE can only be high if PSEL is high
property apb_penable_needs_psel;
@(posedge pclk) disable iff (!preset_n)
penable |-> psel;
endproperty
a_apb_penable_needs_psel: assert property (apb_penable_needs_psel)
else $error("APB: PENABLE without PSEL!");
// Rule 3: Address and control stable during access
property apb_stable_during_access;
logic [31:0] addr;
logic wr;
@(posedge pclk) disable iff (!preset_n)
(psel && !penable, addr = paddr, wr = pwrite) |=>
(psel && penable) |-> ((paddr == addr) && (pwrite == wr));
endproperty
a_apb_stable: assert property (apb_stable_during_access)
else $error("APB: Address/control changed during access!");
// Rule 4: Write data stable during transfer
property apb_wdata_stable;
logic [31:0] data;
@(posedge pclk) disable iff (!preset_n)
(psel && !penable && pwrite, data = pwdata) |=>
(psel && penable && pwrite) |-> (pwdata == data);
endproperty
a_apb_wdata_stable: assert property (apb_wdata_stable)
else $error("APB: Write data changed during transfer!");
// Rule 5: PREADY eventually goes high
property apb_ready_eventually;
@(posedge pclk) disable iff (!preset_n)
(psel && penable) |-> ##[0:15] pready;
// PREADY must go high within 15 cycles
endproperty
a_apb_ready: assert property (apb_ready_eventually)
else $error("APB: PREADY timeout!");
// Rule 6: Transaction completes properly
property apb_transaction_complete;
@(posedge pclk) disable iff (!preset_n)
(psel && penable && pready) |=> !penable;
// After ready, penable must drop next cycle
endproperty
a_apb_complete: assert property (apb_transaction_complete)
else $error("APB: Transaction did not complete properly!");
//==========================================================================
// Coverage of APB States
//==========================================================================
covergroup apb_state_cg @(posedge pclk);
option.name = "apb_protocol_states";
state_cp: coverpoint {psel, penable} {
bins idle = {2'b00};
bins setup = {2'b10};
bins access = {2'b11};
illegal_bins invalid = {2'b01};
}
transitions_cp: coverpoint {psel, penable} {
bins idle_to_setup = (2'b00 => 2'b10);
bins setup_to_access = (2'b10 => 2'b11);
bins access_to_idle = (2'b11 => 2'b00);
bins access_to_setup = (2'b11 => 2'b10); // Back-to-back
}
endgroup
apb_state_cg apb_cg = new();
endmodule
13.2 AXI Protocol Assertions
module axi_protocol_assertions(
input logic aclk,
input logic aresetn,
input logic awvalid,
input logic awready,
input logic wvalid,
input logic wready,
input logic wlast,
input logic bvalid,
input logic bready
);
//==========================================================================
// AXI Write Channel Assertions
//==========================================================================
// Rule 1: Once AWVALID asserted, must stay high until AWREADY
property awvalid_until_awready;
@(posedge aclk) disable iff (!aresetn)
$rose(awvalid) |-> awvalid throughout ##[0:$] awready;
endproperty
a_awvalid_stable: assert property (awvalid_until_awready)
else $error("AXI: AWVALID dropped before AWREADY!");
// Rule 2: WLAST must be asserted for last data beat
property wlast_on_last_beat;
@(posedge aclk) disable iff (!aresetn)
(wvalid && wready && wlast) |=> !wvalid or $fell(wvalid);
endproperty
a_wlast_check: assert property (wlast_on_last_beat)
else $error("AXI: WLAST not on last beat!");
// Rule 3: BVALID follows write data completion
property bvalid_after_wlast;
@(posedge aclk) disable iff (!aresetn)
(wvalid && wready && wlast) |-> ##[1:15] bvalid;
endproperty
a_bvalid_timing: assert property (bvalid_after_wlast)
else $error("AXI: BVALID did not follow WLAST!");
// Rule 4: BVALID stays high until BREADY
property bvalid_until_bready;
@(posedge aclk) disable iff (!aresetn)
$rose(bvalid) |-> bvalid throughout ##[0:$] bready;
endproperty
a_bvalid_stable: assert property (bvalid_until_bready)
else $error("AXI: BVALID dropped before BREADY!");
//==========================================================================
// AXI Handshake Coverage
//==========================================================================
covergroup axi_handshake_cg @(posedge aclk);
aw_handshake_cp: coverpoint {awvalid, awready} {
bins no_transfer = {2'b00};
bins valid_wait = {2'b10};
bins transfer = {2'b11};
bins ready_wait = {2'b01}; // Should be rare
}
w_handshake_cp: coverpoint {wvalid, wready} {
bins no_transfer = {2'b00};
bins valid_wait = {2'b10};
bins transfer = {2'b11};
}
b_handshake_cp: coverpoint {bvalid, bready} {
bins no_transfer = {2'b00};
bins valid_wait = {2'b10};
bins transfer = {2'b11};
}
endgroup
axi_handshake_cg axi_cg = new();
endmodule
13.3 FIFO Protocol Assertions
module fifo_assertions #(
parameter DEPTH = 16
)(
input logic clk,
input logic reset_n,
input logic wr_en,
input logic rd_en,
input logic full,
input logic empty,
input logic [3:0] count
);
//==========================================================================
// FIFO Functional Assertions
//==========================================================================
// Rule 1: Cannot write when full
property no_write_when_full;
@(posedge clk) disable iff (!reset_n)
full |-> !wr_en;
endproperty
a_no_wr_full: assert property (no_write_when_full)
else $error("FIFO: Write attempted when full!");
// Rule 2: Cannot read when empty
property no_read_when_empty;
@(posedge clk) disable iff (!reset_n)
empty |-> !rd_en;
endproperty
a_no_rd_empty: assert property (no_read_when_empty)
else $error("FIFO: Read attempted when empty!");
// Rule 3: Count must be within bounds
property count_in_range;
@(posedge clk) disable iff (!reset_n)
count <= DEPTH;
endproperty
a_count_range: assert property (count_in_range)
else $error("FIFO: Count=%0d exceeds depth=%0d!", count, DEPTH);
// Rule 4: Full when count = DEPTH
property full_when_count_max;
@(posedge clk) disable iff (!reset_n)
(count == DEPTH) |-> full;
endproperty
a_full_flag: assert property (full_when_count_max)
else $error("FIFO: Count=DEPTH but not full!");
// Rule 5: Empty when count = 0
property empty_when_count_zero;
@(posedge clk) disable iff (!reset_n)
(count == 0) |-> empty;
endproperty
a_empty_flag: assert property (empty_when_count_zero)
else $error("FIFO: Count=0 but not empty!");
// Rule 6: Count increment on write only
property count_increment;
@(posedge clk) disable iff (!reset_n)
(wr_en && !rd_en && !full) |=>
(count == $past(count) + 1);
endproperty
a_count_inc: assert property (count_increment)
else $error("FIFO: Count did not increment on write!");
// Rule 7: Count decrement on read only
property count_decrement;
@(posedge clk) disable iff (!reset_n)
(!wr_en && rd_en && !empty) |=>
(count == $past(count) - 1);
endproperty
a_count_dec: assert property (count_decrement)
else $error("FIFO: Count did not decrement on read!");
// Rule 8: Count unchanged on simultaneous read/write
property count_stable_rd_wr;
@(posedge clk) disable iff (!reset_n)
(wr_en && rd_en && !full && !empty) |=>
(count == $past(count));
endproperty
a_count_stable: assert property (count_stable_rd_wr)
else $error("FIFO: Count changed on simultaneous rd/wr!");
//==========================================================================
// FIFO Coverage
//==========================================================================
covergroup fifo_cg @(posedge clk);
option.name = "fifo_functional_coverage";
count_cp: coverpoint count {
bins empty_fifo = {0};
bins partial[] = {[1:DEPTH-1]};
bins full_fifo = {DEPTH};
}
operations_cp: coverpoint {wr_en, rd_en} {
bins idle = {2'b00};
bins write_only = {2'b10};
bins read_only = {2'b01};
bins read_write = {2'b11};
}
// Cross: operations at different fill levels
ops_count_cross: cross count_cp, operations_cp {
ignore_bins no_wr_when_full =
binsof(count_cp.full_fifo) && binsof(operations_cp) intersect {2'b10, 2'b11};
ignore_bins no_rd_when_empty =
binsof(count_cp.empty_fifo) && binsof(operations_cp) intersect {2'b01, 2'b11};
}
endgroup
fifo_cg fifo_coverage = new();
endmodule
13.4 Arbiter Assertions
module arbiter_assertions #(
parameter NUM_MASTERS = 4
)(
input logic clk,
input logic reset_n,
input logic [NUM_MASTERS-1:0] request,
input logic [NUM_MASTERS-1:0] grant
);
//==========================================================================
// Arbiter Protocol Assertions
//==========================================================================
// Rule 1: Only one grant at a time (mutual exclusion)
property one_grant_at_a_time;
@(posedge clk) disable iff (!reset_n)
$onehot0(grant); // At most one bit high
endproperty
a_mutual_exclusion: assert property (one_grant_at_a_time)
else $error("ARB: Multiple grants active! grant=%b", grant);
// Rule 2: Grant only if request
property grant_needs_request;
@(posedge clk) disable iff (!reset_n)
|grant |-> |(grant & request);
// If any grant, corresponding request must be active
endproperty
a_grant_req: assert property (grant_needs_request)
else $error("ARB: Grant without request! req=%b, gnt=%b", request, grant);
// Rule 3: Request eventually gets grant (fairness)
property request_eventually_granted;
@(posedge clk) disable iff (!reset_n)
$rose(request[0]) |-> ##[1:20] grant[0];
// Request[0] must get grant within 20 cycles
endproperty
a_fairness: assert property (request_eventually_granted)
else $error("ARB: Request starved!");
// Rule 4: Grant persists while request active
property grant_persistence;
@(posedge clk) disable iff (!reset_n)
(grant[0] && request[0]) |=>
(grant[0] throughout request[0][->1]);
// Grant stays until request drops
endproperty
a_grant_persist: assert property (grant_persistence)
else $error("ARB: Grant dropped while request active!");
// Rule 5: No grant without any request
property no_spurious_grant;
@(posedge clk) disable iff (!reset_n)
(request == 0) |-> (grant == 0);
endproperty
a_no_spurious: assert property (no_spurious_grant)
else $error("ARB: Grant asserted with no requests!");
//==========================================================================
// Arbiter Coverage
//==========================================================================
covergroup arbiter_cg @(posedge clk);
option.name = "arbiter_coverage";
// Number of simultaneous requests
num_requests_cp: coverpoint $countones(request) {
bins no_req = {0};
bins one_req = {1};
bins two_req = {2};
bins three_req = {3};
bins all_req = {NUM_MASTERS};
}
// Which master got grant
grant_master_cp: coverpoint grant {
bins master[NUM_MASTERS] = {[0:NUM_MASTERS-1]} with ($countones(item) == 1);
}
// Cross: requests vs grants
req_gnt_cross: cross num_requests_cp, grant_master_cp;
endgroup
arbiter_cg arb_cg = new();
endmodule
14. UVM Integration
14.1 Assertions in UVM Interface
//=============================================================================
// APB Interface with Built-in Assertions
//=============================================================================
interface apb_if(input logic pclk);
logic preset_n;
logic [31:0] paddr;
logic psel;
logic penable;
logic pwrite;
logic [31:0] pwdata;
logic [31:0] prdata;
logic pready;
logic pslverr;
//===========================================================================
// APB Protocol Assertions
//===========================================================================
// Assertion 1: Setup to Access phase
property apb_setup_access;
@(posedge pclk) disable iff (!preset_n)
(psel && !penable) |=> (psel && penable);
endproperty
a_setup_access: assert property (apb_setup_access)
else $error("[APB_IF] Setup not followed by access!");
// Assertion 2: Stable address during transfer
property stable_addr;
logic [31:0] captured_addr;
@(posedge pclk) disable iff (!preset_n)
(psel && !penable, captured_addr = paddr) |=>
(psel && penable) |-> (paddr == captured_addr);
endproperty
a_stable_addr: assert property (stable_addr)
else $error("[APB_IF] Address changed during transfer!");
// Assertion 3: PREADY eventually
property pready_timeout;
@(posedge pclk) disable iff (!preset_n)
(psel && penable) |-> ##[0:15] pready;
endproperty
a_pready: assert property (pready_timeout)
else $error("[APB_IF] PREADY timeout!");
//===========================================================================
// Modport with Assertions
//===========================================================================
modport master (
input pclk, preset_n, prdata, pready, pslverr,
output paddr, psel, penable, pwrite, pwdata
);
modport slave (
input pclk, preset_n, paddr, psel, penable, pwrite, pwdata,
output prdata, pready, pslverr
);
modport monitor (
input pclk, preset_n, paddr, psel, penable, pwrite,
pwdata, prdata, pready, pslverr
);
endinterface
14.2 Assertion-Based Checker Component
class apb_assertion_checker extends uvm_component;
`uvm_component_utils(apb_assertion_checker)
virtual apb_if vif;
// Statistics
int assertion_pass_count = 0;
int assertion_fail_count = 0;
function new(string name, uvm_component parent);
super.new(name, parent);
endfunction
function void build_phase(uvm_phase phase);
super.build_phase(phase);
if (!uvm_config_db#(virtual apb_if)::get(this, "", "vif", vif))
`uvm_fatal("CHECKER", "Virtual interface not found!")
endfunction
//===========================================================================
// Concurrent Assertions in UVM Component
//===========================================================================
// NOTE: Concurrent assertions typically go in interface or module
// This shows conceptual integration with UVM
task run_phase(uvm_phase phase);
fork
// Monitor assertion violations
forever begin
@(posedge vif.pclk);
// Check protocol manually (or use bind)
if (vif.psel && vif.penable) begin
if (!vif.pready) begin
// Could assert here
end
end
end
join_none
endtask
function void report_phase(uvm_phase phase);
super.report_phase(phase);
`uvm_info("ASSERTION_REPORT",
$sformatf("\
" +
"╔════════════════════════════════════════╗\
" +
"║ Assertion Checker Report ║\
" +
"╠════════════════════════════════════════╣\
" +
"║ Assertions Passed : %0d ║\
" +
"║ Assertions Failed : %0d ║\
" +
"╚════════════════════════════════════════╝",
assertion_pass_count,
assertion_fail_count),
UVM_LOW)
endfunction
endclass
14.3 Bind Assertions to DUT
//=============================================================================
// DUT Module
//=============================================================================
module apb_slave(
input logic pclk,
input logic preset_n,
input logic [31:0] paddr,
input logic psel,
input logic penable,
input logic pwrite,
input logic [31:0] pwdata,
output logic [31:0] prdata,
output logic pready
);
// DUT logic here...
endmodule
//=============================================================================
// Assertion Module (separate)
//=============================================================================
module apb_slave_assertions(
input logic pclk,
input logic preset_n,
input logic [31:0] paddr,
input logic psel,
input logic penable,
input logic pwrite,
input logic [31:0] pwdata,
input logic [31:0] prdata,
input logic pready
);
// All APB assertions here
property apb_setup_access;
@(posedge pclk) disable iff (!preset_n)
(psel && !penable) |=> (psel && penable);
endproperty
a_setup: assert property (apb_setup_access)
else $error("APB protocol violation!");
// More assertions...
endmodule
//=============================================================================
// Bind statement (in testbench or separate file)
//=============================================================================
module testbench;
// Instantiate DUT
apb_slave dut (
.pclk(clk),
.preset_n(reset_n),
// ... other ports
);
// Bind assertions to DUT instance
bind apb_slave apb_slave_assertions apb_assertions_inst (
.pclk(pclk),
.preset_n(preset_n),
.paddr(paddr),
.psel(psel),
.penable(penable),
.pwrite(pwrite),
.pwdata(pwdata),
.prdata(prdata),
.pready(pready)
);
// Or bind to all instances of apb_slave
// bind apb_slave apb_slave_assertions apb_check (.*);
endmodule
15. Best Practices
15.1 Assertion Organization
//=============================================================================
// GOOD PRACTICE: Organized Assertion Module
//=============================================================================
module apb_protocol_checker(
apb_if.monitor vif
);
//===========================================================================
// CATEGORY 1: Basic Protocol Rules
//===========================================================================
// Setup followed by access
property p_setup_access;
@(posedge vif.pclk) disable iff (!vif.preset_n)
(vif.psel && !vif.penable) |=> (vif.psel && vif.penable);
endproperty
a_setup_access: assert property (p_setup_access)
else $error("[PROTOCOL] Setup-Access violation");
// PENABLE requires PSEL
property p_penable_needs_psel;
@(posedge vif.pclk) disable iff (!vif.preset_n)
vif.penable |-> vif.psel;
endproperty
a_penable_psel: assert property (p_penable_needs_psel)
else $error("[PROTOCOL] PENABLE without PSEL");
//===========================================================================
// CATEGORY 2: Signal Stability Rules
//===========================================================================
// Address stable during transfer
property p_addr_stable;
logic [31:0] addr;
@(posedge vif.pclk) disable iff (!vif.preset_n)
(vif.psel && !vif.penable, addr = vif.paddr) |=>
(vif.psel && vif.penable) |-> (vif.paddr == addr);
endproperty
a_addr_stable: assert property (p_addr_stable)
else $error("[STABILITY] Address changed during transfer");
// Write data stable
property p_wdata_stable;
logic [31:0] data;
@A) - Complete Guide (Part 1)
## Comprehensive Assertions Tutorial with Examples
---
## Table of Contents - Part 1
1. [Introduction to SVA](#1-introduction)
2. [Immediate Assertions](#2-immediate-assertions)
3. [Concurrent Assertions Basics](#3-concurrent-basics)
4. [Sequence Operators](#4-sequence-operators)
5. [Property Declaration](#5-property-declaration)
6. [Implication Operators](#6-implication)
7. [Repetition Operators](#7-repetition)
---
## 1. Introduction to SVA {#1-introduction}
**What are SystemVerilog Assertions?**
Assertions are declarative statements that specify design behavior. They continuously monitor signals and report violations.
**Types of Assertions:**
- **Immediate Assertions**: Execute like procedural statements (combinational)
- **Concurrent Assertions**: Monitor signals over time (temporal)
**Why Use Assertions?**
- Detect bugs early in simulation
- Document design intent
- Enable formal verification
- Provide better debug information
- Reusable across projects
**Assertion vs Coverage:**
- **Assertions**: Check correctness (what MUST happen)
- **Coverage**: Measure completeness (what DID happen)
---
## 2. Immediate Assertions {#2-immediate-assertions}
### 2.1 Basic Immediate Assertions
```systemverilog
module immediate_assertions;
logic clk;
logic [7:0] data;
logic valid;
always @(posedge clk) begin
// Simple assertion
assert (data < 256);
// Assertion with message
assert (valid == 1)
else $error("Valid signal not asserted!");
// Assertion with severity levels
assert (data != 0)
else $fatal("Data is zero - critical error!");
// Assertion with pass/fail actions
assert (data inside {[10:20]})
$display("PASS: Data in range");
else
$error("FAIL: Data out of range, data=%0d", data);
end
endmodule
2.2 Assert, Assume, Cover
module assertion_types;
logic req, ack, gnt;
always_comb begin
// ASSERT: Check design correctness
assert (req || !ack)
else $error("Ack without request!");
// ASSUME: Constrain inputs (for formal verification)
assume (gnt -> req)
else $error("Grant without request - input constraint!");
// COVER: Check if condition occurs (for coverage)
cover (req && ack && gnt)
$display("All signals high simultaneously at %0t", $time);
end
endmodule
2.3 Immediate Assertions in Procedures
module immediate_in_procedures;
logic clk, reset_n;
logic [7:0] counter;
logic [31:0] fifo_count;
parameter FIFO_DEPTH = 16;
always @(posedge clk or negedge reset_n) begin
if (!reset_n) begin
counter <= 0;
// Check reset behavior
assert (counter == 0)
else $error("Counter not zero on reset!");
end else begin
counter <= counter + 1;
// Check increment
assert (counter == $past(counter) + 1)
else $error("Counter increment failed!");
end
end
// Function with assertion
function bit is_fifo_valid(int count);
assert (count >= 0 && count <= FIFO_DEPTH)
else $error("FIFO count out of range: %0d", count);
return (count >= 0 && count <= FIFO_DEPTH);
endfunction
always @(posedge clk) begin
if (is_fifo_valid(fifo_count)) begin
// Process FIFO
end
end
endmodule
3. Concurrent Assertions Basics
3.1 Simple Concurrent Assertions
module concurrent_basic;
logic clk, reset_n;
logic req, gnt;
logic valid, ready;
// Basic concurrent assertion
property req_followed_by_gnt;
@(posedge clk) req |=> gnt;
// |=> means "on next clock cycle"
endproperty
assert property (req_followed_by_gnt)
else $error("Request not followed by grant!");
// Same cycle check
property valid_ready_handshake;
@(posedge clk) valid |-> ready;
// |-> means "on same clock cycle"
endproperty
assert property (valid_ready_handshake)
else $error("Valid without ready!");
// Reset assertion
property reset_behavior;
@(posedge clk) !reset_n |=> (req == 0) && (gnt == 0);
endproperty
assert property (reset_behavior)
else $error("Signals not cleared on reset!");
endmodule
3.2 Disable iff Clause
module disable_iff_example;
logic clk, reset_n, test_mode;
logic req, ack;
logic valid, data_valid;
// Disable assertion during reset
property req_ack_protocol;
@(posedge clk) disable iff (!reset_n)
req |=> ack;
endproperty
assert property (req_ack_protocol)
else $error("Request not acknowledged!");
// Multiple disable conditions
property data_check;
@(posedge clk) disable iff (!reset_n || test_mode)
valid |-> data_valid;
endproperty
assert property (data_check)
else $error("Invalid data!");
// Common pattern: disable during reset and test mode
property normal_operation;
@(posedge clk) disable iff (!reset_n || test_mode || scan_mode)
req |-> ##[1:5] ack;
endproperty
assert property (normal_operation);
endmodule
4. Sequence Operators
4.1 Delay Operators (##)
module sequence_delays;
logic clk;
logic req, gnt, done;
// ##N - Fixed delay by N cycles
property fixed_delay;
@(posedge clk) req |-> ##3 gnt;
// Grant must come exactly 3 cycles after request
endproperty
assert property (fixed_delay)
else $error("Grant not in 3 cycles!");
// ##[m:n] - Delay range
property range_delay;
@(posedge clk) req |-> ##[1:5] gnt;
// Grant must come between 1 and 5 cycles
endproperty
assert property (range_delay)
else $error("Grant not within 1-5 cycles!");
// ##[1:$] - Eventually (1 or more cycles)
property eventual_response;
@(posedge clk) req |-> ##[1:$] done;
// Done must eventually happen
endproperty
assert property (eventual_response)
else $error("Done never occurred!");
// ##[0:$] - Immediately or eventually
property immediate_or_later;
@(posedge clk) req |-> ##[0:$] done;
// Done can be same cycle or later
endproperty
assert property (immediate_or_later);
endmodule
4.2 Sequence Composition
module sequence_composition;
logic clk;
logic a, b, c, d, e;
// Define sequences
sequence seq_ab;
@(posedge clk) a ##1 b;
endsequence
sequence seq_cd;
@(posedge clk) c ##1 d;
endsequence
// Concatenate sequences
property seq_concat;
@(posedge clk) seq_ab ##2 seq_cd;
// a, then b (1 cycle), then 2 cycles, then c, then d
endproperty
assert property (seq_concat);
// Sequence AND (both must occur)
property seq_and;
@(posedge clk) seq_ab and seq_cd;
// Both sequences must complete
endproperty
assert property (seq_and);
// Sequence OR (either can occur)
property seq_or;
@(posedge clk) seq_ab or seq_cd;
// At least one sequence must complete
endproperty
assert property (seq_or);
// Sequence intersect (same endpoint)
property seq_intersect;
@(posedge clk) seq_ab intersect seq_cd;
// Both sequences end at same time
endproperty
assert property (seq_intersect);
endmodule
4.3 Throughout Operator
module throughout_example;
logic clk, reset_n;
logic busy, transfer, valid;
logic lock, process, unlock;
// Signal must stay high throughout sequence
property busy_during_transfer;
@(posedge clk) disable iff (!reset_n)
busy throughout (transfer ##[1:10] valid);
// busy must be high from transfer until valid
endproperty
assert property (busy_during_transfer)
else $error("Busy dropped during transfer!");
// Example: Lock held during processing
property lock_during_process;
@(posedge clk) disable iff (!reset_n)
lock throughout (process ##[1:100] unlock);
endproperty
assert property (lock_during_process)
else $error("Lock released prematurely!");
// Multiple conditions throughout
property multi_throughout;
@(posedge clk) disable iff (!reset_n)
(busy && lock) throughout (transfer ##[1:20] valid);
// Both busy AND lock must stay high
endproperty
assert property (multi_throughout);
endmodule
5. Property Declaration
5.1 Named Properties and Sequences
module named_properties;
logic clk, reset_n;
logic req, gnt, done, ack;
//===========================================================================
// Define Reusable Sequences
//===========================================================================
sequence req_gnt_seq;
@(posedge clk) req ##[1:3] gnt;
endsequence
sequence gnt_done_seq;
@(posedge clk) gnt ##[1:5] done;
endsequence
sequence done_ack_seq;
@(posedge clk) done ##1 ack;
endsequence
//===========================================================================
// Define Reusable Properties
//===========================================================================
property request_grant;
@(posedge clk) disable iff (!reset_n)
req |=> gnt;
endproperty
property grant_done;
@(posedge clk) disable iff (!reset_n)
gnt |-> ##[1:10] done;
endproperty
property full_transaction;
@(posedge clk) disable iff (!reset_n)
req_gnt_seq ##0 gnt_done_seq ##0 done_ack_seq;
endproperty
//===========================================================================
// Use Properties in Assertions
//===========================================================================
a_req_gnt: assert property (request_grant)
else $error("Request not granted!");
a_gnt_done: assert property (grant_done)
else $error("Grant not completed!");
a_full_txn: assert property (full_transaction)
else $error("Full transaction failed!");
//===========================================================================
// Use Properties for Coverage
//===========================================================================
c_full_txn: cover property (full_transaction)
$display("INFO: Full transaction completed at %0t", $time);
endmodule
5.2 Parameterized Properties
module parameterized_properties;
logic clk, reset_n;
logic req, ack;
logic [7:0] data;
logic valid;
//===========================================================================
// Property with Delay Parameter
//===========================================================================
property delayed_response(signal, response, int delay);
@(posedge clk) disable iff (!reset_n)
signal |-> ##delay response;
endproperty
// Use with different delays
a_ack_1: assert property (delayed_response(req, ack, 1))
else $error("Ack not in 1 cycle!");
a_ack_3: assert property (delayed_response(req, ack, 3))
else $error("Ack not in 3 cycles!");
//===========================================================================
// Property with Range Parameters
//===========================================================================
property value_in_range(logic[7:0] val, int min_val, int max_val);
@(posedge clk) disable iff (!reset_n)
(val >= min_val) && (val <= max_val);
endproperty
a_data_range: assert property (value_in_range(data, 0, 255))
else $error("Data out of range: %0d", data);
//===========================================================================
// Property with Signal Parameters
//===========================================================================
property handshake_protocol(logic v, logic r);
@(posedge clk) disable iff (!reset_n)
v |-> r;
endproperty
a_handshake: assert property (handshake_protocol(valid, ack))
else $error("Handshake failed!");
endmodule
6. Implication Operators
6.1 Overlapping Implication (|->)
module overlapping_implication;
logic clk, reset_n;
logic valid, ready, accept;
logic req, data_valid;
// |-> : Overlapping (same cycle check)
property same_cycle_check;
@(posedge clk) disable iff (!reset_n)
valid |-> ready;
// If valid is high, ready MUST be high in SAME cycle
endproperty
a_same_cycle: assert property (same_cycle_check)
else $error("Ready not asserted with valid!");
// Antecedent with multiple conditions
property multi_condition_antecedent;
@(posedge clk) disable iff (!reset_n)
(valid && ready) |-> accept;
// If BOTH valid and ready, then accept
endproperty
a_multi_cond: assert property (multi_condition_antecedent)
else $error("Accept not asserted!");
// Consequent with sequence
property antecedent_to_sequence;
@(posedge clk) disable iff (!reset_n)
req |-> data_valid ##1 ready ##1 accept;
// If req, then data_valid now, ready next, accept after
endproperty
a_ant_seq: assert property (antecedent_to_sequence)
else $error("Request sequence incomplete!");
endmodule
6.2 Non-Overlapping Implication (|=>)
module non_overlapping_implication;
logic clk, reset_n;
logic req, gnt, ack, done;
// |=> : Non-overlapping (next cycle check)
property next_cycle_check;
@(posedge clk) disable iff (!reset_n)
req |=> gnt;
// If req high at T, gnt MUST be high at T+1
endproperty
a_next_cycle: assert property (next_cycle_check)
else $error("Grant not in next cycle!");
// Chain of implications
property chain_of_events;
@(posedge clk) disable iff (!reset_n)
req |=> gnt |=> ack |=> done;
// T0: req
// T1: gnt must be high
// T2: ack must be high
// T3: done must be high
endproperty
a_chain: assert property (chain_of_events)
else $error("Event chain broken!");
// Implication with delay
property delayed_implication;
@(posedge clk) disable iff (!reset_n)
req |=> ##2 gnt;
// If req at T0, gnt must be high at T3 (1 + 2)
endproperty
a_delayed: assert property (delayed_implication)
else $error("Delayed grant failed!");
endmodule
6.3 Implication Comparison
module implication_comparison;
logic clk;
logic trigger, response;
// Overlapping |-> (same cycle)
property overlapping_ex;
@(posedge clk) trigger |-> response;
// T0: trigger=1 → response must be 1 at T0
endproperty
// Non-overlapping |=> (next cycle)
property non_overlapping_ex;
@(posedge clk) trigger |=> response;
// T0: trigger=1 → response must be 1 at T1
endproperty
// Timeline example:
// Cycle: T0 T1 T2
// trigger: 1 0 0
// response: 1 1 0
//
// overlapping_ex: PASS (response=1 at T0)
// non_overlapping_ex: PASS (response=1 at T1)
a_overlap: assert property (overlapping_ex);
a_non_overlap: assert property (non_overlapping_ex);
endmodule
7. Repetition Operators
7.1 Consecutive Repetition [*n]
module consecutive_repetition;
logic clk, reset_n;
logic busy, ready, valid;
// [*n] - Exactly n consecutive times
property busy_exactly_3;
@(posedge clk) disable iff (!reset_n)
busy[*3];
// busy=1 for exactly 3 consecutive cycles
endproperty
assert property (busy_exactly_3);
// [*m:n] - Between m and n consecutive times
property busy_range;
@(posedge clk) disable iff (!reset_n)
busy[*2:5];
// busy=1 for 2, 3, 4, or 5 consecutive cycles
endproperty
assert property (busy_range);
// [*] - Zero or more consecutive times
property optional_busy;
@(posedge clk) disable iff (!reset_n)
busy[*] ##1 ready;
// busy for 0+ cycles, then ready
// Matches: ready immediately, or busy then ready
endproperty
assert property (optional_busy);
// [+] - One or more consecutive times
property at_least_one_busy;
@(posedge clk) disable iff (!reset_n)
busy[+] ##1 ready;
// busy for 1+ cycles, then ready
endproperty
assert property (at_least_one_busy);
// Complex example
property complex_repetition;
@(posedge clk) disable iff (!reset_n)
valid ##1 busy[*3:7] ##1 ready;
// valid, then busy for 3-7 cycles, then ready
endproperty
assert property (complex_repetition);
endmodule
7.2 Goto Repetition [->n]
module goto_repetition;
logic clk, reset_n;
logic req, ack, done;
// [->n] - Non-consecutive repetition (goto)
property req_ack_3times;
@(posedge clk) disable iff (!reset_n)
req[->3] |=> ack;
// req goes high 3 times (not necessarily consecutive),
// then ack on next cycle after 3rd req
endproperty
assert property (req_ack_3times)
else $error("Ack not after 3 requests!");
// Timeline example:
// Cycle: T0 T1 T2 T3 T4 T5 T6
// req: 1 0 1 0 1 0 0
// ^1st ^2nd ^3rd
// ack: 0 0 0 0 0 1 0
// ^Must be high (T5 = T4+1)
// [->m:n] - Occurs m to n times (non-consecutive)
property req_range;
@(posedge clk) disable iff (!reset_n)
req[->2:4] |=> done;
// req occurs 2, 3, or 4 times, then done
endproperty
assert property (req_range);
// Practical example: Handshake retry
property retry_handshake;
@(posedge clk) disable iff (!reset_n)
req[->1:3] ##1 ack;
// Request retried 1-3 times, then acknowledged
endproperty
assert property (retry_handshake)
else $error("Handshake retry failed!");
endmodule
7.3 Non-Consecutive Repetition [=n]
module non_consecutive_repetition;
logic clk, reset_n;
logic event_sig, done;
logic pulse, response;
// [=n] - Non-consecutive, ends when nth match ends
property event_3_times;
@(posedge clk) disable iff (!reset_n)
event_sig[=3] ##1 done;
// event_sig goes high 3 times,
// done must be high 1 cycle AFTER 3rd occurrence ends
endproperty
assert property (event_3_times);
// Timeline comparison [->] vs [=]:
// Cycle: T0 T1 T2 T3 T4 T5
// pulse: 1 0 1 0 1 0
// ^1 ^2 ^3
//
// [->3]: Matches at T4 (when 3rd pulse occurs)
// [=3]: Matches at T5 (cycle after 3rd pulse)
property goto_vs_equal;
@(posedge clk) disable iff (!reset_n)
pulse[->3] |-> response; // Check response at T4
endproperty
property equal_version;
@(posedge clk) disable iff (!reset_n)
pulse[=3] |-> response; // Check response at T5
endproperty
a_goto: assert property (goto_vs_equal);
a_equal: assert property (equal_version);
// [=m:n] with range
property event_range;
@(posedge clk) disable iff (!reset_n)
event_sig[=2:5] ##1 done;
// event occurs 2-5 times, done 1 cycle after last
endproperty
assert property (event_range);
endmodule
Key Concepts:
- Immediate assertions execute like statements
- Concurrent assertions monitor over time
- Properties define temporal behavior
- Sequences define patterns
- Implication: |-> (same cycle), |=> (next cycle)
- Repetition: [*] consecutive, [->] goto, [=] non-consecutive
- disable iff for conditional checking