郑飞君

作品数:8被引量:31H指数:3
导出分析报告
供职机构:浙江大学电气工程学院超大规模集成电路设计研究所更多>>
发文主题:等价性验证等价性组合电路布尔可满足性KRIPKE结构更多>>
发文领域:自动化与计算机技术电子电信更多>>
发文期刊:《浙江大学学报(理学版)》《电路与系统学报》《电子学报》《计算机辅助设计与图形学学报》更多>>
所获基金:国家自然科学基金更多>>
-

检索结果分析

署名顺序

  • 全部
  • 第一作者
结果分析中...
条 记 录,以下是1-8
视图:
排序:
结合半加图的算术电路等价性验证技术
《浙江大学学报(工学版)》2008年第8期1345-1349,1403,共6页翁延玲 葛海通 严晓浪 郑飞君 
国家自然科学基金资助项目(90207002)
为了克服现有等价性验证技术难以快速验证复杂算术电路的局限性,提出了一种利用综合引擎分析并再现算术电路优化过程的算法.该算法结合了乘法器的编码方式识别技术、加法电路的半加树提取技术和部分积加法电路的架构识别技术来提取乘法...
关键词:综合 等价性验证 算术电路 半加树 
一种避免内存爆炸的组合电路等价性验证方法
《电路与系统学报》2007年第3期21-25,共5页杨军 卢永江 葛海通 郑飞君 严晓浪 
国家自然科学基金资助项目(90207002)
割集在组合电路等价性验证中得到了广泛的应用,已有的方法常构造能将整个电路一分为二的割集,虽然这种割集在验证后续节点时可以重用已构建的BDD,但它的排序对大多数后续节点都很差,容易引起内存爆炸问题。本文中的割集只针对要验证等...
关键词:等价性验证 BDD 割集 
结合通用割集和专用割集的组合电路验证方法被引量:1
《浙江大学学报(工学版)》2006年第9期1511-1515,共5页杨军 郑飞君 卢永江 葛海通 严晓浪 
国家自然科学基金资助项目(90207002)
为了提高组合电路的等价性验证速度,提出了一种利用电路内部等价信息的新型验证方法.该方法结合了通用割集和专用割集.从原始输出进行回溯得到通用割集,用通用割集验证所有候选等价点(CEP)的等价性.从特定候选等价点进行回溯得到专用割...
关键词:形式验证 通用割集 专用割集 依赖性 
一种形式化验证方法:模型检验被引量:17
《浙江大学学报(理学版)》2006年第4期403-407,共5页杨军 葛海通 郑飞君 严晓浪 
国家自然科学基金资助项目(No.90207002)
模型检验作为一种形式化验证方法,近年来在各种硬件、软件设计中得到了广泛应用.文中首先介绍了描述系统行为的Kripke结构和描述系统性质的CTL逻辑,然后介绍了模型检验中常用的两种算法:标记算法和基于固定点的算法,最后介绍了为避免内...
关键词:模型检验 KRIPKE结构 CTL逻辑 标记 固定点 符号模型检验 
面向等价性验证的锁存器匹配算法被引量:2
《浙江大学学报(工学版)》2006年第8期1293-1296,共4页郑飞君 杨军 葛海通 严晓浪 
国家自然科学基金资助项目(90207002)
为了克服现有等价性验证技术中难以精确匹配锁存器的局限性,提出了一种结合多种方法的新型锁存器匹配算法.该算法结合任意模拟、局部二叉判决图、目标模拟3种方法来匹配锁存器,并使用了类似滤波器的思想,任意模拟对锁存器作初步快速匹配...
关键词:等价性验证 锁存器匹配 局部二叉判决图 目标模拟 
使用输出分组和电路可满足性的等价性验证算法被引量:3
《计算机辅助设计与图形学学报》2005年第11期2484-2488,共5页郑飞君 严晓浪 葛海通 杨军 卢永江 
国家自然科学基金(90207002)
介绍了一种使用电路可满足性解算器的组合电路等价性验证算法.对包含多输出的复杂验证问题,首先对联接电路作输出分组,将等价性验证问题转化为包含若干个组的电路可满足性问题,继而使用电路解算器解决问题.同时,注意各个子问题间的有用...
关键词:等价性验证 输出分组 电路可满足性 
使用布尔可满足性的组合电路等价性验证算法被引量:3
《电子与信息学报》2005年第4期651-654,共4页郑飞君 严晓浪 葛海通 杨军 
国家自然科学基金(90207002)资助课题
该文提出了一种使用布尔可满足性SAT的新颖组合电路等价性验证技术。算法是在联接电路(Miter circuit)中进行推理来简化验证问题,推理中使用了'与/非'图结构简化、BDD扩展、隐含学习多种方法,最后 使用有效SAT解算器zChaff解决验证任...
关键词:等价性验证 与/非图 可满足性解算器 隐含学习 
结合二叉判决图和布尔可满足性的等价性验证算法被引量:8
《电子学报》2004年第8期1233-1235,共3页严晓浪 郑飞君 葛海通 杨军 
国家自然科学基金 (No .90 2 0 70 0 2 )
本文提出了一种结合二叉判决图BDD和布尔可满足性SAT的新颖组合电路等价性验证技术 .算法是在与 /非图AIG中进行推理 ,并交替使用BDD扩展和基于电路SAT解算器简化电路 .如尚未解决 ,将用基于合取范式SAT解算器进行推理 .与已有算法相比...
关键词:等价性验证 与/非图 孤立节点 二叉判决图 可满足性解算器 
检索报告 对象比较 聚类工具 使用帮助 返回顶部