systemverilog-assertion

1. Assertion Style Classification

Usage Guide

• Shared between simulation + formal: use assert property
• Formal-only input constraints: use assume property
• Coverage targets: use cover property
• Immediate assert is for combinational checks only (inside always_comb)

2. Naming Conventions

3. Clock/Reset Patterns

3.1 Basic Structure

// All concurrent assertions use default clocking + disable iff
default clocking cb @(posedge sys_clk); endclocking
default disable iff (!sys_rst_n);

3.2 Past-Valid Guard

The $past() value is invalid on the first cycle after reset, so use a guard:

logic past_valid;
always_ff @(posedge sys_clk or negedge sys_rst_n) begin
  if (!sys_rst_n) past_valid <= 1'b0;
  else            past_valid <= 1'b1;
end

// Always check past_valid when using $past
a_data_stable: assert property (
  past_valid && $rose(i_valid) |-> ##1 $stable(i_data)
) else $error("Data must be stable after valid rises");

4. Core Assertion Patterns

4.1 Valid/Ready Handshake

// Valid must hold until ready
a_valid_hold: assert property (
  i_valid && !o_ready |=> i_valid
) else $error("valid must hold until ready");

// Data must be stable while valid
a_data_stable: assert property (
  i_valid && !o_ready |=> $stable(i_data)
) else $error("data must be stable while valid && !ready");

// No unknowns allowed
a_valid_no_x: assert property (
  !$isunknown(i_valid)
) else $error("valid must not be X/Z");

4.2 FIFO Safety

a_no_overflow: assert property (
  i_push && !i_pop |-> o_count < DEPTH
) else $error("FIFO overflow: push when full");

a_no_underflow: assert property (
  i_pop && !i_push |-> o_count > 0
) else $error("FIFO underflow: pop when empty");

4.3 One-Hot / Mutex

a_onehot_grant: assert property (
  $onehot0(o_grant)
) else $error("Grant must be one-hot or zero");

a_mutex_access: assert property (
  !(o_read_en && o_write_en)
) else $error("Simultaneous read and write forbidden");

4.4 Liveness (Eventually)

// Request must be acknowledged within N cycles
a_req_ack: assert property (
  i_req |-> ##[1:MAX_LATENCY] o_ack
) else $error("No ack within MAX_LATENCY cycles");

5. Bind File Patterns

Attach assertions externally without modifying the RTL module:

// sva_my_module.sv
module sva_my_module_checker (
  input logic       sys_clk,
  input logic       sys_rst_n,
  input logic [7:0] i_data,
  input logic       i_valid,
  input logic       o_ready
);
  default clocking cb @(posedge sys_clk); endclocking
  default disable iff (!sys_rst_n);

  // Assertions here...
  a_valid_hold: assert property (
    i_valid && !o_ready |=> i_valid
  ) else $error("valid must hold until ready");
endmodule

// Bind statement (separate file or bottom of same file)
bind my_module sva_my_module_checker u_sva_checker (.*);

See templates/sva-bind-template.sv for complete scaffold.

6. SymbiYosys Integration

6.0 sv2v Conversion (Mandatory for SymbiYosys/Yosys)

SymbiYosys uses Yosys internally, which has limited SystemVerilog support. RTL .sv files must be converted to Verilog via sv2v before running sby:

sv2v rtl/{module}/*.sv -o rtl/{module}/{module}_v2v.v

• The .sby config [files] section must list the converted _v2v.v file, not .sv
• SVA bind files / property files (sva_*.sv) do NOT need conversion — they are read with -formal -sv by SymbiYosys
• The RTL that the SVA binds to needs sv2v conversion

6.1 Formal Verification Modes

6.2 assume vs assert

• assume: input constraint for formal tool (behaves like assert in simulation)
• assert: property under verification
• In formal, traces violating assume are discarded (beware of over-constraining!)

6.3 Liveness Caution

• BMC cannot prove liveness properties (eventually) — use prove mode
• Even in prove mode, infinite waits may cause induction failure → add bounds

7. Anti-Patterns