公开(公告)号：CN103838908A

公开(公告)日：2014-06-04

申请号：CN201310418675.3

申请日：2013-09-14

Applicant: 电子科技大学

Inventor： 杨国武 ,  崔晓爽 ,  高毅 ,  康文涛 ,  牛伟纳 ,  张艳 ,  徐永生 ,  杨俊 ,  杨绪鹏 ,  周志慧

IPC: G06F17/50

Abstract: 本发明提供了一种基于AIG和SAT求解器的GSTE模型检测方法，其特征在于包括以下步骤：步骤1，使用ABC工具建立AIG模型；将该AIG转化成FRAIG，同时使用逻辑综合算法化简该FRAIG，减小AIG规模；步骤2，计算每条边上的状态集不动点Ψ*，步骤3：将算得的每条边上的不动点和相应边上的cons做验证，若则报错，并通过反向迁移找到反例；步骤4：判断每条边上的状态集是否到达不动点，若到达不动点，完成本次验证，否则返回步骤2，进行下一轮状态集的计算。

公开(公告)号：CN103838908B

公开(公告)日：2017-08-25

申请号：CN201310418675.3

申请日：2013-09-14

Applicant: 电子科技大学

Inventor： 杨国武 ,  崔晓爽 ,  高毅 ,  康文涛 ,  牛伟纳 ,  张艳 ,  徐永生 ,  杨俊 ,  杨绪鹏 ,  周志慧

IPC: G06F17/50

Abstract: 本发明提供了一种基于AIG和SAT求解器的GSTE模型检测方法，其特征在于包括以下步骤：步骤1，使用ABC工具建立AIG模型；将该AIG转化成FRAIG，同时使用逻辑综合算法化简该FRAIG，减小AIG规模；步骤2，计算每条边上的状态集不动点Ψ*，步骤3：将算得的每条边上的不动点和相应边上的cons做验证，若则报错，并通过反向迁移找到反例；步骤4：判断每条边上的状态集是否到达不动点，若到达不动点，完成本次验证，否则返回步骤2，进行下一轮状态集的计算。