Systemverilog Assertion

1. Naming Conventions

2. Clock/Reset Patterns

2.1 Basic Structure

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

2.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");

3. Assertion Hygiene (Project Requirements)

• Every assertion has a label (per §1 naming) AND a failure message: else $error("[%m] ... at %0t", $time)
• Concurrent asserts at module scope only — never assert property inside always_comb, never bare immediate assert(sig) inside always_ff (simulation-only, invisible to formal)
• Unknown checks use $isunknown; verify assertion reachability with cover property
• Minimize assume property (over-constraining discards traces); validate assumes with cover
• One-hot/mutex: a_onehot_grant: assert property ($onehot0(o_grant)); — mutual exclusion: assert property (!(o_read_en && o_write_en));
• Bounded liveness: a_req_ack: assert property (i_req |-> ##[1:MAX_LATENCY] o_ack); (unbounded eventually is unprovable by BMC — see §5.3)
• Handshake pattern reference: templates/sva-bind-template.sv; FIFO safety/liveness: examples/fifo-sva-example.sv

4. Bind-File-First Policy

Attach assertions externally via a sva_{module}_checker module + bind statement — do NOT modify the RTL module. The checker module ports mirror the RTL port names verbatim (i_/o_ prefixes, sys_clk, sys_rst_n), so the bind uses (.*):

bind my_module sva_my_module_checker u_sva_checker (.*);

Complete scaffold (checker module + default clocking/disable + bind): templates/sva-bind-template.sv.

5. SymbiYosys Integration

5.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
• OSS SymbiYosys uses a generated immediate-assert harness top read with -formal -sv so Yosys keeps real $assert / $cover cells.
• SVA bind files / property files (sva_*.sv) do NOT need conversion — they remain the commercial/full-SVA path and are read with -formal -sv by tools that support bind.
• The RTL that the SVA binds to needs sv2v conversion

5.1 Formal Verification Modes

5.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!)

5.3 Liveness Caution

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