公开(公告)号：CN101794330A

公开(公告)日：2010-08-04

申请号：CN200910244172.2

申请日：2009-12-30

Applicant: 中国科学院计算技术研究所

Inventor： 张弢 ,  吕涛 ,  李晓维

IPC: G06F17/50

Abstract: 本发明涉及集成电路验证方法及其系统，方法包括：步骤1，抽象引擎对待验证的集成电路进行抽象，生成对应的抽象模型，进行形式化计算；步骤2，激励生成引擎初始化根据待检测的集成电路的规范建立的马尔可夫模型；步骤3，激励生成引擎由马尔可夫模型生成激励，将激励输入仿真器，仿真器对待检测的集成电路进行仿真；步骤4，激励生成引擎依据形式化信息比较本周期仿真结果和上周期仿真获得的仿真结果，如果本周期仿真结果更接近目标状态，则调整马尔可夫模型中参数；步骤5，如果待检测的集成电路未达到目标状态并且仿真次数未超过预设次数，则执行步骤3；否则，终止仿真，并报告成功或者运行超时。本发明能够降低计算成本，提高检测效率。

公开(公告)号：CN101794330B

公开(公告)日：2011-11-09

申请号：CN200910244172.2

申请日：2009-12-30

Applicant: 中国科学院计算技术研究所

Inventor： 张弢 ,  吕涛 ,  李晓维

IPC: G06F17/50

Abstract: 本发明涉及集成电路验证方法及其系统，方法包括：步骤1，抽象引擎对待验证的集成电路进行抽象，生成对应的抽象模型，进行形式化计算；步骤2，激励生成引擎初始化根据待检测的集成电路的规范建立的马尔可夫模型；步骤3，激励生成引擎由马尔可夫模型生成激励，将激励输入仿真器，仿真器对待检测的集成电路进行仿真；步骤4，激励生成引擎依据形式化信息比较本周期仿真结果和上周期仿真获得的仿真结果，如果本周期仿真结果更接近目标状态，则调整马尔可夫模型中参数；步骤5，如果待检测的集成电路未达到目标状态并且仿真次数未超过预设次数，则执行步骤3；否则，终止仿真，并报告成功或者运行超时。本发明能够降低计算成本，提高检测效率。