gf-formal

---
name: "gf-formal"
description: "Parse request -- What properties to verify? Which module?; Read the design -- Understand ports, signals, behavior; Spawn sv-formal agent -- Generate properties + .sby config"
license: "Apache-2.0"
---

# GF-Formal -- Formal Verification Skill

## Tool Detection

```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---
```

## Workflow

1. Parse request -- What properties to verify? Which module?
2. Read the design -- Understand ports, signals, behavior
3. Spawn sv-formal agent -- Generate properties + .sby config
4. Run SymbiYosys: `sby -f <config>.sby`
5. Parse results -- Read sby output for pass/fail/counterexample
6. Report -- 3-layer error translation if failed, clear summary if passed

## Result Format

```
---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---
```

## Integration with /gf Orchestrator

Formal verification is an optional enhancement step:
- After simulation passes, for safety-critical designs
- When user explicitly requests formal verification
- For CDC, FIFO, or protocol designs

## .sby Configuration Templates

### BMC Template
```sby
[tasks]
bmc
[options]
mode bmc
depth 20
expect pass
[engines]
smtbmc z3
[script]
read -formal design.sv
prep -top top_module
[files]
design.sv
```

### Prove Template
```sby
[tasks]
prove
[options]
mode prove
depth 40
expect pass
[engines]
smtbmc z3
abc pdr
[script]
read -formal design.sv
prep -top top_module
[files]
design.sv
```

### Cover Template
```sby
[tasks]
cover
[options]
mode cover
depth 30
expect pass
[engines]
smtbmc z3
[script]
read -formal design.sv
prep -top top_module
[files]
design.sv
```

### Multi-Task (BMC + Prove + Cover)
```sby
[tasks]
bmc
prove
cover
[options]
bmc: mode bmc
bmc: depth 20
prove: mode prove
prove: depth 40
cover: mode cover
cover: depth 30
expect pass
[engines]
bmc: smtbmc z3
prove: smtbmc z3
prove: abc pdr
cover: smtbmc z3
[script]
read -formal design.sv
prep -top top_module
[files]
design.sv
```

### .sby Options
| Option | Modes | Description |
|--------|-------|-------------|
| `mode` | all | `bmc`, `prove`, `cover`, or `live` |
| `depth` | bmc, cover | Cycles to check (default 20) |
| `timeout` | all | Timeout in seconds |
| `multiclock` | all | Multiple clocks / async |
| `expect` | all | Expected: pass, fail, unknown |

## SVA Property Patterns

### No Overflow
```systemverilog
a_no_overflow: assert property (
    @(posedge clk) disable iff (rst) full |-> !wr_en);
```

### No Underflow
```systemverilog
a_no_underflow: assert property (
    @(posedge clk) disable iff (rst) empty |-> !rd_en);
```

### Valid/Ready Handshake
```systemverilog
a_valid_stable: assert property (
    @(posedge clk) disable iff (rst) (valid && !ready) |=> valid);
a_data_stable: assert property (
    @(posedge clk) disable iff (rst) (valid && !ready) |=> $stable(data));
```

### One-Hot
```systemverilog
a_onehot: assert property (
    @(posedge clk) disable iff (rst) $onehot(state));
```

### Liveness
```systemverilog
a_req_granted: assert property (
    @(posedge clk) disable iff (rst) req |-> ##[1:MAX_LATENCY] grant);
```

### Reset Behavior
```systemverilog
a_reset: assert property (
    @(posedge clk) rst |-> (data_out == '0) && (count == '0));
```

### FIFO Count
```systemverilog
a_count_inc: assert property (
    @(posedge clk) disable iff (rst)
    (wr_en && !rd_en && !full) |=> (count == $past(count) + 1));
```

## Proof Strategy

| Property Type | Approach | Engine |
|---|---|---|
| Simple bounds | BMC then prove | `smtbmc z3` |
| Protocol compliance | BMC + prove | `smtbmc z3`, `abc pdr` |
| FSM correctness | Prove | `abc pdr` |
| Liveness | Live mode | `aiger suprove` |
| Complex arithmetic | BMC | `smtbmc bitwuzla` |

## Engines

| Engine | Modes | Strengths |
|---|---|---|
| `smtbmc` | bmc, prove, cover | Readable traces, k-induction |
| `abc pdr` | prove | Unbounded proofs, auto-invariants |
| `abc bmc3` | bmc | Fast bit-level checking |
| `aiger suprove` | prove, live | Liveness verification |

### SMT Solvers
| Solver | Best For |
|---|---|
| `z3` | Good default |
| `yices` | Fast bit-vectors |
| `bitwuzla` | Complex arithmetic |
| `boolector` | Hardware-specialized |

## Counterexample Interpretation

| Failure | Trace Location |
|---|---|
| BMC | `<task>/engine_0/trace.vcd` |
| Induction | `<task>/engine_0/trace_induct.vcd` |
| Cover | `<task>/engine_0/trace<N>.vcd` |

### Debugging
- BMC fails: counterexample is reachable, fix design
- Prove fails but BMC passes: unreachable induction state, add invariants or use `abc pdr`
- Cover fails: over-constrained, relax assumptions

| Pattern | Fix |
|---|---|
| Missing initial value | Add reset logic |
| Unconstrained input | Add `assume` properties |
| Unreachable induction | Strengthen invariants or use `abc pdr` |

## Formal Extensions

| Directive | Purpose |
|---|---|
| `assert(expr)` | Must always be true |
| `assume(expr)` | Constrain solver inputs |
| `cover(expr)` | Reachability target |

| Attribute | Behavior |
|---|---|
| `(* anyconst *)` | Solver picks constant |
| `(* anyseq *)` | Solver picks per-cycle |

```systemverilog
`ifdef FORMAL
    initial assume(rst);
    always @(posedge clk) begin
        a_example: assert(count <= MAX);
        c_reach: cover(count == MAX);
    end
`endif
```