无论是在芯片测试还是在系统研发的过程中，工程师都需要进行严谨的形式验证。通过这一方式可以及时找出错误节点，对系统优化具有重要作用。然而，如何才能真正的让形式验证成为自己研发工作的重要助力？为什么平时的工作中验证过程就如同走流程一般枯燥？本文将会通过两个方面的介绍，帮助你找到合理利用形式验证的秘诀。
有界结果和无界结果具有同等意义
大多数情况下，当检验器没有达到决定性结果的时候，验证工程师会问我们该怎么办。一个形式工具，可以返回三种不同的状态：Pass代表运行正常。Fail意味着形式工具发现了故障，用户可以根据所提供的反例进行调试。这两个都是决定性的结果。第三类的名称根据所使用的形式工具不同而有所区别——探索，未确定，尚无定论，或终止。听起来好像都是不好的结果，但这些结果都是有意义的。
这类的结果表示需要的周期比所记录的证明约束的周期短的话，形式工具无法找到这样的错误。如果工具返回并记录到一个20个周期的有界证明的不确定状态，则用户知道在小于20周期的设计中没有错误。
形式验证的重要一步，是证明对于给定DUT所要求的证明深度是合格的。有一个明确的方法来跟踪计算所需的证明界限。一旦用户计算所需的证明深度，那么所有不确定的结果被分成两组。首先检验器达到所需的证明深度。另一种是检验器还没有达到所需的深度证明。例如，所需的证明深度是30，但在形式工具的分析中只达到了20个周期。在这一点上，用户会寻找可以用来达到所要求的证明深度的技术。大多数情况下，有一些可用的方法，比如使用抽象模型。
如果检验器达到所需的证明深处，有界结果和无界结果一样好。如果用户没有得到无界证明，这并不意味着其结果是没有意义的。
实现形式符号指令需要一个合理的方法
形式符号指令意味着形式化技术被给予了与验证流程中模拟相同的权重。在形式是唯一用于验证DUT的技术的模块中，形式工程师与设计和验证工程师被赋予了同等的责任和义务，以确保在设计中没有错误。
为了实现形式符号指令，我们需要一个合理的方法。这意味着形式化测试平台需要所有的端对端检验器覆盖完整的设计功能。约束必须有效，而不会过度约束。抽象模型和其他复杂的解决方法都可能会用到，以确保所有检验器达到所要求的证明深度。形式覆盖将被要求用于证明形式验证结果。缺乏的任何一部分都会使形式验证工作不完整，不能够实现符号指令。
在采用形式符号指令项目之前，形式工程师应该了解如何才能实现形式符号指令。要掌握实现方法必须牢记四个C跳—检验器（checkers）、约束（constraints）、复杂度（complexity）以及覆盖（coverage）。
结语
工程师通过对符号指令的合理设置以及对有界结果、无界结果的分析利用，能够顺利的通过形式验证发现系统设计中的缺陷和有待改进之处，从而能够让形式验证真正成为自己研发过程中的有力帮手。
