Formal验证不是“黑魔法”

相比EDA仿真，Formal做的事情不是那么直观。当你测试一个场景时，EDA仿真会展示给你所有仿真周期的设计状态，但是Formal工具可能只会展示极少的周期行为。

如果你不信，可以了解下Formal的核心算法，既提高对工具的信心，还可以在执行Formal验证遇到问题时更快地提出解决方案。

首先从一个小例子开始，展示如何使用一个更“聪明”的数据结构将一个复杂的问题转换为更易于处理的问题。

布尔逻辑通常通过真值表来表示，该表根据系统的每个输入对应的期望输出。下面的真值表描述了一个1位的ADD操作。

随着输入个数的增加，真值表的大小会迅速增长：每添加一个输入列，输出的行数增加一倍。

 MUX操作输出需要的行数是ADD的两倍。

为了记录可能的输入，我们需要6 bit：

1 bit记录输入了多少25元，

2 bit记录输入了多少10元，

3 bit记录输入了多少5元。

要写出一个完整的真值表，我们将需要64行（2^6行），但只有6行将产生结果1。

Formal工具通过算法和数据结构的巧妙选择，将一个指数级的真值表转化为更加紧凑的真值表处理。

为了验证设计，我们需要比较两种规格：

设计规格通常比实现细节更抽象，规格通常是一组属性，如SystemVerilog断言、RTL模型或像SystemC这样的高级语言模型。实现通常将是一个更详细的RTL模型或门级网表。

在某些情况下，两个模型之间抽象层次一样，例如ECO中的等价性比对。

在上图中，方框A和方框B表示接收相同输入的模型，并通过checker对其输出进行比较。然后，checker确认A和B产生等价的结果。如果checker发现了导致比对失败的输入序列，则可以提供一个反例用于定位。上述是一个黑盒验证模型，因为checker不观察A和B内部的状态。虽然黑盒验证的可见性较低，但它不受内部变化的影响，这使得验证环境的维护成本比较低。

当然，更重要的是

如果A和B足够简单，可以测试所有可能的序列。对于下面的图，其中A和B是一个更大的系统组件。

在这个例子中，如果我们已经证明了A和B是等价的，那么我们就可以删除A和B，只需要证明一个更简单的问题，即证明C和D是等价的。通过使用分而治之的策略，我们通常可以使用FV工具验证规模更大的设计。

如果一个设计包括加法和乘法模块，则可以使用不同的引擎来验证不同的操作。通常，EDA仿真不这样做，因为建议一个统一的验证环境更加高效。而FV工具只会分析要验证的属性（规格），剔除对属性结果没有影响的其他逻辑。

如上图所示，有几个框可以从设计中删除，因为它们在所验规格结果的计算中没有起到任何作用。在大型设计中，这将大大减少所需要考虑的逻辑的数量。