codejunkie99/gf-formal

GF-Formal -- Formal Verification Skill

Tool Detection

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

[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

[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

[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)

[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

a_no_overflow: assert property (
    @(posedge clk) disable iff (rst) full |-> !wr_en);

No Underflow

a_no_underflow: assert property (
    @(posedge clk) disable iff (rst) empty |-> !rd_en);

Valid/Ready Handshake

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

a_onehot: assert property (
    @(posedge clk) disable iff (rst) $onehot(state));

Liveness

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

Reset Behavior

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

FIFO Count

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 |

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