中文 英语
知识中心
导航
知识中心

验证

受欢迎程度

描述

功能验证

创建一个新设计的成本很大——非常大。虽然在芯片设计的早期,有可能第一次就把它做好,但设计的规模和复杂性很快就会增长到工程师很可能会犯一些错误的地步。为了找到这些错误,我们必须实践设计,看看它是否以正确的方式做出反应。这是一种验证行为。当发现问题时,我们将进入调试阶段,在此阶段我们将了解导致问题的原因并决定如何修复设计。然后我们回到验证,直到我们获得足够的信心,认为设计中没有任何错误。今天,系统的复杂性是如此之大,以至于不可能执行设计的所有方面,因此我们必须在执行的验证中非常有选择性。在今天,用于验证的时间、人力和费用比实际设计本身更多,这并不罕见,即使有这么大的支出,大多数设计在最初制作时仍然存在几个漏洞。运气好的话,这些漏洞并没有完全阻止设计工作,并且可以找到解决方案,从而使产品的第一个版本成为可能。

在核查的早期,事情是非正式的。它通常包括练习一个模型并观察产生的波形。设计师将决定他们的想法是否正确,如果正确,就进行下一个实验。这已经不可能了,因为测试的数量太多了,而且很难重新进行实验,看看是否有什么变化。今天,核查已经变得更加结构化。

从根本上说,验证就是两个模型的比较。这种观点认为,如果这两个模型是彼此独立推导出来的,而且它们在功能上是匹配的,那么它们很有可能都是正确的。独立是什么意思呢?我们假设两个不同的人分别阅读了一个规范并编写了他们的模型,而没有直接相互讨论。这两个人通常来自设计团队和验证团队。

为什么不“直接讨论”就应该编写模型呢?如果规范存在问题——定义方式的模糊性,那么您希望在验证过程中使该问题变得明显。您不希望他们每个人编写模型的方式受到讨论的影响,除非它直接导致规范的澄清。如果他们在规范中发现了问题,就讨论这个问题并修正规范,以消除歧义。没关系。事实上,这本身就是一种验证行为。这是对规范的非正式回顾。

比较模型有两种主要方法,通常称为静态验证方法和动态验证方法。

动态验证是最常见的,它利用模拟器、仿真器或原型。这些方法通过将样本数据发送到模型中并检查输出以查看模型的功能来练习模型。如果我们发送足够多的输入数据,那么模型总是做正确事情的信心就会增加。输入数据流(通常称为刺激)的构造方式是将模型带入代码的各个不同部分,我们可以比较两个模型之间的输出数据(通常称为响应)。当发现差异时,这要么意味着设计模型不正确,验证模型不正确,要么就像我们已经暗示的那样——规范有问题。发送到模型中的每一组数据都被称为一个测试。两个模型之间的比较是由检查人员完成的。刺激可以构建为将设计带入特定的功能区域,通常称为定向测试,或者可以基于随机数据流。现在我们不只是发送任何随机数据-这不太可能完全测试模型,相反,它是受控随机化,通常被称为伪随机、约束随机或定向随机测试。

静态验证,通常称为形式验证,是一种数学证明,证明两个模型在所有条件下是相同的。没有刺激是必要的,因为所有可能的刺激都被考虑在内。第二个模型(验证模型)通常以一种不同的方式构造,使用所谓的属性。属性定义了设计必须展示的行为。或者,它可以定义一些永远不会发生的事情。

两种核查方法都需要的另一种描述是一组限制核查的限制条件,将核查限制在一组合法的状态、投入或活动。

验证是一种以最有效的方式最大限度地提高设计质量的尝试,而验证的方式对每个公司来说都是不同的,有时对每个产品来说也是不同的。例如,与可植入的医疗设备相比,廉价儿童玩具的质量水平较低。这意味着没有一种正确的方法来进行验证,许多人把它称为艺术而不是科学。

形式验证

有几种类型的形式化方法用于验证设计。
首先是等价性检验。这需要两个设计,它们可能处于相同或不同的抽象级别,并找到它们之间的功能差异。等价性检查可以进一步分解为两个主要领域——组合等价性检查,通常被称为等价性检查,和顺序等价性检查。

通过组合等价性检验,证明逻辑综合后的设计与输入RTL描述一致。它还用于显示当进行测试逻辑或其他门级转换时,没有功能受到影响。它比较了原始描述中对应寄存器之间的组合逻辑。

顺序等价性检查是一项新兴技术,它可以采用两个具有根本不同时间的设计,使一个未计时或部分计时的模型与一个RTL模型进行比较,或者在经过重新计时或其他转换以提高功率或其他设计质量的RTL模型之间进行比较。这是大规模采用高水平合成的必要技术。

形式验证的另一个主要分支是属性检查。属性定义了必须在设计中出现的行为,或者必须不可能出现的行为。第三种选择被称为公平条件,它将确保几个选项中的每一个都不会受到不公平的对待,例如在仲裁中。

在某些情况下,可能很难证明一个性质,而不是提供一个完整的证明,有限的证明是所有可能的。一个有界的证明可能会说,该行为是,或不是,在一个定义的时钟数量内,或从一个特定的开始状态,或当某些约束应用到系统时。

多媒体

什么时候使用哪个验证引擎

多媒体

正式验收

多媒体

异构计算验证

多媒体

正式数据路径验证

多媒体

计划外验证

Baidu