形式化芯片验证：救世主还是乌托邦

以下内容节选自 微信公众号 老石谈芯





与传统的基于仿真的验证方法相比，形式化验证有着本质性的不同。形式化验证方法拥有很多特殊的优点，能够在理论上完全克服传统验证方法的缺陷和不足。总结说来，形式化验证的优点主要体现在下三个方面。


第一，形式化验证能覆盖完整的设计状态空间。


与其他所有基于仿真的验证方法相比，这一点是形式化方法最大的优势所在。通常来讲，一个数字电路的设计通常由若干个逻辑状态空间（logic state space）组成，这其中可以包含以下几类状态：

[li]
电路复位后的初始化状态， 也称为复位状态；[/li][li]
内部逻辑实现时的中间状态；[/li][li]
各个输入输出的状态。[/li]

第二，形式化验证能提供最小实例。

形式化验证的第二个主要优点在于能迅速提供一个最小实例，如下图所示。这里“最小实例”指的是，达到一个目标状态所需要的必要条件，包括各个输入值、寄存器的状态，以及达到目标状态需要的最少周期数等。

第三，形式化验证能提供“基于状态”或“基于输出”的分析和调试方法。

如上文所述，传统的电路仿真都是基于输入的方法，即给出输入后才能观察内部状态以及电路输出。然而，形式化验证并不依赖任何输入，因此可以做到“基于状态”或者“基于输出”，并以此进行设计分析和调试。

例如，在基于状态的方法中，我们希望知道在一个设计中是否能够通过某种方式达到某种状态（如前文中所述），或者更进一步，希望将此状态作为接下来分析和调试的起始状态。