Stats
Actions
Tags
From gateflow
Generates SVA properties from natural language, configures SymbiYosys, runs formal proofs on hardware designs like FIFOs, and explains pass/fail results.
How this skill is triggered — by the user, by Claude, or both
Slash command
/gateflow:gf-formalThis skill is limited to the following tools:
The summary Claude sees in its skill listing — used to decide when to auto-load this skill
```bash
which sby
If not found:
---GATEFLOW-RESULT---
STATUS: ERROR
DETAILS: SymbiYosys not installed. Install to enable formal verification.
pip install symbiyosys
Also need: yosys, z3 (or yices2)
macOS: brew install yosys z3
Linux: sudo apt install yosys z3
---END-GATEFLOW-RESULT---
sby -f <config>.sby---GATEFLOW-RESULT---
STATUS: PASS | FAIL | ERROR
PROOFS: N proved, M failed, K covers
FILES: [generated files]
DETAILS: [proof results or counterexample explanation]
---END-GATEFLOW-RESULT---
Formal verification is an optional enhancement step:
npx claudepluginhub codejunkie99/gateflow-plugin --plugin gateflowExtracts SystemVerilog Assertions from RTL and runs formal verification with SymbiYosys BMC/induction. Proves or disproves properties for exhaustive corner-case coverage.
Provides behavioral guidelines to reduce common LLM coding mistakes, focusing on simplicity, surgical changes, assumption surfacing, and verifiable success criteria.