格林定理的数字版本及其在形式验证中的覆盖问题的应用
摘要：一种新的方案解决覆盖问题，引入了一种量化评估块与其环境交互的方法。通过设置适用于基于模型检测的集成电路验证的Green定理的离散版本，实现这一目标。该方法最适合解决覆盖问题，因为它能够量化描述模型的一组规则的不完整性或冗余性。此外，该方法可以在整个验证过程中连续进行，从而使用户能够确定不完整性/冗余性发生的阶段。尽管该方法是基于一个小型硬件示例进行演示，我们还展示了它在大型系统中提供精确覆盖估计的可能性。我们通过在相同的测试用例上进行检查，将该方法与其他方法进行了比较。
作者：Eli Appleboim, Emil Saucan
论文ID：cs/0309008
分类：Symbolic Computation
分类简称：cs.SC
提交时间：2007-05-23