Assertion-Based Specification Design

SVA methodology treating assertions as executable specifications, not testbench utilities.

Core Principle (MANDATORY)

Specifications SHALL be written as SystemVerilog Assertions

• Natural language explanations are secondary and optional
• RTL implementation details MUST NOT be referenced unless unavoidable
• Written assertions MUST be sufficient to understand intended behavior without reading RTL
• Assertions define what the design must do, not how it does it

When to Use This Skill

• Defining timing specifications for RTL modules
• Specifying protocol requirements (AXI4, UART, custom interfaces)
• Creating formal properties for transaction sequences
• Reviewing assertion coverage completeness
• Debugging temporal property failures

Directory and File Policy (MANDATORY)

Assertion File Locations

sim/assertions/
├── spec/              # Timing-related specifications (REQUIRED location)
│   ├── uart_timing_spec.sva
│   ├── axi4_protocol_spec.sva
│   └── frame_parser_timing_spec.sva
├── functional/        # Functional correctness assertions
│   ├── Frame_Parser_Assertions.sv
│   └── Uart_Tx_Assertions.sv
└── bind/              # Bind statements
    ├── bind_Frame_Parser.sv
    └── bind_Uart_Tx.sv

Critical Rules:

• All timing-related specifications → sim/assertions/spec/
• Functional module assertions → sim/assertions/functional/
• Bind statements → sim/assertions/bind/
• NEVER embed assertions inside DUT modules

Assertion Separation (MANDATORY)

❌ Wrong: Assertions in DUT

module Frame_Parser (/*...*/);
    // ❌ Never embed assertions in DUT
    assert property (@(posedge clk) frame_valid |-> byte_count >= 4);
endmodule

✅ Correct: Separate Assertion Module

// File: sim/assertions/functional/Frame_Parser_Assertions.sv
module Frame_Parser_Assertions (
    input logic clk, 
    input logic rst, 
    input logic frame_valid,
    input logic [7:0] byte_count
);
    // Property definition
    property p_frame_minimum_length;
        @(posedge clk) disable iff (rst)
        frame_valid |-> byte_count >= 4;
    endproperty
    
    // Assertion
    a_frame_minimum_length: assert property (p_frame_minimum_length)
        else $error("Frame length violation: byte_count=%0d", byte_count);
    
    // Optional coverage
    c_frame_minimum_length: cover property (p_frame_minimum_length);
endmodule

Bind Statement

// File: sim/assertions/bind/bind_Frame_Parser.sv
`ifdef ENABLE_ASSERTIONS
bind Frame_Parser Frame_Parser_Assertions u_assertions (
    .clk(clk),
    .rst(rst),
    .frame_valid(frame_valid),
    .byte_count(byte_count)
);
`endif

Enable at compile time:

dsim +define+ENABLE_ASSERTIONS -f dsim_config.f

Specification-First Design Pattern

1. Define Requirements as Properties

Example: UART protocol timing spec

// File: sim/assertions/spec/uart_timing_spec.sva
module uart_timing_spec (
    input logic clk,
    input logic rst,
    input logic tx_start,
    input logic tx_done,
    input logic [15:0] baud_counter
);
    // Specification: TX duration must match baud rate
    property p_tx_duration;
        int start_time;
        @(posedge clk) disable iff (rst)
        (tx_start, start_time = $time) |-> 
        ##[1:$] (tx_done && ($time - start_time >= baud_counter * 10));
    endproperty
    
    a_tx_duration: assert property (p_tx_duration)
        else $error("TX duration too short");
    
    // Specification: No overlapping TX operations
    property p_no_tx_overlap;
        @(posedge clk) disable iff (rst)
        tx_start |-> !tx_start throughout ##[1:$] tx_done;
    endproperty
    
    a_no_tx_overlap: assert property (p_no_tx_overlap)
        else $error("TX overlap detected");
endmodule

2. Property Naming Convention

Use p_ prefix for properties, a_ for assertions, c_ for coverage:

property p_handshake_valid_before_ready;
    @(posedge clk) disable iff (rst)
    ready |-> valid;
endproperty

a_handshake: assert property (p_handshake_valid_before_ready)
    else $error("Ready asserted without valid");

c_handshake: cover property (p_handshake_valid_before_ready);

3. Formal Properties vs Implementation

Good (specification-focused):

// Specifies: "Request must be followed by acknowledge within 10 cycles"
property p_request_ack_latency;
    @(posedge clk) disable iff (rst)
    request |-> ##[1:10] acknowledge;
endproperty

Bad (implementation-focused):

// ❌ References internal state machine states
property p_state_machine_transition;
    @(posedge clk) disable iff (rst)
    (state == WAIT_ACK) |-> ##[1:10] (state == IDLE);
endproperty

Temporal Operators

Delay Operators

// Fixed delay: exactly N cycles later
##N expr       // expr true N cycles after trigger

// Range delay: between M and N cycles
##[M:N] expr   // expr true M to N cycles after trigger

// Unbounded delay: eventually
##[1:$] expr   // expr true sometime in the future

Implication Operators

// Overlapping implication (same cycle)
antecedent |-> consequent

// Non-overlapping implication (next cycle)
antecedent |=> consequent

