公开(公告)号：CN101556627B

公开(公告)日：2011-12-07

申请号：CN200910083790.3

申请日：2009-05-13

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

Inventor： 陈博文 ,  沈海华

IPC: G06F17/50

Abstract: 本发明涉及用于验证电路的模型检测中的模型抽象方法和系统，所述电路由Verilog设计，所述方法包括：步骤1，读入所述电路的Verilog代码，依据检测需求处理所述Verilog代码中的变量，以规范并简化所述代码；步骤2，根据规范后的所述变量和该变量的赋值，提取所述电路的数据路径；步骤3，提取数据路径的数据运算，根据该数据运算抽象所述数据路径；步骤4，对抽象后的所述变量和该变量的赋值进行操作，生成状态机的状态集和边集。本发明能够在用户提供必要的信息后，自动对Verilog代码进行分析，从中提取数据路径。

公开(公告)号：CN101504687A

公开(公告)日：2009-08-12

申请号：CN200910079992.0

申请日：2009-03-16

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

Inventor： 陈博文 ,  沈海华

IPC: G06F17/50

Abstract: 本发明涉及模型检测中的模型抽象方法及系统，方法包括：步骤1，输入原始模型和指导属性；步骤2，为指导属性的每个节点求解其在原始模型中的超语义，根据超语义为指导属性的每个非叶子节点求解对应的基本序列；步骤3，对原始模型的状态空间建立划分；步骤4，应用指导属性、每个节点的超语义和每个非叶子节点的基本序列分割划分；步骤5，为指导属性的每个节点建立对应的证明模型，应用证明模型进一步分割步骤4分割后的划分；步骤6，由进一步分割后的划分生成原始模型对应的抽象模型。本发明能够在只提供指导属性的前提下，根据该指导属性自动地完成细化工作，同时使细划后的划分能够保留与指导属性相关的信息。

公开(公告)号：CN100514971C

公开(公告)日：2009-07-15

申请号：CN200610065680.0

申请日：2006-03-21

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

Inventor： 陈博文

IPC: H04L29/06

Abstract: 本发明公开了一种IP核接口标准化方法，用于建立IP核间点对点通信的标准接口，包含以下方面：1、建立IP核间的点对点通信信道，所述点对点通信信道由FIFO实现；在IP核间做点对点通信时，所述IP核分为主动端与被动端；所述的点对点通信信道分为三个子信道，子信道1用于所述主动端向所述被动端发送数据，子信道2用于所述主动端向所述被动端发送数据请求，子信道3用于所述被动端向所述主动端发送数据；2、根据IP核是主动端或被动端，为IP核定义不同的接口。本发明对IP核接口进行标准化，使IP核接口不再依赖于特定的片上总线规范，增强了IP核的可重用性。本发明提供的IP核接口具有通用性，适用范围广。

公开(公告)号：CN101556627A

公开(公告)日：2009-10-14

申请号：CN200910083790.3

申请日：2009-05-13

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

Inventor： 陈博文 ,  沈海华

IPC: G06F17/50

Abstract: 本发明涉及用于验证电路的模型检测中的模型抽象方法和系统，所述电路由Verilog设计，所述方法包括：步骤1，读入所述电路的Verilog代码，依据检测需求处理所述Verilog代码中的变量，以规范并简化所述代码；步骤2，根据规范后的所述变量和该变量的赋值，提取所述电路的数据路径；步骤3，提取数据路径的数据运算，根据该数据运算抽象所述数据路径；步骤4，对抽象后的所述变量和该变量的赋值进行操作，生成状态机的状态集和边集。本发明能够在用户提供必要的信息后，自动对Verilog代码进行分析，从中提取数据路径。

公开(公告)号：CN1822597A

公开(公告)日：2006-08-23

申请号：CN200610065680.0

申请日：2006-03-21

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

Inventor： 陈博文

IPC: H04L29/06

Abstract: 本发明公开了一种IP核接口标准化方法，用于建立IP核间点对点通信的标准接口，包含以下方面：1.建立IP核间的点对点通信信道，所述点对点通信信道由FIFO实现；在IP核间做点对点通信时，所述IP核分为主动端与被动端；所述的点对点通信信道分为三个子信道，子信道1用于所述主动端向所述被动端发送数据，子信道2用于所述主动端向所述被动端发送数据请求，子信道3用于所述被动端向所述主动端发送数据；2.根据IP核是主动端或被动端，为IP核定义不同的接口。本发明对IP核接口进行标准化，使IP核接口不再依赖于特定的片上总线规范，增强了IP核的可重用性。本发明提供的IP核接口具有通用性，适用范围广。