刘建元

作品数：11被引量：14H指数：2
导出分析报告
供职机构：西安邮电学院计算机学院更多>>
发文主题：符号模型检验布尔函数微处理器二叉决策图OBDD更多>>
发文领域：自动化与计算机技术电子电信理学更多>>
发文期刊：《西北大学学报（自然科学版）》《微电子学与计算机》《计算机辅助设计与图形学学报》《小型微型计算机系统》更多>>
所获基金：国家自然科学基金国家高技术研究发展计划更多>>
-
在结果中检索

检索结果分析

署名顺序

  • 全部
  • 第一作者
结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
三维模型库语义网构建及检索方法研究被引量：2
《西安邮电学院学报》2012年第3期53-57,共5页贾晖 刘建元 张建刚 
为了实现三维模型语义检索,描述了一种基于本体来构建三维模型库语义网的方法,并在此基础上实现基于语义的三维模型检索。该方法首先建立三维模型库本体描述,根据模型库中的内容提取类,对象和属性。其次利用Word-Net英文本体查找本体原...
关键词：三维模型检索技术 三维模型库 WORDNET 语义网 
雷达数字波束形成及其数学分析被引量：2
《雷达与对抗》2008年第2期32-35,共4页裴晓东 刘建元 
从相控阵雷达波束形成原理逐步引出了数字波束形成技术,并就其数字配相和幅度加权进行了详细的数学分析。给出了一种数字波束形成器的实现结构,也客观地指出了目前在工程实现中仍需注意的一些问题。
关键词：雷达 数字波束形成 数字配相 幅度加权 
数字电路设计中的符号模型检验技术
《微电子学与计算机》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 ) ,其中
关键词：语言包含 互模拟 有限自动机 计算机 
基于PVS的飞机订票系统的形式化描述与验证被引量：1
《西安邮电学院学报》2001年第3期1-5,共5页杨红丽 刘建元 韩俊刚 
国家 8 6 3资助项目
形式化方法主要应用于安全性第一的系统的规范与形式验证。原型证明系统PVS为开发和分析形式化规范和验证提供了一个集成化环境。本文介绍PVS系统的证明方法和特点 ,并利用PVS系统对飞机订票系统的需求给出了形式化规范 ,对部分关键属...
关键词：PVS 形式化规范 形式化证明 
有序二叉判定图及其构造算法研究被引量：1
《西安邮电学院学报》2001年第3期6-10,共5页刘建元 
国家自然科学基金资助 (6 94730 1)
有序二叉判定图OBDD(orderedbinarydecisiondiagram)是一种数据结构 ,它把布尔函数表示为有向无回路图 ,是布尔函数的一种正则表示 ,可以用来检查布尔函数的一些性质如可满足性、等价性等等。本文将详细地介绍OBDD的数据结构及基于OBDD...
关键词：二叉决策图 分支程序 符号操作 布尔函数 布尔代数 逻辑设计验证 
用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语言 翻译程序 硬件描述语言 
全选清除导出
共2页<12>
检索报告 对象比较 聚类工具 使用帮助 返回顶部