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

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

Engines

SMT Solvers

Counterexample Interpretation

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

Formal Extensions

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