【日更计划120】数字IC基础题【UVM部分】

上期答案

[326] 形式验证是静态仿真还是动态仿真？

是静态仿真

[327] 形式验证有哪些方法？

1. 模型检查
2. 形式等效

[328] 解释模型检查

在“模型检查”方法中，将要验证的模型描述为从设计规范中提取的一组property。 因此要详尽搜索设计的状态空间，检查所有property是否在所有状态下均成立。 如果在任何状态下违反了property，则会引发错误。 下图是一个示意图：

[329] 什么是形式等效

形式等效用于验证两个具有相同或不同抽象的模型在功能上是否一致的方法。 此方法无法确定模型在功能上是否正确，但是可以确定两个模型在功能上是否相同。 常用于比较RTL设计和综合网表的功能。 它也可以用来检查两个RTL模型或两个门级模型的一致性。 下图是一个示意图：

[330] 列出一些可以使用形式等效的场景

1. RTL设计与综合网表
2. RTL设计与参考模型
3. 两个RTL设计
4. 两个门级模型
5. 两个参考模型

[325] 什么是形式验证？

形式验证是使用数学建模来验证设计实现是否符合spec的方法。 形式验证使用数学推理和算法来证明设计符合spec。 在形式验证中，该工具隐式地涵盖了所有情况（输入和状态），而无需开发任何激励生成器或预期输出。 该工具需要以property或更高级别的模型形式对spec进行形式描述，以详尽地涵盖所有输入组合，证明功能的正确性。 SystemVerilog的property也可用于形式化描述spec。

本期题目

[331] 与动态仿真相比，形式验证有什么优势？

[332] 形式验证有什么局限性？

[333] 如果设计中的某个模块经过形式验证可以正常工作，我们是否还需要收集该模块的覆盖率？

[334] CMOS电路功耗由哪些部分组成？

[335] 什么是动态功耗？它与哪些参数有关？

正确答案将在下一期公布，或者到下面的文章获取答案