This skill should be used when proving or disproving formal properties on RTL using SymbiYosys BMC and induction. Triggers on 'formal verification', 'prove property', 'SVA'.
See references/sva-patterns.md for SVA temporal operator reference, common assertion patterns,
and SymbiYosys engine selection guide.
</Purpose>
<Use_When>
<Do_Not_Use_When>
<Why_This_Exists> Simulation cannot exhaustively cover all corner cases. Formal verification proves properties hold for all possible inputs, catching bugs that would take millions of simulation cycles to find. SymbiYosys is open-source and integrates cleanly with Yosys-based flows. </Why_This_Exists>
RTL modules required:
rtl/**/*.sv files must existIf prerequisite is missing: WARNING — recommend running . Proceed with available artifacts — orchestrator will adapt scope.
/rtl-agent-team:rtl-p4-implementTask(subagent_type="rtl-agent-team:p5s-sva-orchestrator", prompt="Execute SVA formal verification. User input: $ARGUMENTS")
Do not perform any work directly. The orchestrator agent manages 3-round SVA refinement, sv2v conversion, SymbiYosys BMC/induction execution, and counterexample diagnosis.