一种结合约束满足消除误判的等价性验证方法

• 摘要：

  本发明涉及一种结合约束满足消除误判的等价性验证方法,属于模型验证技术领域.本方法首先在规范模型和实现模型中根据启发式信息选择合适的候选等价对;然后在约束求解器中对电路的输入变量进行基于边界赋值的约束传播快速求解;最后如果不存在误判现象,直接输入结果;否则用如下方法消除误判:a)将当前等价对所对应的模型转为约束关系;b)用约束求解器求得所有规范模型和实现模型不等价的赋值,并转为约束关系;c)将步骤a和b得到的约束关系调用约束求解器的进行求解,如结果为不可满足,则得到两模型等价;如果为可满足,则得到模型不等价.本发明提高了等价性验证效率和芯片的首次硅片成功率,加快电子产品上市时间.

• 专利类型：

  发明专利

• 申请/专利号：

  CN201010204016.6

• 申请日期：

  2010.06.21

• 公开/公告号：

  CN101887473A

• 公开/公告日：

  2010-11-17

• 发明人：

  欧阳丹彤 张立明 白洪涛 李占山

• 申请人：

  吉林大学

• 主分类号：

  G06F17/50(2006.01)I

• 主权项：

  一种结合约束满足消除误判的等价性验证方法,其特征在于:至少包括如下步骤:步骤1:建立规范描述和实现描述的模型;步骤2:在规范模型和实现模型中选择合适候选等价对位置,便于基于割集方法的等价性验证;步骤3:对于候选等价对利用约束求解器进行快速求解;步骤4:判断是否可能存在误判:如果得到规范模型和实现模型等价,则验证结果为等价,不存在误判,转步骤6;如果得到规范模型和实现模型不等价,但此时并不能得到两模型不等价,即可能存在误判现象;步骤5:消除误判现象;步骤6:输出等价性验证结果,等价性验证结束.