SVA Assertion Writer — IC HDL Agent Skill

name: assertion-writer description: > Generate SystemVerilog Assertions (SVA) for a given RTL module. Covers immediate assertions (combinational checks), concurrent assertions (temporal sequences), and assume/cover statements. Assertions verify interface protocols, data integrity, FSM correctness, FIFO overflow/underflow, handshake compliance, and CDC properties. Generates assertions suitable for simulation, formal verification (JasperGold, Questa Formal), and FPGA debug (Vivado assert IP). category: verification level: advanced

Purpose

Generate a comprehensive set of SVA assertions that catch bugs at their source — the instant a signal violates its specification. Assertions document design intent in executable form and serve as both verification checkers and formal properties.

Input Specification

Required

DUT interface: Port list, signal directions, widths
Design specification: What behavior is legal and illegal

Optional

Assertion type preference: simulation-only, formal-compatible, or both
Coverage goals: which properties to cover
Tool target: Questa, VCS, Xcelium, JasperGold (affects system function usage)

Core Categories of Assertions

Category 1: Interface Protocol Checks

Verify that external interfaces obey their protocol:

systemverilog

// AXI-Stream: data must be stable when valid is asserted and ready is not yet true
property axist_data_stable;
    @(posedge clk) disable iff (!rst_n)
    (s_valid && !s_ready) |=> $stable(s_data);
endproperty
AXIST_DATA_STABLE: assert property (axist_data_stable)
    else $error("AXI-Stream data changed while valid asserted and not ready");

// AXI-Stream: valid must not de-assert before ready
property axist_valid_stable;
    @(posedge clk) disable iff (!rst_n)
    (s_valid && !s_ready) |=> s_valid;
endproperty
AXIST_VALID_STABLE: assert property (axist_valid_stable)
    else $error("AXI-Stream valid de-asserted before handshake");

Category 2: Data Integrity Checks

Verify that data transformations are correct:

systemverilog

// FIFO: read data must match what was written (same order)
// Requires a shadow model / scoreboard
property fifo_data_integrity;
    @(posedge clk) disable iff (!rst_n)
    // (implementation depends on scoreboard, not pure SVA)
endproperty

// Counter: count must increment by 1 when enabled
property counter_increment;
    @(posedge clk) disable iff (!rst_n)
    (en && !clear) |=> (count == $past(count) + 1);
endproperty
COUNT_INC: assert property (counter_increment);

Category 3: FSM Correctness

systemverilog

// One-hot state encoding check
property fsm_onehot;
    @(posedge clk) disable iff (!rst_n)
    $onehot0(state);  // 0 or exactly 1 bit set
endproperty
FSM_ONEHOT: assert property (fsm_onehot);

// State must never be unknown
property fsm_known;
    @(posedge clk) disable iff (!rst_n)
    !$isunknown(state);
endproperty
FSM_KNOWN: assert property (fsm_known);

// Specific illegal state transitions
property fsm_no_direct_idle_to_error;
    @(posedge clk) disable iff (!rst_n)
    (state == IDLE) |=> (state != ERROR);
endproperty
FSM_NO_IDLE_TO_ERROR: assert property (fsm_no_direct_idle_to_error);

Category 4: FIFO Properties

systemverilog

// Never overflow: write when full is forbidden
property fifo_no_overflow;
    @(posedge clk) disable iff (!rst_n)
    full |-> !wr_en;
endproperty
FIFO_NO_OVERFLOW: assert property (fifo_no_overflow);

// Never underflow: read when empty is forbidden
property fifo_no_underflow;
    @(posedge clk) disable iff (!rst_n)
    empty |-> !rd_en;
endproperty
FIFO_NO_UNDERFLOW: assert property (fifo_no_underflow);

// Empty flag must be set when count is 0
property fifo_empty_when_zero;
    @(posedge clk) disable iff (!rst_n)
    (count == 0) |-> empty;
endproperty
FIFO_EMPTY_CHECK: assert property (fifo_empty_when_zero);

// Full flag must be set when count equals depth
property fifo_full_when_depth;
    @(posedge clk) disable iff (!rst_n)
    (count == DEPTH) |-> full;
endproperty
FIFO_FULL_CHECK: assert property (fifo_full_when_depth);

Category 5: Mutex and Arbitration

systemverilog

// Grant must be one-hot (at most one master granted)
property arbiter_grant_onehot;
    @(posedge clk) disable iff (!rst_n)
    $onehot0(gnt);
endproperty
ARB_GNT_ONEHOT: assert property (arbiter_grant_onehot);

// Grant implies corresponding request
property arbiter_grant_implies_request;
    @(posedge clk) disable iff (!rst_n)
    gnt |-> (gnt & req) == gnt;
endproperty
ARB_GNT_REQ: assert property (arbiter_grant_implies_request);

Category 6: Reset Behavior

systemverilog

// All outputs must be at reset values during reset
property reset_outputs;
    @(posedge clk) disable iff (1'b0)  // always check, even during reset
    !rst_n |-> (valid == 1'b0) && (ready == 1'b0) && (data == '0);
endproperty
RESET_OUTPUTS: assert property (reset_outputs);

Category 7: Coverage Properties

systemverilog

// Cover: has the FIFO ever been full?
FIFO_FULL_COVER: cover property (@(posedge clk) full);

// Cover: has back-to-back write then read occurred?
BACK_TO_BACK: cover property (@(posedge clk) wr_en ##1 rd_en);

// Cover: all state transitions
STATE_TRANS_COVER: cover property (@(posedge clk)
    (state == IDLE) ##1 (state != IDLE));

Output Template

systemverilog

// =============================================================================
// SVA Assertion Module: [module_name]_assertions
// Design: [design_name]
// Generated by: ICHDL Agent (assertion-writer)
// =============================================================================

module [module_name]_assertions (
    input logic clk,
    input logic rst_n,
    // ... all signals needed for assertions ...
);

    // ---- Interface Protocol Checks ----
    // ...

    // ---- Data Integrity Checks ----
    // ...

    // ---- FSM Correctness ----
    // ...

    // ---- Cover Properties ----
    // ...

endmodule

Binding Assertions to DUT

systemverilog

// In testbench or separate bind file:
bind dut_module [module_name]_assertions u_assertions (.*);

Common Mistakes to Flag

Assertions that fire during reset (always use disable iff (!rst_n))
Over-constrained assertions that fire on legal behavior
Missing $isunknown checks for X/Z propagation detection
Assertions without error messages (always add else $error(...))
Concurrent assertions in combinational always blocks (use immediate assertions there)

Interaction with Other Skills

verilog-module: The DUT being verified
fsm-generator: FSM-specific assertions
fifo-generator: FIFO-specific assertions
cdc-synchronizer: CDC protocol assertions
testbench-simple: Bind assertions module into testbench

Disclaimer

This skill is provided "as is" for reference and educational purposes only. Code generated using this skill should be independently reviewed and verified before use in any production design, tape-out, or safety-critical application. The author(s) and ICHDL assume no liability for any errors, omissions, or damages arising from the use of this skill or any code generated with it.

Usage Rights

You are free to use, modify, and distribute this skill for personal or commercial purposes. Attribution to ICHDL (ichdl.com) is appreciated but not required. Redistribution of this skill in substantially unmodified form must retain this notice.