Core capabilities
- Combinational equivalence checking (CEC): Compare combinational logic equivalence—common after synthesis and optimization.
- Sequential equivalence checking (SEC): Sequential timing equivalence for post-ECO or local modification verification.
- Counterexample generation: When not equivalent, output counterexamples (input vector + difference point) for debug.
- External adapter layer: Currently calls external commercial formal engines; D1 shadow interface definition complete.
- Agent-ready: Python API wraps CEC/SEC submission and returns structured equivalence results.
Agent calling patterns
cec = client.call("iFormal.check_equivalence",
design_ref="snap_a",
reference_ref="snap_b"
)
# cec.equivalent → bool
# cec.counter_example → dict | None (counterexample when not equivalent)
# cec.proof_log → str (proof summary)Input / output contract
| Direction | Parameter | Type | Description |
|---|---|---|---|
| Input | design_ref | str | Design snapshot to verify (e.g. post-synthesis netlist) |
| Input | reference_ref | str | Reference snapshot (e.g. original RTL or golden netlist) |
| Input | mode | str (optional) | Verification mode: cec | sec, default cec |
| Output | equivalent | bool | Whether the two designs are logically equivalent |
| Output | counter_example | dict (optional) | Counterexample when not equivalent (input vector, differing signals) |
| Output | proof_log | str | Proof log with checkpoint count and runtime |
Role in the flow
01 Synth
iMap
Logic synthesis & tech mapping
02 Verify
iFormal
Post-synthesis CEC equivalence check
03 Physical design
iFP · iPL · iCTS · iRT
Full place & route flow
04 ECO verify
iFormal · iLVS
Post-change equivalence and LVS
iFormal runs after synthesis and after ECO: verify pre/post-synthesis netlist equivalence and that local changes preserve function. Pairs with iLVS for a complete verification loop.
Related resources
- iLVS — Layout vs. schematic: Physical verification; complements iFormal logic verification.
- iMap — Tech mapping: Synthesis tool; its output is a typical iFormal CEC target.
- EDA tools overview: Map of all 22 point tools.