Formal Verification Skill
Architecture
This skill uses a modular knowledge base. Load only the modules relevant to the current task.
Available Modules
FPV (Formal Property Verification)
| Module |
Path |
Use When |
| Property Writing |
knowledge/fpv/property-writing.md |
Writing or reviewing SVA properties/assertions |
| Engine Tuning |
knowledge/fpv/engine-tuning.md |
Selecting/configuring proof engines; deep bug hunting (DBH), hunt, swarm, and beyond-bound search route through this index |
| Complexity Management |
knowledge/fpv/complexity-management.md |
Dealing with proof complexity, capacity issues, many undetermined properties, global invariants, helper lemmas, AG/CAG, or proof_structure |
| TCL Commands |
knowledge/fpv/tcl-commands.md |
Writing TCL scripts for JasperGold/formal tools |
| Workflow |
knowledge/fpv/workflow.md |
End-to-end FPV setup, execution, debug cycle |
Shared Knowledge
| Module |
Path |
Use When |
| SVA Reference |
knowledge/shared/sva-reference.md |
SVA syntax, operators, sequences |
| Common TCL |
knowledge/shared/tcl-common.md |
TCL patterns shared across apps |
Tool-Specific
| Resource |
Path |
Use When |
| JasperGold Specifics |
tool-specific/jaspergold/ |
JasperGold-specific commands, quirks, versions |
| VC Formal Specifics |
tool-specific/vc-formal/ |
VC Formal-specific details (when available) |
How to Use This Skill
- Identify the task category from the user's request
- Read the relevant module(s) from the table above — typically 1-2 modules per task
- Check tool-specific notes if the user is working with a specific EDA tool
- Apply the knowledge following the module's decision trees and patterns
Mandatory Escalation Routing
When a JasperGold baseline leaves an assertion undetermined and the task asks
for the strongest conclusion, a falsification witness, deeper reachability, or
risk investigation, read knowledge/fpv/engine-tuning.md and
knowledge/fpv/engine-tuning/bug-hunting.md before writing the next run. Apply
the leaf's DBH activation gate and complete its mandatory DBH_DECISION record
before writing the next Tcl. Treat a missing decision record as incomplete
routing; distinguish focused bounded deepening from an actual Hunt strategy.
When a JasperGold/formal run leaves many properties undetermined after a sane
direct prove, do not continue only with longer time limits, engine racing,
ProofMaster, or ad-hoc local helpers. Read knowledge/fpv/complexity-management.md.
If the hard assertions are global invariants over many peers or generated
instances — especially no-duplicate, uniqueness, conservation, mutual exclusion,
placement, token ownership, queues/FIFOs/banks/tiles/arbiters — also read
knowledge/fpv/complexity-management/decomposition.md before choosing the next
proof shape. Treat these labels as routing triggers, not as a mandatory CAG
choice; the decomposition decision tree selects a proven compact helper or
proof_structure AG/CAG/partition and defines the required signoff gate.
Routing Examples
- "Help me write an assertion for FIFO overflow" → Read
property-writing.md + sva-reference.md
- "My proof is running forever" → Read
complexity-management.md + engine-tuning.md
- "Set up a JasperGold FPV run" → Read
workflow.md + tcl-commands.md + jaspergold/
- "414 assertions, 412 undetermined, no CEX" → Read
workflow.md + complexity-management.md + complexity-management/decomposition.md
- "Prove no duplicates across many FIFOs" → Read
complexity-management.md + complexity-management/decomposition.md
- "Convert this JasperGold script to VC Formal" → Read
tcl-commands.md + both tool-specific dirs
- "Run deep bug hunting / DBH beyond this stalled bound" → Read
engine-tuning.md, then engine-tuning/bug-hunting.md
Key Principles
- Formal verification is exhaustive — unlike simulation, it proves properties hold for ALL inputs. Guide users to leverage this strength.
- Complexity is the enemy — most FPV failures are capacity issues, not property errors. Always consider complexity implications.
- Properties should be meaningful — a proven trivial property gives false confidence. Push for properties that capture real design intent.
- Incremental verification — start simple, add complexity gradually. Don't try to prove everything at once.
- Tool awareness — know the specific tool's strengths and quirks. Check
tool-specific/ when in doubt.
1---2name: formal-verification3description: Comprehensive formal verification skill covering property writing (SVA/assertions), proof engine tuning, complexity management, TCL scripting, and end-to-end FPV workflows. Supports JasperGold and VC Formal (extensible). Use this skill whenever the user works on formal property verification (FPV), writes SVA assertions or properties, configures proof engines, debugs complexity issues, writes JasperGold/VC Formal TCL scripts, runs formal verification batch jobs, or asks about any formal verification methodology. Also trigger for CDC, RDC, lint, and coverage tasks if those modules are available. Even if the user just mentions "formal", "property", "assertion", "prove", "CEX", "counterexample", "JasperGold", "Jasper", "VC Formal", or "FPV", consult this skill.4---56# Formal Verification Skill78## Architecture910This skill uses a modular knowledge base. Load only the modules relevant to the current task.1112### Available Modules1314#### FPV (Formal Property Verification)15| Module | Path | Use When |16|--------|------|----------|17| Property Writing | `knowledge/fpv/property-writing.md` | Writing or reviewing SVA properties/assertions |18| Engine Tuning | `knowledge/fpv/engine-tuning.md` | Selecting/configuring proof engines; deep bug hunting (DBH), `hunt`, swarm, and beyond-bound search route through this index |19| Complexity Management | `knowledge/fpv/complexity-management.md` | Dealing with proof complexity, capacity issues, many `undetermined` properties, global invariants, helper lemmas, AG/CAG, or `proof_structure` |20| TCL Commands | `knowledge/fpv/tcl-commands.md` | Writing TCL scripts for JasperGold/formal tools |21| Workflow | `knowledge/fpv/workflow.md` | End-to-end FPV setup, execution, debug cycle |2223#### Shared Knowledge24| Module | Path | Use When |25|--------|------|----------|26| SVA Reference | `knowledge/shared/sva-reference.md` | SVA syntax, operators, sequences |27| Common TCL | `knowledge/shared/tcl-common.md` | TCL patterns shared across apps |2829#### Tool-Specific30| Resource | Path | Use When |31|----------|------|----------|32| JasperGold Specifics | `tool-specific/jaspergold/` | JasperGold-specific commands, quirks, versions |33| VC Formal Specifics | `tool-specific/vc-formal/` | VC Formal-specific details (when available) |3435## How to Use This Skill36371. **Identify the task category** from the user's request382. **Read the relevant module(s)** from the table above — typically 1-2 modules per task393. **Check tool-specific notes** if the user is working with a specific EDA tool404. **Apply the knowledge** following the module's decision trees and patterns4142### Mandatory Escalation Routing4344When a JasperGold baseline leaves an assertion `undetermined` and the task asks45for the strongest conclusion, a falsification witness, deeper reachability, or46risk investigation, read `knowledge/fpv/engine-tuning.md` and47`knowledge/fpv/engine-tuning/bug-hunting.md` before writing the next run. Apply48the leaf's DBH activation gate and complete its mandatory `DBH_DECISION` record49before writing the next Tcl. Treat a missing decision record as incomplete50routing; distinguish focused bounded deepening from an actual Hunt strategy.5152When a JasperGold/formal run leaves many properties `undetermined` after a sane53direct `prove`, do not continue only with longer time limits, engine racing,54ProofMaster, or ad-hoc local helpers. Read `knowledge/fpv/complexity-management.md`.5556If the hard assertions are global invariants over many peers or generated57instances — especially no-duplicate, uniqueness, conservation, mutual exclusion,58placement, token ownership, queues/FIFOs/banks/tiles/arbiters — also read59`knowledge/fpv/complexity-management/decomposition.md` before choosing the next60proof shape. Treat these labels as routing triggers, not as a mandatory CAG61choice; the decomposition decision tree selects a proven compact helper or62`proof_structure` AG/CAG/partition and defines the required signoff gate.6364### Routing Examples6566- "Help me write an assertion for FIFO overflow" → Read `property-writing.md` + `sva-reference.md`67- "My proof is running forever" → Read `complexity-management.md` + `engine-tuning.md`68- "Set up a JasperGold FPV run" → Read `workflow.md` + `tcl-commands.md` + `jaspergold/`69- "414 assertions, 412 undetermined, no CEX" → Read `workflow.md` + `complexity-management.md` + `complexity-management/decomposition.md`70- "Prove no duplicates across many FIFOs" → Read `complexity-management.md` + `complexity-management/decomposition.md`71- "Convert this JasperGold script to VC Formal" → Read `tcl-commands.md` + both tool-specific dirs72- "Run deep bug hunting / DBH beyond this stalled bound" → Read `engine-tuning.md`, then `engine-tuning/bug-hunting.md`7374## Key Principles75761. **Formal verification is exhaustive** — unlike simulation, it proves properties hold for ALL inputs. Guide users to leverage this strength.772. **Complexity is the enemy** — most FPV failures are capacity issues, not property errors. Always consider complexity implications.783. **Properties should be meaningful** — a proven trivial property gives false confidence. Push for properties that capture real design intent.794. **Incremental verification** — start simple, add complexity gradually. Don't try to prove everything at once.805. **Tool awareness** — know the specific tool's strengths and quirks. Check `tool-specific/` when in doubt.
gokeshenzhen