一种结合依赖关系消除误判的等价性验证方法

摘要

本发明涉及一种结合依赖关系消除误判的等价性验证方法，属于模型验证技术领域。在验证等价性的两个电路中，引入新变量代替候选等价点后得到两电路不等价，此时新引入的变量扩大了原候选等价点的取值范围，可能发生误判。为消除误判，本方法首先对所有候选等价点依据电路结构信息计算其对应的拓扑关系。分析候选等价点对应的拓扑关系是否存在依赖关系：如不存在依赖关系，则不存在误判，即原电路不等价；若候选等价点间如存在依赖关系，则将候选等价点对应的子电路还原，进一步调用约束求解器求解。如果得到可满足的结果，则两电路是不等价的；如不可满足，则发生了误判现象，即两电路是等价的。本发明提高了等价性验证效率和芯片的首次硅片成功率，加快电子产品上市时间。

主权项

一种结合依赖关系消除误判的等价性验证方法，其特征在于：至少包括如下步骤：步骤1：对所有候选等价点依据电路结构信息计算其对应的拓扑关系；步骤2：分析候选等价点对应的拓扑关系是否存在依赖关系；步骤3：判断是否存在误判：如果候选等价结点间不存在依赖关系，则验证结果为等价，不存在误判，转步骤5；如果候选等价结点间存在依赖关系，则此时并不能得到两模型不等价，即可能存在误判现象；步骤4：结合依赖关系消除误判；步骤5：输出等价性验证结果，等价性验证结束。