形式化芯片验证:救世主还是乌托邦
以下内容节选自 微信公众号 老石谈芯与传统的基于仿真的验证方法相比,形式化验证有着本质性的不同。形式化验证方法拥有很多特殊的优点,能够在理论上完全克服传统验证方法的缺陷和不足。总结说来,形式化验证的优点主要体现在下三个方面。
第一,形式化验证能覆盖完整的设计状态空间。
与其他所有基于仿真的验证方法相比,这一点是形式化方法最大的优势所在。通常来讲,一个数字电路的设计通常由若干个逻辑状态空间(logic state space)组成,这其中可以包含以下几类状态:
电路复位后的初始化状态, 也称为复位状态;
内部逻辑实现时的中间状态;
各个输入输出的状态。
第二,形式化验证能提供最小实例。
形式化验证的第二个主要优点在于能迅速提供一个最小实例,如下图所示。这里“最小实例”指的是,达到一个目标状态所需要的必要条件,包括各个输入值、寄存器的状态,以及达到目标状态需要的最少周期数等。
第三,形式化验证能提供“基于状态”或“基于输出”的分析和调试方法。
如上文所述,传统的电路仿真都是基于输入的方法,即给出输入后才能观察内部状态以及电路输出。然而,形式化验证并不依赖任何输入,因此可以做到“基于状态”或者“基于输出”,并以此进行设计分析和调试。
例如,在基于状态的方法中,我们希望知道在一个设计中是否能够通过某种方式达到某种状态(如前文中所述),或者更进一步,希望将此状态作为接下来分析和调试的起始状态。 :lol
页:
[1]