期刊导航
期刊开放获取
河南省图书馆
退出
期刊文献
+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
检索
高级检索
期刊导航
共找到
7
篇文章
<
1
>
每页显示
20
50
100
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
显示方式:
文摘
详细
列表
相关度排序
被引量排序
时效性排序
用VIS验证微处理器PIC
被引量:
2
1
作者
杜慧敏
刘建元
+1 位作者
韩俊刚
高德远
《计算机辅助设计与图形学学报》
EI
CSCD
北大核心
2000年第5期390-395,共6页
近年来 ,二叉判定图 BDD(Binary Decision Diagram )和符号模型检验在形式化验证数字电路设计中取得了突破性进展 .文中介绍了符号模型检验的基本原理和方法 ,重点介绍如何用 VIS系统验证微处理器 PIC设计的正确性 .利用 VIS证明了 PIC...
近年来 ,二叉判定图 BDD(Binary Decision Diagram )和符号模型检验在形式化验证数字电路设计中取得了突破性进展 .文中介绍了符号模型检验的基本原理和方法 ,重点介绍如何用 VIS系统验证微处理器 PIC设计的正确性 .利用 VIS证明了 PIC设计部分电路的等价性 ,发现了一个设计错误并证明了 PIC中一些重要模块的特性 .
展开更多
关键词
微处理器
检验
VIS
二叉决策图
PIC
下载PDF
职称材料
基于OBDD的SMC反例生成研究
被引量:
1
2
作者
姚全珠
苗永军
《计算机工程与应用》
CSCD
2012年第10期54-58,145,共6页
针对传统的符号模型检测反例生成算法在生成反例时会产生大量的无关变量,使得反例难以理解。提出一种改进的反例生成算法,将反例中的状态扩展为一个状态集,使用零压缩二叉决策图(Zero-Suppressed Binary Decision Diagrams,ZBDD)来存储...
针对传统的符号模型检测反例生成算法在生成反例时会产生大量的无关变量,使得反例难以理解。提出一种改进的反例生成算法,将反例中的状态扩展为一个状态集,使用零压缩二叉决策图(Zero-Suppressed Binary Decision Diagrams,ZBDD)来存储所求出的状态集。删除了系统中的无关变量,仅保留了相关的变量,实验表明该算法能有效地减少状态的变量数,减少存储反例所需的空间。
展开更多
关键词
有序二叉决策图
模型检测
计算树逻辑(CTL)
反例生成
下载PDF
职称材料
基于符号模型检验的硬件验证
被引量:
2
3
作者
刘建元
《微电子学与计算机》
CSCD
北大核心
2002年第5期62-64,共3页
随着程序或电路规模的增大,状态数目将呈指数增加而引起组合爆炸。符号模型检验是形式化方法的一个重要方面,可以处理大规模的数据结构和控制序列,缓和了组合爆炸问题。文章介绍了符号模型检验的原理和方法,利用验证工具VIS验证了8位微...
随着程序或电路规模的增大,状态数目将呈指数增加而引起组合爆炸。符号模型检验是形式化方法的一个重要方面,可以处理大规模的数据结构和控制序列,缓和了组合爆炸问题。文章介绍了符号模型检验的原理和方法,利用验证工具VIS验证了8位微处理器PIC的一些关键属性,并给出实验结果。
展开更多
关键词
符号模型检验
硬件验证
微处理器
有限状态机
分支时态逻辑
有序二叉判定图
下载PDF
职称材料
基于OBDD时序电路设计的验证
4
作者
刘建元
《陕西师范大学学报(自然科学版)》
CAS
CSCD
北大核心
2002年第2期55-58,共4页
依据有序二叉判定图 (OBDD)和计算树逻辑 (或称分支时态逻辑 )CTL(ComputationalTreeLogic)的基本原理 ,分析了基于OBDD和CTL的验证数字电路设计的基本原理 ,并在此基础上 。
关键词
OBDD
时序电路
有序二叉判定图
分支时态逻辑
等价性检验
符号模型检验
布尔函数
电路设计
下载PDF
职称材料
数字电路设计中的符号模型检验技术
5
作者
刘建元
《微电子学与计算机》
CSCD
北大核心
2002年第10期11-12,16,共3页
符号模型检验把有序二叉判定图OBDD技术引入到模型检验中,有效地缓解了状态组合爆炸问题。文章主要介绍了CTL模型检验基本概念和原理,给出了符号模型检验算法,验证了模4计数器的某些特性。
关键词
数字电路设计
有序二叉判定图
分支时态逻辑
模型检验
符号模型检验
OBDD
下载PDF
职称材料
在数字电路验证中使用模型检验
被引量:
3
6
作者
李鸿儒
宋强
《科学技术与工程》
2008年第8期2038-2043,共6页
形式化方法作为仿真方法的补充,为电路功能验证提供了新的途径。介绍了形式化验证方法之一,模型检验的理论基础和实现方法。介绍了分支时态逻辑CTL、CTL的固定点算法,二元决策图BDD,以及符号模型检验方法。最后使用SMV工具在一个CISC处...
形式化方法作为仿真方法的补充,为电路功能验证提供了新的途径。介绍了形式化验证方法之一,模型检验的理论基础和实现方法。介绍了分支时态逻辑CTL、CTL的固定点算法,二元决策图BDD,以及符号模型检验方法。最后使用SMV工具在一个CISC处理器的存储管理单元(MMU)上应用了模型检验,验证了模型检验在模块级验证中的可行性。
展开更多
关键词
形式化验证
模型检验
分支时态逻辑
固定点
符号模型检验
二元决策图
SMV
下载PDF
职称材料
模糊计算树逻辑的符号模型检测
被引量:
1
7
作者
聂朋展
姜久雷
马占有
《计算机应用研究》
CSCD
北大核心
2021年第8期2381-2385,共5页
对含有模糊不确定性信息的系统进行模型检测时,状态空间爆炸问题成为了亟待解决的主要问题。将形式化的系统模型用拟布尔公式表示,用多终端二叉决策图来对拟布尔公式进行存储。对模糊计算树逻辑的不动点语义给出了解释和证明,然后给出...
对含有模糊不确定性信息的系统进行模型检测时,状态空间爆炸问题成为了亟待解决的主要问题。将形式化的系统模型用拟布尔公式表示,用多终端二叉决策图来对拟布尔公式进行存储。对模糊计算树逻辑的不动点语义给出了解释和证明,然后给出模糊计算树逻辑的符号化模型检测算法,最后通过一个实例验证算法的正确性。该算法可有效缓解对模糊模型检测验证时的状态空间爆炸问题,并扩展了模型检测的应用范围。
展开更多
关键词
模糊计算树逻辑
不动点算法
多终端二叉决策图
符号模型检测
下载PDF
职称材料
题名
用VIS验证微处理器PIC
被引量:
2
1
作者
杜慧敏
刘建元
韩俊刚
高德远
机构
西安邮电学院ASIC中心
出处
《计算机辅助设计与图形学学报》
EI
CSCD
北大核心
2000年第5期390-395,共6页
基金
国家自然科学基金!( 69473 0 17)
文摘
近年来 ,二叉判定图 BDD(Binary Decision Diagram )和符号模型检验在形式化验证数字电路设计中取得了突破性进展 .文中介绍了符号模型检验的基本原理和方法 ,重点介绍如何用 VIS系统验证微处理器 PIC设计的正确性 .利用 VIS证明了 PIC设计部分电路的等价性 ,发现了一个设计错误并证明了 PIC中一些重要模块的特性 .
关键词
微处理器
检验
VIS
二叉决策图
PIC
Keywords
binary
decision
diagram
,
computational tree logic
, equivalence
check
,
symbolic model checking
分类号
TP332.06 [自动化与计算机技术—计算机系统结构]
下载PDF
职称材料
题名
基于OBDD的SMC反例生成研究
被引量:
1
2
作者
姚全珠
苗永军
机构
西安理工大学计算机科学与工程学院
出处
《计算机工程与应用》
CSCD
2012年第10期54-58,145,共6页
文摘
针对传统的符号模型检测反例生成算法在生成反例时会产生大量的无关变量,使得反例难以理解。提出一种改进的反例生成算法,将反例中的状态扩展为一个状态集,使用零压缩二叉决策图(Zero-Suppressed Binary Decision Diagrams,ZBDD)来存储所求出的状态集。删除了系统中的无关变量,仅保留了相关的变量,实验表明该算法能有效地减少状态的变量数,减少存储反例所需的空间。
关键词
有序二叉决策图
模型检测
计算树逻辑(CTL)
反例生成
Keywords
ordered binary decision diagram
(OBDD)
model
checking
comput
ation
tree
logic
(CTL)
counter-example generation
分类号
TP311 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
基于符号模型检验的硬件验证
被引量:
2
3
作者
刘建元
机构
西安邮电学院
出处
《微电子学与计算机》
CSCD
北大核心
2002年第5期62-64,共3页
基金
国家自然科学基金资助项目(69473017)
文摘
随着程序或电路规模的增大,状态数目将呈指数增加而引起组合爆炸。符号模型检验是形式化方法的一个重要方面,可以处理大规模的数据结构和控制序列,缓和了组合爆炸问题。文章介绍了符号模型检验的原理和方法,利用验证工具VIS验证了8位微处理器PIC的一些关键属性,并给出实验结果。
关键词
符号模型检验
硬件验证
微处理器
有限状态机
分支时态逻辑
有序二叉判定图
Keywords
finite-state machine
,
computational tree logic
,
ordered binary decision diagram
,
symbolic model checking
分类号
TP332 [自动化与计算机技术—计算机系统结构]
下载PDF
职称材料
题名
基于OBDD时序电路设计的验证
4
作者
刘建元
机构
西安邮电学院计算机科学系
出处
《陕西师范大学学报(自然科学版)》
CAS
CSCD
北大核心
2002年第2期55-58,共4页
基金
国家自然科学基金资助项目 (6 94 730 17)
文摘
依据有序二叉判定图 (OBDD)和计算树逻辑 (或称分支时态逻辑 )CTL(ComputationalTreeLogic)的基本原理 ,分析了基于OBDD和CTL的验证数字电路设计的基本原理 ,并在此基础上 。
关键词
OBDD
时序电路
有序二叉判定图
分支时态逻辑
等价性检验
符号模型检验
布尔函数
电路设计
Keywords
ordered binary decision diagram
computational tree logic
equivalence
checking
symbolic model checking
分类号
TN791 [电子电信—电路与系统]
下载PDF
职称材料
题名
数字电路设计中的符号模型检验技术
5
作者
刘建元
机构
西安邮电学院
出处
《微电子学与计算机》
CSCD
北大核心
2002年第10期11-12,16,共3页
基金
国家自然科学基金(69473017)
文摘
符号模型检验把有序二叉判定图OBDD技术引入到模型检验中,有效地缓解了状态组合爆炸问题。文章主要介绍了CTL模型检验基本概念和原理,给出了符号模型检验算法,验证了模4计数器的某些特性。
关键词
数字电路设计
有序二叉判定图
分支时态逻辑
模型检验
符号模型检验
OBDD
Keywords
ordered binary decision diagram
,
computational tree logic
,
model
checking
,
symbolic model checking
分类号
TN79 [电子电信—电路与系统]
下载PDF
职称材料
题名
在数字电路验证中使用模型检验
被引量:
3
6
作者
李鸿儒
宋强
机构
西北工业大学
出处
《科学技术与工程》
2008年第8期2038-2043,共6页
文摘
形式化方法作为仿真方法的补充,为电路功能验证提供了新的途径。介绍了形式化验证方法之一,模型检验的理论基础和实现方法。介绍了分支时态逻辑CTL、CTL的固定点算法,二元决策图BDD,以及符号模型检验方法。最后使用SMV工具在一个CISC处理器的存储管理单元(MMU)上应用了模型检验,验证了模型检验在模块级验证中的可行性。
关键词
形式化验证
模型检验
分支时态逻辑
固定点
符号模型检验
二元决策图
SMV
Keywords
formal verification
model
checking
computational tree logic
fix point
symbolic model checking
binary
decision
diagram
SMV
分类号
TP301.6 [自动化与计算机技术—计算机系统结构]
下载PDF
职称材料
题名
模糊计算树逻辑的符号模型检测
被引量:
1
7
作者
聂朋展
姜久雷
马占有
机构
北方民族大学计算机科学与工程学院
常熟理工学院计算机科学与工程学院
出处
《计算机应用研究》
CSCD
北大核心
2021年第8期2381-2385,共5页
基金
国家自然科学基金资助项目(61762002,61962001)
宁夏自然科学基金资助项目(2018AAC03127)
北方民族大学研究生创新项目(YCX20068)。
文摘
对含有模糊不确定性信息的系统进行模型检测时,状态空间爆炸问题成为了亟待解决的主要问题。将形式化的系统模型用拟布尔公式表示,用多终端二叉决策图来对拟布尔公式进行存储。对模糊计算树逻辑的不动点语义给出了解释和证明,然后给出模糊计算树逻辑的符号化模型检测算法,最后通过一个实例验证算法的正确性。该算法可有效缓解对模糊模型检测验证时的状态空间爆炸问题,并扩展了模型检测的应用范围。
关键词
模糊计算树逻辑
不动点算法
多终端二叉决策图
符号模型检测
Keywords
fuzzy
comput
ation
tree
logic
fixed point algorithm
multi-terminal
binary
decision
diagram
s
symbolic model checking
分类号
TP305 [自动化与计算机技术—计算机系统结构]
下载PDF
职称材料
题名
作者
出处
发文年
被引量
操作
1
用VIS验证微处理器PIC
杜慧敏
刘建元
韩俊刚
高德远
《计算机辅助设计与图形学学报》
EI
CSCD
北大核心
2000
2
下载PDF
职称材料
2
基于OBDD的SMC反例生成研究
姚全珠
苗永军
《计算机工程与应用》
CSCD
2012
1
下载PDF
职称材料
3
基于符号模型检验的硬件验证
刘建元
《微电子学与计算机》
CSCD
北大核心
2002
2
下载PDF
职称材料
4
基于OBDD时序电路设计的验证
刘建元
《陕西师范大学学报(自然科学版)》
CAS
CSCD
北大核心
2002
0
下载PDF
职称材料
5
数字电路设计中的符号模型检验技术
刘建元
《微电子学与计算机》
CSCD
北大核心
2002
0
下载PDF
职称材料
6
在数字电路验证中使用模型检验
李鸿儒
宋强
《科学技术与工程》
2008
3
下载PDF
职称材料
7
模糊计算树逻辑的符号模型检测
聂朋展
姜久雷
马占有
《计算机应用研究》
CSCD
北大核心
2021
1
下载PDF
职称材料
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
上一页
1
下一页
到第
页
确定
用户登录
登录
IP登录
使用帮助
返回顶部