Formality形式验证和SAT算法

以下文章来源于志芯，作者JackXu

Formality 是一种广泛应用于芯片设计的形式验证工具，主要用于验证不同设计阶段的网表的逻辑等价性。

Formality 形式验证流程

导入设计文件。Reference Design（参考设计）：读入 RTL 设计文件，通常是 Verilog 或 SystemVerilog 文件。Implementation Design（实现设计）：读入综合后的门级网表或布局布线后的网表。库文件：读入相关的库文件，如工艺库。

设置约束。设置路径约束，例如某些路径只走某1端，或者某些引脚在不同设计阶段的值。设置其他验证约束，如时钟域交叉等。

匹配（Match）： 将 Reference Design 和 Implementation Design 中的逻辑锥（Logic Cones）和比较点（Compare Points）进行匹配。匹配过程会尝试将两个设计中的逻辑结构对齐，以便后续的验证。

验证（Verify）。Formality 使用多种算法来验证两个设计的逻辑等价性。对于每个比较点，验证算法会检查两个设计的输出是否一致。

Formality 形式验证的基本比较单元

Formality 将设计分解为逻辑锥和比较点。逻辑锥是从输入到输出的一组逻辑门，比较点是逻辑锥的输出点。通过比较点的输出结果来验证两个设计的逻辑等价性。

SAT 算法

Formality 内部使用 Boolean Satisfiability Problem（布尔可满足性问题，简称SAT）求解器来验证逻辑等价性。SAT 求解器通过布尔可满足性问题的求解来判断两个设计是否等价。SAT 求解器会尝试找到满足两个设计输出相等的变量赋值组合。SAT是计算复杂性理论中的一个经典问题，也是计算机科学中的一个重要研究领域。

在芯片设计中，设计人员会按照特定规范在设计中加入相关属性描述。SAT算法可以用于检查这些属性是否在电路的整个运作流程中都能满足。例如，通过将电路设计中的信号转换为布尔表达式，利用SAT求解器检查是否存在满足这些表达式的变量组合，从而验证电路的正确性。

在芯片设计的不同阶段，如逻辑综合、布局布线等，需要验证不同版本的电路设计是否逻辑等价。SAT算法可以用于检查两个电路设计是否在所有可能的输入下产生相同的输出。通过将两个电路的逻辑表达式转化为布尔公式，并利用SAT求解器检查是否存在使两个公式不等价的输入组合，从而验证电路的逻辑等价性。

SAT问题通常根据布尔表达式的结构进行分类。CNF（Conjunctive Normal Form，合取范式）：布尔表达式是若干个子句的合取（AND），每个子句是若干个文字的析取（OR）。文字是变量或其否定。DNF（Disjunctive Normal Form，析取范式）：布尔表达式是若干个子项的析取（OR），每个子项是若干个文字的合取（AND）。

SAT问题是一个NP完全问题，这意味着目前没有已知的多项式时间算法可以解决所有类型的SAT问题。然而，对于特定的SAT问题，如3-SAT（每个子句恰好有3个文字的CNF），已经有许多高效的启发式算法。

“Nondeterministic Polynomial Time”（非确定性多项式时间）通常简称为“NP”。它是计算复杂性理论中的一个重要概念，用来描述一类计算问题的特性。NP问题：如果对于一个判定问题（即答案只有“是”或“否”的问题），存在一个多项式时间的验证算法，那么这个问题就属于NP问题。也就是说，对于一个可能的解，我们可以在多项式时间内验证它是否是正确的解。多项式时间：多项式时间是指算法的运行时间与输入规模的关系是多项式函数。例如，如果输入规模为n，算法的运行时间是n²、n³或n⁴等，那么这个算法就是多项式时间算法。P问题：P（Polynomial Time）问题是指可以在多项式时间内解决的判定问题。P与NP的关系：P是NP的子集，即所有P问题都是NP问题，因为如果一个问题可以在多项式时间内解决，那么它的解也一定可以在多项式时间内验证。但是，是否所有NP问题都是P问题，即P是否等于NP，这是计算机科学中一个未解决的重大问题，也是千禧年七大数学难题之一。NP完全问题（NPC）：如果一个NP问题满足以下两个条件，那么它就是NP完全问题；（1）它是一个NP问题；（2）所有其他NP问题都可以在多项式时间内归约到它。归约是指将一个问题转换为另一个问题，如果一个问题A可以归约到问题B，那么解决B的方法也可以用来解决A；NP完全问题在计算复杂性理论中具有重要意义。如果能够找到一个多项式时间算法来解决任何一个NP完全问题，那么所有NP问题都可以在多项式时间内解决，从而证明P=NP。反之，如果能够证明任何一个NP完全问题不能在多项式时间内解决，那么P≠NP；旅行商问题（TSP）、背包问题、布尔可满足性问题（SAT）等都是著名的NP完全问题。

SAT问题第一个被证明是NP完全的问题。给定一个布尔表达式，它包含多个布尔变量（可以取值为真或假）和逻辑运算符（如与、或、非）。问题是判断是否存在一种变量的赋值方式，使得整个布尔表达式的值为真。例如，对于布尔表达式（A∧B）∨（￢A∧C），可以通过尝试不同的A、B、C的值来判断是否存在一种赋值使表达式为真。对于简单的布尔表达式，可以通过穷举变量赋值来解决。但对于复杂的布尔表达式，变量数量很多时，穷举的方法会非常耗时。然而，给定一个变量赋值，我们可以快速验证这个赋值是否使布尔表达式为真。并且很多其他问题可以归约到SAT问题，它也是NP完全的。

以下是一些常见的SAT求解算法。

SAT算法原理中的DPLL算法（Davis-Putnam-Logemann-Loveland）。DPLL算法是一种经典的SAT求解算法，基于回溯搜索。其基本思想是通过递归地分配变量值，并利用布尔约束传播（Boolean Constraint Propagation, BCP）来简化问题，直到找到一个满足的赋值或证明无解。

SAT算法原理中的 CDCL算法（Conflict-Driven Clause Learning）。CDCL算法是DPLL算法的改进版本，它在DPLL的基础上引入了冲突驱动的子句学习机制。当检测到冲突时，CDCL算法不仅会回溯，还会学习一个新的子句，以避免在未来的搜索中再次遇到类似的冲突。