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