深层解析形式验证

Y轴越往上走，被高层要求覆盖的设计空间就越大。证实这些高层要求具有很高价值，原因有很多：

　　1. 高层要求关系到微架构中的要求

　　2. 高层要求关系到测试平台中的输出检查器组

　　3. 高层要求覆盖了与工程师想要写入的数百条较低层断言相同的设计空间

　　4. 高层要求覆盖了由于工程师遗漏的较低层断言的缺失而未被覆盖的设计空间

　　最后一点我们这里举个例子，假如设计包含一个FIFO，并且工程师忘了编写一个断言来检查FIF从不下溢。这种安全性违例将由高层要求加以识别。然而，通过形式性地验证高层要求，高层要求违例的根源就能得以跟踪。例如，如果针对高层要求在影响锥中包含了FIFO，那么导致高层要求不能满足的下溢条件将被检测到。

　　理想的形式验证工具要求具有一定的规模，以便穷尽地检查所有可能的输入条件以及设计中任意点的可控性和可视性(见表1)。我们的旗舰产品，例如JasperGold，就采用了高性能和大规模的形式验证技术，能够穷尽地验证模块是否满足源自微架构的高层要求。这款产品使用数学算法，因为不需要使用仿真测试平台或激励。

　　表1：仿真与形式验证的比较

　　本文小结

　　形式验证要求你以不同的方式思考。例如，仿真是完全经验主义的做法，也就是说，你通过反复试验试图查明缺陷，这要花相当多的时间尝试所有可能的组合，因此永远不会完整。另外，由于工程师必须定义和产生大量输入条件，他们的工作重点将是如何在非设计目标基础上分解设计。另一方面，形式验证是穷尽式数学技术，允许工程师仅关注设计意图，或“什么是设计的正确行为?”。

　　验证实现工作包括将多种输入条件定义为测试计划的一部分、创建功能覆盖模型、开发测试平台、创建输入激励发生器、编写指导性测试以及执行测试、分析覆盖率指标、调整激励发生器以面向未验证的设计部分，然后反复这一过程。纯形式验证技术则相反，专注于证实模块的端到端、直接对应微架构规范的高层要求，帮助用户戏极大提高项目的设计和验证产能，同时确保正确性。