// Example: handshake protocol
property p_valid_ready_handshake;
    @(posedge clk) disable iff (rst)
    valid && ready |-> ##1 !valid;  // Valid drops after handshake
endproperty

Repetition Operators

// Consecutive repetition
signal[*N]             // signal true for exactly N cycles
signal[*M:N]           // signal true for M to N cycles

// Go-to repetition (allows gaps)
signal[->N]            // signal becomes true N times (eventually)

// Example: burst detection
property p_burst_transfer;
    @(posedge clk) disable iff (rst)
    burst_start |-> valid[*4];  // 4 consecutive valid cycles
endproperty

Throughout Operator

// Condition must hold throughout sequence
property p_hold_valid_until_ready;
    @(posedge clk) disable iff (rst)
    valid |-> valid throughout ##[1:$] ready;
endproperty

AXI4-Lite Protocol Assertions

Example specification for AXI4-Lite write channel:

// File: sim/assertions/spec/axi4_protocol_spec.sva
module axi4_protocol_spec (
    input logic clk,
    input logic rst,
    input logic awvalid, awready,
    input logic wvalid, wready,
    input logic bvalid, bready
);
    // AXI4 Rule: AWVALID stable until AWREADY
    property p_awvalid_stable;
        @(posedge clk) disable iff (rst)
        (awvalid && !awready) |=> $stable(awvalid);
    endproperty
    
    a_awvalid_stable: assert property (p_awvalid_stable)
        else $error("AXI4 violation: AWVALID changed before AWREADY");
    
    // AXI4 Rule: BVALID after both AW and W handshakes
    property p_bvalid_ordering;
        logic aw_done, w_done;
        @(posedge clk) disable iff (rst)
        (awvalid && awready, aw_done = 1) ##0
        (wvalid && wready, w_done = 1) ##0
        (aw_done && w_done) |-> ##[1:$] bvalid;
    endproperty
    
    a_bvalid_ordering: assert property (p_bvalid_ordering)
        else $error("AXI4 violation: BVALID ordering incorrect");
endmodule

Debugging Assertion Failures

1. Enable Assertions with MCP

python mcp_server/mcp_client.py --workspace . --tool run_uvm_simulation \
    --test-name axiuart_basic_test --mode run --waves \
    --compile-args "+define+ENABLE_ASSERTIONS"

2. Assertion Failure Prioritization

Investigate assertion failures BEFORE waveform inspection:

1. Read assertion error message and property name
2. Identify violated specification requirement
3. Check if failure is DUT bug or assertion bug
4. Use waveform to understand failure context

3. Error Message Best Practices

a_setup_time: assert property (p_setup_time_met)
    else $error("[%0t] Setup time violation: data=0x%h, required_stable=%0d cycles",
        $time, data_signal, SETUP_CYCLES);

Assertion Coverage

Measuring Specification Coverage

// Cover all specified behaviors
c_normal_operation: cover property (p_normal_frame_processing);
c_error_recovery: cover property (p_error_frame_recovery);
c_back_to_back: cover property (p_back_to_back_frames);

// Cover corner cases
c_minimum_latency: cover property (
    @(posedge clk) disable iff (rst)
    request |-> ##1 acknowledge
);

c_maximum_latency: cover property (
    @(posedge clk) disable iff (rst)
    request |-> ##10 acknowledge
);

Compilation Control

Conditional Compilation

`ifdef ENABLE_ASSERTIONS
module My_Module_Assertions (/*...*/);
    // Assertions here
endmodule

bind My_Module My_Module_Assertions u_assertions (.*);
`endif

Severity Levels

// Error (test fails)
assert property (p_critical) else $error("Critical failure");

// Warning (logged but test continues)
assert property (p_recommended) else $warning("Recommended practice violated");

// Info (just notification)
assert property (p_performance) else $info("Suboptimal performance detected");

// Fatal (simulation stops immediately)
assert property (p_safety_critical) else $fatal(1, "Safety violation - halting");

Project-Specific Guidelines

Reference Material

Follow detailed guidelines in:

• sim/assertions/README.md - Assertion coding guidelines
• docs/forCopilot-assertions.md - Comprehensive assertion design rules (if exists)

File Organization

sim/assertions/
├── spec/
│   └── <module>_timing_spec.sva          # Timing specifications
├── functional/
│   └── <Module>_Assertions.sv            # Functional properties
└── bind/
    └── bind_<Module>.sv                  # Bind statements

Integration with MCP Workflow

MCP server can enable/disable assertions dynamically. See mcp-workflow skill for detailed command sequences.

Additional Resources

• Assertion guidelines: sim/assertions/README.md
• DSIM assertion debugging: Reference dsim-debugging skill
• RTL coding standards: Reference rtl-coding-standards skill for module structure

Summary

Assertion design principles:

1. Assertions define specifications, not implementations
2. Never embed assertions in DUT modules - use separate assertion modules with bind
3. Timing specs → sim/assertions/spec/
4. Use p_ prefix for properties, a_ for assertions, c_ for coverage
5. Assertions drive debugging - investigate failures before waveforms
6. Enable with +define+ENABLE_ASSERTIONS at compile time
7. Properties should be RTL-agnostic (specify behavior, not structure)