公开(公告)号：CN103150453A

公开(公告)日：2013-06-12

申请号：CN201310101920.8

申请日：2013-03-27

Applicant: 吉林大学

Inventor： 张立明 ,  欧阳丹彤 ,  赵毅 ,  叶育鑫 ,  李占山 ,  张永刚 ,  于海鸿 ,  李河 ,  刘杰 ,  董旭初

IPC: G06F17/50

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

公开(公告)号：CN102929149A

公开(公告)日：2013-02-13

申请号：CN201210444316.0

申请日：2012-11-08

Applicant: 吉林大学

Inventor： 张立明 ,  欧阳丹彤 ,  赵毅 ,  李占山 ,  白洪涛 ,  张永刚 ,  于海鸿 ,  李河 ,  刘杰 ,  董旭初

IPC: G05B13/04

Abstract: 本发明涉及一种离散事件系统的反向遍历诊断方法，属于模型诊断技术领域。首先建立系统模型自动机；选择合适位置加入便于诊断所需的传感器，参考系统最大传输延迟的相关性质设计时间窗口。然后，根据时间窗口的长度，周期得到系统的观测序列和状态。随后，如当观测序列发生改变时，根据当前时间窗口内的观测和自动机间的转移关系，进行反向遍历，反向遍历得到前一状态的信息。如果为初始状态，则给出相应路径及其故障信息；如果为中间状态，则根据此中间状态给出相应的路径及其诊断信息。此时如果得到诊断信息，将此窗口内得到的观测和诊断信息加入到中间状态列表，完成当前窗口观测的诊断。否则继续反向遍历前一状态，直到完成诊断。

公开(公告)号：CN102929149B

公开(公告)日：2015-03-11

申请号：CN201210444316.0

申请日：2012-11-08

Applicant: 吉林大学

Inventor： 张立明 ,  欧阳丹彤 ,  赵毅 ,  李占山 ,  白洪涛 ,  张永刚 ,  于海鸿 ,  李河 ,  刘杰 ,  董旭初

IPC: G06F11/00

Abstract: 本发明涉及一种离散事件系统的反向遍历诊断方法，属于模型诊断技术领域。首先建立系统模型自动机；选择合适位置加入便于诊断所需的传感器，参考系统最大传输延迟的相关性质设计时间窗口。然后，根据时间窗口的长度，周期得到系统的观测序列和状态。随后，如当观测序列发生改变时，根据当前时间窗口内的观测和自动机间的转移关系，进行反向遍历，反向遍历得到前一状态的信息。如果为初始状态，则给出相应路径及其故障信息；如果为中间状态，则根据此中间状态给出相应的路径及其诊断信息。此时如果得到诊断信息，将此窗口内得到的观测和诊断信息加入到中间状态列表，完成当前窗口观测的诊断。否则继续反向遍历前一状态，直到完成诊断。

公开(公告)号：CN103150453B

公开(公告)日：2016-01-06

申请号：CN201310101920.8

申请日：2013-03-27

Applicant: 吉林大学

Inventor： 张立明 ,  欧阳丹彤 ,  赵毅 ,  叶育鑫 ,  李占山 ,  张永刚 ,  于海鸿 ,  李河 ,  刘杰 ,  董旭初

IPC: G06F17/50

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