过度约束正式的财产验证（FPV）会有什么影响

正式性能验证（FPV）越来越多地用于补充片上系统（SoC）验证的仿真。将FPV添加到您的验证流程可以大大加快验证关闭并发现棘手的案例错误，但了解这些技术之间的差异非常重要。主要区别在于FPV使用属性，即断言和约束，而不是测试平台。断言也用于模拟，但约束的作用是不同的。理解约束对于成功使用FPV是必要的。

约束

约束游戏在FPV中发挥核心作用。它们定义了对被测设计的法律刺激，即可以达到的状态空间。断言定义了DUT对法律激励的期望行为。

约束描述了如何允许DUT的输入表现，应该采用什么值以及输入之间的时间关系。约束可以被认为是模拟中的刺激。在约束随机模拟中，约束求解器为下一个周期生成满足所有约束的输入向量。它将继续在刺激周期之后产生循环直到模拟结束，或直到它达到无法产生法律刺激的情况。

相比之下，形式验证的约束可以描述，例如，如何在给定的协议中合法沟通。

过度和不足约束

编写精确描述所有法律刺激的约束很难并且通常是不可取的。这意味着正式环境要么不受约束，要么过度约束。约束不足意味着对精确建模刺激所需的约束要少。这意味着一些潜在的非法输入将被驱动到被测设备（DUT）。过度约束意味着存在比所需更多的约束，并且不允许所有合法行为。

略微受限制的环境通常是最好的方法。许多设计可以处理规范中未定义的输入和行为，如果使用的约束更少，则将验证设计中更大的状态空间。约束不足的环境可能会导致断言失败，如果是这种情况，则需要添加其他约束。例如，假设我们有一个4位乘法器来验证：

规范说它可以乘以正整数A和B> 0，但是验证工程师假定A和B> = 0.约束和检查乘数的断言很简单：

如果在这种情况下证明了该属性 - 对于A和B中的任何一个或两个都为零以及正整数 - 那么显然它将保持A和B仅大于零。约束允许其他行为，这意味着环境受到限制。较少的约束通常也会改善正式工具的运行时间。如果属性通过，我们不必再担心欠约束情况了。

过度约束正式环境是一个更大的问题，因为它可能隐藏设计中的错误。实际上，您没有像您认为的那样进行验证。例如，假设乘数可以乘以正数和负数，但验证工程师误解了规范并写入约束以将A和B限制为> = 0.假设乘数有效，则上面的属性将通过，并且您认为验证已完成，因为所有属性都已通过。

过度约束只是无意中的问题。故意过度约束是将设计验证分解为案例的有用方法。一个例子是验证存储器控制器。首先限制刺激只做写事务，然后限制它只做读事务。这些情况中的每一种都明显过度约束。

在第一种情况下，不允许读取合法事务的事务，在第二种情况下，不允许写入事务。这不是问题，因为这两个案例共同涵盖了所有法律刺激。在这种情况下，只有一个案例被行使而不是另一个案例，导致验证工程师认为已经完成了验证。故意过度约束的风险是错过了合法的输入值，并且未验证诸如读取后写入的序列（在存储器控制器的情况下）。

冲突约束

约束限制了在正式属性验证中探索的输入集和状态空间。如果验证环境具有相互冲突的约束或设计中的语句，则不可能有合法的输入，并且设计中的任何状态空间都不可访问。例如，下面的两个约束可以单独满足，但它们一起产生冲突：

相等：假设属性

冲突约束可以被视为过度约束环境的最极端形式，受到如此限制没有合法的投入。这意味着没有断言可以失败，实际上是因为没有进行检查。这类似于说我的测试用例没有在模拟中失败，原因是你没有执行任何测试用例。该陈述是正确的，但它在验证完整性方面具有误导性。