3、Formality基础概念：Reference Design与Implementation Design、逻辑锥、等价性检查原理
好，咱们今天聊聊Formality最核心的几个概念。说实话，我刚接触Formality那会儿，也被这些术语搞得有点晕。什么Reference Design、Implementation Design，听着就像绕口令。但搞懂了这些，你就能明白形式验证到底在干什么。
3.1 Reference Design与Implementation Design
这两个概念，说白了就是“标准答案”和“你的答卷”。
Reference Design（参考设计），我习惯叫它“黄金模型”。它通常是你认为功能完全正确的那个版本。比如RTL代码刚写完，仿真都通过了，这时候的RTL就是Reference。或者综合后的网表，如果你要验证它和RTL是否一致，那RTL就是Reference。
Implementation Design（实现设计），就是你要验证的那个设计。它可能是综合后的门级网表，也可能是做了扫描链插入、时钟树综合之后的版本。你心里没底，想知道它和Reference是不是功能等价。
关键点：Formality会逐点比较两个设计的每一个寄存器、每一个输出端口。如果所有可比点上的逻辑值都一致，那就证明两个设计功能等价。
我在项目中遇到过一种情况：综合后的网表功能仿真全过，但Formality跑出来一堆不匹配。后来发现是综合脚本里有个约束写错了，导致某个模块被优化掉了。你看，仿真过了不代表没问题，形式验证就是来补这个缺的。
3.2 逻辑锥
逻辑锥这个概念，嗯，其实挺形象的。你想想看，一个寄存器的输入，是由一堆组合逻辑和前面的寄存器共同决定的。这些逻辑从输入端口或寄存器开始，像锥子一样汇聚到目标寄存器。这就是逻辑锥。
Formality在比较两个设计时，不是傻乎乎地全芯片一起比。它会先找出所有可比点，然后针对每个可比点，分别构建它在Reference和Implementation中的逻辑锥。再比较这两个逻辑锥是否等价。
我的经验：逻辑锥的大小直接影响验证效率。如果某个逻辑锥特别大，比如包含了整个乘法器或复杂的状态机，Formality跑起来就会很慢。我曾经遇到一个设计，某个寄存器的逻辑锥里竟然有上万条路径，跑了一整天都没出结果。后来我们做了些优化，把大模块拆开验证，效率就上来了。
逻辑锥的边界是什么？就是那些可比点。可比点包括：
- 所有寄存器（D触发器的输出端）
- 所有顶层输入端口
- 所有顶层输出端口
- 黑盒子的边界
Formality会从这些可比点出发，反向追踪组合逻辑，直到遇到另一个可比点为止。这样形成的逻辑锥，就是它要比较的基本单元。
3.3 等价性检查原理
等价性检查的原理，说白了就是“数学证明”。Formality会把两个设计都转换成一种叫“规范形式”的布尔表达式，然后比较这些表达式是否完全一致。
具体来说，它用了两种核心技术：
- BDD（二叉决策图）：把布尔函数表示成一种有向无环图。如果两个函数的BDD结构完全一样，那它们就等价。
- SAT（布尔可满足性）：把等价性问题转换成SAT问题。如果找不到任何一组输入能让两个逻辑锥的输出不同，那就证明它们等价。
Formality会先用一些启发式算法快速判断，比如随机仿真、结构匹配。如果这些方法搞不定，才会调用BDD或SAT引擎做深度证明。
注意：等价性检查不是万能的。它只能证明两个设计在逻辑功能上等价，但无法验证时序、功耗、面积这些物理特性。我曾经见过一个案例，RTL和网表在Formality上完全等价，但流片回来芯片就是跑不到目标频率。后来发现是综合时某个路径的时序约束没写对，导致关键路径延迟超标。所以形式验证和静态时序分析要配合使用，缺一不可。
还有一个容易忽略的点：等价性检查的前提是两个设计有相同的可比点。如果综合过程中把某些寄存器合并了、删除了，或者插入了新的测试寄存器，那可比点就对不上了。这时候需要告诉Formality哪些寄存器是“不匹配”的，让它跳过这些点的比较。
我个人习惯的做法是：先跑一次“自动匹配”，看看Formality能自动找到多少可比点。如果匹配率低于95%，那就得手动检查了。通常问题出在：
- 综合时插入了扫描链，多了很多测试寄存器
- 时钟门控引入了新的锁存器
- 某些寄存器被优化掉了（比如常数寄存器）
遇到这些情况，别慌。Formality提供了set_verification_compare_points和set_verification_clock_gate_hold这些命令，可以帮你处理这些“不匹配”的点。
最后说一句：等价性检查是个好工具，但它不是银弹。你想想看，如果Reference Design本身就有bug，那验证通过又有什么意义？所以，保证Reference Design的正确性，才是形式验证的第一步。