Formality

页

工具概述

定位与起源

定位与起源：Formality是Synopsys的等价性检查工具——用形式验证(Formal Verification)的方法证明两个设计在功能上是等价的。Formality最核心的应用是：证明RTL和综合后的门级网表功能等价——这是tape-out的必须检查项。

Formality由Synopsys于1990年代推出——基于BDD(二元决策图)和SAT求解器的组合引擎。在IC设计流程中，Formality是"守门人"——每次综合、每次ECO、每次DFT插入——门级网表都在变——Formality证明这些变化没有改变功能。等价性检查fail→不能tape-out。

核心技术

组合等价+时序等价：组合等价——在两个设计中所有寄存器一一对应——组合逻辑功能相同。时序等价——pipeline retiming后寄存器位置变了——但整个周期的输入→输出功能不变。时序等价是Formality的高级能力——也是复杂CPU/GPU设计中最需要的。

BDD+SAT混合引擎：Formality用BDD处理常规逻辑等价——用SAT求解器处理复杂的算术等价(乘法器优化后的结构完全不同但算术结果相同)。BDD快但内存爆炸——SAT慢但内存小——混合引擎自动选择最优算法。

ECO等价性检查：ECOs后只改了几十个门——Formality的增量等价检查只验证改动部分——不需要重新验证整个设计。验证时间从小时级降到分钟级。

低功耗等价性检查：当设计加入isolation cells、level shifters、retention registers后——Formality验证这些低功耗单元没有改变功能逻辑。这是UPF/CPF验证的关键一环。

主要功能

* RTL vs Gate等价：综合后的网表vs原始RTL——证明功能等价——tape-out必须过。 * Gate vs Gate等价：DFT插入后/CTS后/ECO后 vs 原始网表——证明改动未改变功能。 * 增量ECO验证：只验证ECO改动的部分——几分钟完成——支持快速ECO迭代。 * 低功耗等价：验证UPF插入的isolation/level shifter/retention不影响功能逻辑。

实战案例

- 某CPU的retiming等价性检查：综合时做了aggressive retiming——寄存器位置大幅变化。Formality时序等价检查证明retiming后功能不变——避免了手工review retiming的噩梦。 - Formality抓到一个ECO bug：某ECO修改了一个AND门为OR门——Formality报不等价。根因：ECO工具在spare cell中选错了类型(AND vs OR在spare cell库中外观相同但功能不同)。 - 低功耗等价检查：某设计插入了2000+isolation cells后——Formality验证全部等价——发现3个isolation钳位值选错——在tape-out前修复。

常见误区

误区一：Formality=简单比对。 综合后的网表和RTL在结构上完全不同——组合逻辑被重新映射、共享、合并。Formality需要证明结构不同的两个网表功能相同——这需要SAT/BDD求解——不是简单的结构比对。

误区二：等价性检查pass=功能正确。 Formality只证明"这两个网表等价"——不证明"它们本身功能正确"。如果RTL有bug——综合后的网表也有同样的bug——Formality报告pass。

误区三：Formality跑一次就够了。 每次ECO/每次CTS/每次DFT插入后都要重跑等价性检查。Formality是CI流程的一环——每次网表变更自动触发。

版本演进

- 1990s：Formality诞生：BDD-based等价性检查。最先验证RTL=Gate。 - 2000s：时序等价：支持pipeline retiming和状态重编码后的等价性证明。 - 2010s：低功耗等价：支持UPF/CPF电源管理单元的等价性检查。增量ECO验证。 - 2020s：AI辅助：ML预测等价性检查fail的可能的根因——加速debug。形式+仿真融合。