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

摘要

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

主权项

一种结合依赖关系消除误判的等价性验证方法，其特征在于：至少包括如下步骤：步骤1：对所有候选等价点依据电路结构信息计算其对应的拓扑关系；拓扑关系计算方法为：按照电路从原始输入到原始输出的结构拓扑顺序递推计算电路中候选等价点所使用的原始输入的集合，记录候选等价点和其相应的拓扑关系；在递推计算候选等价点的拓扑信息时，如当前候选等价点对应的拓扑关系使用已经计算过的候选等价点，则可得到两候选等价点存在依赖关系；步骤2：分析候选等价点对应的拓扑关系是否存在依赖关系；步骤3：判断是否存在误判：如果候选等价结点间不存在依赖关系，则验证结果为等价，不存在误判，转步骤5；如果候选等价结点间存在依赖关系，则此时并不能得到两模型不等价，即可能存在误判现象；所述的分析候选等价点是否存在依赖关系的方法按以下步骤进行：1)：按电路的从输入到输出的拓扑顺序，对候选等价点和电路其它元件的拓扑关系进行分析，如共用相同的原始输入则候选等价点和电路存在依赖关系；2)：按顺序对候选等价点对应的拓扑关系进行分析，如两候选等价点共用相同的原始输入则两候选等价点间存在依赖关系；3)：记录存在依赖关系的候选等价点和其相应的拓扑关系；步骤4：结合依赖关系消除误判；所述的结合依赖关系消除误判的方法按以下步骤进行：4)：将存在依赖关系的候选等价点对应的子电路还原，其它候选等价结点使用变量代替；5)：对还原后的电路调用约束求解器进行求解，如结果为不可满足，则得到两模型等价；如果为可满足，则得到两模型不等价；步骤5：输出等价性验证结果，等价性验证结束。