Rtl P5s Sva Policy

SVA property extraction must iterate at least 3 times to strengthen assertion quality. Each round builds upon the previous:

• Round 1 (Draft): Extract initial properties from RTL and uarch spec. Focus on safety (no overflow, no deadlock) and protocol (handshake) properties.
• Round 2 (Strengthen): Review Round 1 properties for completeness. Add missing edge cases: reset behavior, boundary conditions, back-to-back transactions, error paths. Add cover properties to verify reachability. Check for vacuous assertions.
• Round 3 (Harden): Cross-check against spec requirements. Add liveness properties (##[1:N] bounded eventually). Verify assume/assert balance (not over-constrained). Add cross-module interface properties if applicable.
• Additional rounds: Continue if coverage of spec requirements < 100% or if new RTL paths are discovered.

Each round produces a review note at .rat/scratch/phase-5/sva-iteration-r{N}.md.

Escalation & Stop Conditions

• SymbiYosys not installed → halt, instruct user to install (pip install sbyosys or from source)
• Property timeout (>200 depth) → mark as "timeout" in formal_verify.json, recommend simulation
• Counterexample found → report to user with waveform trace before any RTL fix
• SVA signal names do not match RTL ports → sva-extractor must fix before running formal

Final Checklist

• formal/*.sv written with meaningful properties
• All SVA signal references match RTL port names (i_/o_ prefix, {domain}_clk/{domain}_rst_n)
• formal_verify.json produced with status per property
• No "failed" status without counterexample attached
• Timeouts documented and flagged for simulation fallback

Assume/Assert Principle and Engine Guide

Use assume statements to constrain inputs to legal protocol ranges before proving. Principle: assume inputs, assert outputs. Inputs are constrained with assume; outputs are verified with assert. Target properties: no deadlock, no overflow, interface protocol compliance, data integrity. Assertion clock: @(posedge sys_clk) disable iff (!sys_rst_n) for synchronous properties.

See examples/handshake-assertions.sv for valid/ready handshake SVA patterns. See examples/fifo-assertions.sv for FIFO overflow/underflow assertion patterns.

SymbiYosys engine guide:

See references/sva-patterns.md for complete temporal operator reference and pattern library.

sv2v conversion note: SymbiYosys relies on Yosys for reading design files. Yosys has limited SystemVerilog support, so RTL .sv files need Verilog conversion before sby. This is a Layer 2 concern — formal verification scripts handle sv2v conversion internally. Do NOT run sv2v manually. SVA property files (formal/*_props.sv) are read with -formal -sv and do NOT need conversion.

# Scripts handle sv2v internally:
sby -f formal/{module}.sby   # .sby task script runs sv2v as a pre-step