国家自然科学基金(69473017)

作品数：10被引量：13H指数：2
导出分析报告
相关作者：韩俊刚刘建元杜慧敏郭建郝克刚更多>>
相关机构：西安邮电学院西北大学西北工业大学更多>>
相关期刊：《计算机工程与应用》《西北大学学报（自然科学版）》《微电子学与计算机》《计算机辅助设计与图形学学报》更多>>
相关主题：形式化验证符号模型检验布尔函数计算机微处理器更多>>
相关领域：自动化与计算机技术电子电信更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
数字电路设计中的符号模型检验技术
《微电子学与计算机》2002年第10期11-12,16,共3页刘建元 
国家自然科学基金(69473017)
符号模型检验把有序二叉判定图OBDD技术引入到模型检验中,有效地缓解了状态组合爆炸问题。文章主要介绍了CTL模型检验基本概念和原理,给出了符号模型检验算法,验证了模4计数器的某些特性。
关键词：数字电路设计 有序二叉判定图 分支时态逻辑 模型检验 符号模型检验 OBDD 
基于符号模型检验的硬件验证被引量：2
《微电子学与计算机》2002年第5期62-64,共3页刘建元 
国家自然科学基金资助项目(69473017)
随着程序或电路规模的增大,状态数目将呈指数增加而引起组合爆炸。符号模型检验是形式化方法的一个重要方面,可以处理大规模的数据结构和控制序列,缓和了组合爆炸问题。文章介绍了符号模型检验的原理和方法,利用验证工具VIS验证了8位微...
关键词：符号模型检验 硬件验证 微处理器 有限状态机 分支时态逻辑 有序二叉判定图 
基于OBDD时序电路设计的验证
《陕西师范大学学报（自然科学版）》2002年第2期55-58,共4页刘建元 
国家自然科学基金资助项目 (6 94 730 17)
依据有序二叉判定图 (OBDD)和计算树逻辑 (或称分支时态逻辑 )CTL(ComputationalTreeLogic)的基本原理 ,分析了基于OBDD和CTL的验证数字电路设计的基本原理 ,并在此基础上 。
关键词：OBDD 时序电路 有序二叉判定图 分支时态逻辑 等价性检验 符号模型检验 布尔函数 电路设计 
一种测试语言包含的算法
《小型微型计算机系统》2001年第10期1241-1244,共4页刘建元 杜慧敏 
国家自然科学基金 (69473 0 17)资助
在积自动机基础上 ,利用互模拟关系引出了商自动机 ,用以解决积自动机的状态组合爆炸问题 .进而提出一个自然的测试语言包含的算法 ,这种算法的空间复杂度与规范自动机的状态数目呈指数关系即 O(2 k ) ,其中
关键词：语言包含 互模拟 有限自动机 计算机 
用VIS系统验证电路的实时特性的探讨被引量：1
《计算机工程与应用》2001年第17期74-76,110,共4页郭建 韩俊刚 
国家自然科学基金资助(编号:69473017)。
文章在分析形式化验证／综合系统VIS 的基础上，改进了该电子系统中的关键技术——二叉判定图（BDD），使BDD能表示电路的定时性质，这样就为VIS系统能够进行电路的时间特性验证和实时模型检验打下了基础。
关键词：VIS系统 形式化验证 二叉判定图 实时二叉判定图 集成电路 制造工艺 
基于时态逻辑的硬件设计形式化验证技术——模型检验被引量：5
《小型微型计算机系统》2001年第5期521-524,共4页郭建 杜惠敏 韩俊刚 郝克刚 
国家自然科学基金资助! (NO69473 0 17)
通过对时态逻辑的研究来探讨时态逻辑在硬件设计形式化验证上的应用 ,同时对布尔函数在计算机内的表示二叉判定图 (BDD)进行了进一步地分析 。
关键词：时态逻辑 模型检验 布尔函数 硬件设计 形式化验证 计算机 
实时系统状态空间分析的一种算法
《计算机应用》2000年第S1期62-65,共4页杜慧敏 杨红丽 韩俊刚 
自然科学基金!(694730 1 7)
提出了一种生成实时系统可达状态的算法 ,该算法生成一个较小的状态空间 ,但仍然保留了足够的时间信息用于分析。同时给出一个实例来说明算法的有效性 ,并与其它方法进行了比较。
关键词：形式化验证 互模拟 实时自动机 区域图 可达图 
对VIS系统关键技术的改进
《计算机应用》2000年第S1期184-187,共4页郭建 韩俊刚 
国家自然科学基金!(694730 1 7)
本文在分析形式化验证 /综合系统VIS的基础上 ,改进了此系统中的关键技术———二叉判定图 (BDD) ,使BDD能表示电路的定时性质 ,这样就为VIS系统能够进行电路的时间特性验证和实时模型检验打下了基础。
关键词：VIS系统 形式化验证 二叉判定图 实时二叉判定图 
用VIS验证微处理器PIC被引量：2
《计算机辅助设计与图形学学报》2000年第5期390-395,共6页杜慧敏 刘建元 韩俊刚 高德远 
国家自然科学基金!( 69473 0 17)
近年来 ,二叉判定图 BDD(Binary Decision Diagram )和符号模型检验在形式化验证数字电路设计中取得了突破性进展 .文中介绍了符号模型检验的基本原理和方法 ,重点介绍如何用 VIS系统验证微处理器 PIC设计的正确性 .利用 VIS证明了 PIC...
关键词：微处理器 检验 VIS 二叉决策图 PIC 
硬件描述语言VHDL到Verilog的翻译被引量：4
《西北大学学报（自然科学版）》2000年第1期15-19,共5页郭建 刘建元 杜慧敏 韩俊刚 郝克刚 华庆一 
国家自然科学基金资助项目!(69473017)
分析了两种常用硬件描述语言 Verilog和 VHDL的语言特征 ,找出它们之间内在的对应关系 ,并阐述了由 VHDL向 Verilog语言翻译的实现方法。
关键词：VHDL语言 VERILOG语言 翻译程序 硬件描述语言 
全选清除导出
共1页<1>
检索报告 对象比较 聚类工具 使用帮助 返回顶部