Command
Code Generation
Command
/gf-formal
Run formal verification
Install
> /plugin marketplace add codejunkie99/gateflow-plugin > /plugin install gateflow@gateflow
How it fires
How this command gets triggered: by you, by Claude, or both.
- Fires itselfClaude auto-loads it when your prompt matches the work.
- You can call itInvoke it directly when you want it.
- Slash command
/gf-formal
Context preview
What this command does when you run it.
Run formal verification
Command definition
gf-formal.mdname: gf-formal description: Run formal verification argument-hint: "[files...] [--property 'description']" allowed-tools: - Bash - Read - Write - Glob - Grep
GateFlow Formal Verification Command
Usage
/gf-formal rtl/fifo.sv # Auto-generate and prove properties /gf-formal rtl/fifo.sv --property "never overflows" # Prove specific property /gf-formal formal/fifo.sby # Run existing .sby config
Execution
1. If argument is `.sby` file: run directly with `sby -f <file>.sby` 2. If argument is `.sv` file: a. Read the module b. Generate SVA properties (or use --property hint) c. Create `.sby` configuration d. Run SymbiYosys e. Report with 3-layer error translation 3. If no arguments: find `.sby` configs in `formal/` and run all
Ships withgateflow-plugin
AI-powered hardware development platform — design, verify, synthesize, and deploy working RTL with natural language. Supports SystemVerilog, Verilog, and VHDL across the full open-source FPGA toolchain. Loving hardware doesn't have to be gatekept.
Get the whole plugin
Other commands on gateflow-plugin.
Command
Command
Command
gf-demo
One-command demo - generates, lints, and simulates a working project
@codejunkie99Install CommandCommand
Command