形式测试(formal verification) 又分为两类：
等效测试(Equivalence Checking) 和模型测试(Model Checking)。
等效测试 (Equivalence Checking )
Equivalence checking compares two models(使用LEC或Formality)
1. 比较两个netlist，以确保扫描链的插入，时间树的综合，以及人
为修改等，不会改变电路的功能
2. It can detect bugs in the synthesis software
• 验证网表是否正确实现了原来 RTL代码的功能。
• 等效测试可以用来检验合成工具的可靠性。在少数场合，等量测试
可以检验手写RTL代码是否实现了门级设计要求。
• 等效测试可以证明两种RTL编码在逻辑上等价。为了获得更好的合成效果，
对源代码作了一些小的修改，而又不影响其功能，就可以通过证明等价而避
免繁琐的模拟。
3. Equivalence checking found a bug in an arithmetic operator
可以用較少的時間來找出錯誤點
模型测试Model Checking (Assertion 如SVA)
模型测试技术是形式测试技术的最新发展成果，采用这种技
术可以检验一种设计的断言和特征。比方说，设计中的所有状态
机可以独立检测。还有一种功能更为强大的测试可以预测是否会
发生死锁。
另外一种可以进行形式测试的断言跟接口有关。首先用形式
描述语言来描述接口，然后用工具来检测它。例如，一个断言可
能会作如下定义，一旦产生了ALE信号，就会随之产生DTACK或
ABORT信号。
模型测试技术困难之处在于利用对设计要求所作的说明，来鉴别所要检测的
断言。
在所有的断言中，只有一个子集可以进行检测。现有技术不能检测高级断
言，因此也不能保证能正确实现其复杂功能。
一种理想的情况是，在特定的寄存器状态下，异步传输（ATM）信元以相关
顺序输出。但模型测试技术不能做到这一点。(SVA 可測Async-fifo)
功能测试 (Functional Verification )
功能测试的主要目地是确保设计能实现预期功能。功能测
试就是为了使设计符合其所要
• 除非设计要求以精确的语法诉诸于正规的语言，否则无法证明设计
是否符合要求。
• 描述设计要求的文件是由人用自然语言写成的，而各人正确表达自
己意思的能力又各不相同，人们可以对同一文件作出不同的解释。
• 功能测试能够显示设计是否符合要求，但无法完全证明这一点。
• 我们可以因为一点小小的不一致就说设计没有实现预期功能，反之
则不然：没有人能证明它完全一致。
為了應對以上的測試
我們需要建立测试平台(Testbench Generation )
• 测试平台生成程序：按照代码覆盖规律，或利用某些经过证明的
结果，对源代码进行分析。
• 生成测试平台，可以用来增加代码覆盖，或检验设计方案的某些
性质。
测试平台生成程序局限及用途
—Designer input is still required.
—The jury is still out on the usefulness at these tools.
测试对象通常都是RTL代码，没有重重会聚点。测试人员要判
断测试平台所给的激发信号是否有效，如果有效，则要知道预期的
输出结果，并把它和设计的输出比较
模型测试产生的测试平台不仅能用来描述某项特性可能不符
合要求，或者什么样的输入顺序可能引起错误。而且可以用来检
测到设计要求中没有考虑到的非正常状态，或者为解决问题提供
调试环境。
沒有留言:
張貼留言