期刊文献+
共找到10篇文章
< 1 >
每页显示 20 50 100
使用布尔可满足性的组合电路等价性验证算法 被引量:3
1
作者 郑飞君 严晓浪 +1 位作者 葛海通 杨军 《电子与信息学报》 EI CSCD 北大核心 2005年第4期651-654,共4页
该文提出了一种使用布尔可满足性SAT的新颖组合电路等价性验证技术。算法是在联接电路(Miter circuit)中进行推理来简化验证问题,推理中使用了'与/非'图结构简化、BDD扩展、隐含学习多种方法,最后 使用有效SAT解算器zChaff解... 该文提出了一种使用布尔可满足性SAT的新颖组合电路等价性验证技术。算法是在联接电路(Miter circuit)中进行推理来简化验证问题,推理中使用了'与/非'图结构简化、BDD扩展、隐含学习多种方法,最后 使用有效SAT解算器zChaff解决验证任务。该算法综合了BDD和SAT的优点,限制BDD构建大小避免了内存爆 炸,推理简化减小了SAT搜索空间。ISCAS85电路实验结果表明了本算法的有效性。 展开更多
关键词 等价性验证 与/非图 可满足性解算器 隐含学习
下载PDF
使用输出分组和电路可满足性的等价性验证算法 被引量:3
2
作者 郑飞君 严晓浪 +2 位作者 葛海通 杨军 卢永江 《计算机辅助设计与图形学学报》 EI CSCD 北大核心 2005年第11期2484-2488,共5页
介绍了一种使用电路可满足性解算器的组合电路等价性验证算法.对包含多输出的复杂验证问题,首先对联接电路作输出分组,将等价性验证问题转化为包含若干个组的电路可满足性问题,继而使用电路解算器解决问题.同时,注意各个子问题间的有用... 介绍了一种使用电路可满足性解算器的组合电路等价性验证算法.对包含多输出的复杂验证问题,首先对联接电路作输出分组,将等价性验证问题转化为包含若干个组的电路可满足性问题,继而使用电路解算器解决问题.同时,注意各个子问题间的有用隐含信息的共享,减小了SAT推理的搜索空间.实验结果表明,该算法是实用有效的. 展开更多
关键词 等价性验证 输出分组 电路可满足性
下载PDF
面向等价性验证的锁存器匹配算法 被引量:2
3
作者 郑飞君 杨军 +1 位作者 葛海通 严晓浪 《浙江大学学报(工学版)》 EI CAS CSCD 北大核心 2006年第8期1293-1296,共4页
为了克服现有等价性验证技术中难以精确匹配锁存器的局限性,提出了一种结合多种方法的新型锁存器匹配算法.该算法结合任意模拟、局部二叉判决图、目标模拟3种方法来匹配锁存器,并使用了类似滤波器的思想,任意模拟对锁存器作初步快速匹配... 为了克服现有等价性验证技术中难以精确匹配锁存器的局限性,提出了一种结合多种方法的新型锁存器匹配算法.该算法结合任意模拟、局部二叉判决图、目标模拟3种方法来匹配锁存器,并使用了类似滤波器的思想,任意模拟对锁存器作初步快速匹配,提出的局部二叉判决图技术降低了发生内存爆炸的可能性,目标模拟则针对性地对锁存器作进一步的划分.ISCAS89电路实验结果表明,该算法与模拟和自动测试矢量生成等方法相比,在运行时间、占用内存和匹配精度等方面均体现出有效性,可用于处理较大规模的时序电路验证问题. 展开更多
关键词 等价性验证 锁存器匹配 局部二叉判决图 目标模拟
下载PDF
一种形式化验证方法:模型检验 被引量:17
4
作者 杨军 葛海通 +1 位作者 郑飞君 严晓浪 《浙江大学学报(理学版)》 CAS CSCD 北大核心 2006年第4期403-407,共5页
模型检验作为一种形式化验证方法,近年来在各种硬件、软件设计中得到了广泛应用.文中首先介绍了描述系统行为的Kripke结构和描述系统性质的CTL逻辑,然后介绍了模型检验中常用的两种算法:标记算法和基于固定点的算法,最后介绍了为避免内... 模型检验作为一种形式化验证方法,近年来在各种硬件、软件设计中得到了广泛应用.文中首先介绍了描述系统行为的Kripke结构和描述系统性质的CTL逻辑,然后介绍了模型检验中常用的两种算法:标记算法和基于固定点的算法,最后介绍了为避免内存爆炸而引入的符号模型检验技术. 展开更多
关键词 模型检验 KRIPKE结构 CTL逻辑 标记 固定点 符号模型检验
下载PDF
结合二叉判决图和布尔可满足性的等价性验证算法 被引量:8
5
作者 严晓浪 郑飞君 +1 位作者 葛海通 杨军 《电子学报》 EI CAS CSCD 北大核心 2004年第8期1233-1235,共3页
本文提出了一种结合二叉判决图BDD和布尔可满足性SAT的新颖组合电路等价性验证技术 .算法是在与 /非图AIG中进行推理 ,并交替使用BDD扩展和基于电路SAT解算器简化电路 .如尚未解决 ,将用基于合取范式SAT解算器进行推理 .与已有算法相比... 本文提出了一种结合二叉判决图BDD和布尔可满足性SAT的新颖组合电路等价性验证技术 .算法是在与 /非图AIG中进行推理 ,并交替使用BDD扩展和基于电路SAT解算器简化电路 .如尚未解决 ,将用基于合取范式SAT解算器进行推理 .与已有算法相比主要有如下改进 :在AIG中结合多种引擎进行简化 ,不存在误判可能 ;充分利用了基于电路解算器和基于合取范式解算器各自优点 ,减小了SAT推理的搜索空间 .实验结果表明了本算法的有效性 . 展开更多
关键词 等价性验证 与/非图 孤立节点 二叉判决图 可满足性解算器
下载PDF
结合通用割集和专用割集的组合电路验证方法 被引量:1
6
作者 杨军 郑飞君 +2 位作者 卢永江 葛海通 严晓浪 《浙江大学学报(工学版)》 EI CAS CSCD 北大核心 2006年第9期1511-1515,共5页
为了提高组合电路的等价性验证速度,提出了一种利用电路内部等价信息的新型验证方法.该方法结合了通用割集和专用割集.从原始输出进行回溯得到通用割集,用通用割集验证所有候选等价点(CEP)的等价性.从特定候选等价点进行回溯得到专用割... 为了提高组合电路的等价性验证速度,提出了一种利用电路内部等价信息的新型验证方法.该方法结合了通用割集和专用割集.从原始输出进行回溯得到通用割集,用通用割集验证所有候选等价点(CEP)的等价性.从特定候选等价点进行回溯得到专用割集,通过消除高层次结点间的依赖关系对专用割集进行优化,用专用割集验证特定候选等价点的等价性.实验结果表明,与传统依赖性处理策略相比,该验证方法中的依赖性处理策略减少了验证时间.与只基于通用割集或专用割集的验证方法相比,该方法可以使组合电路的验证速度明显提高. 展开更多
关键词 形式验证 通用割集 专用割集 依赖性
下载PDF
高粉煤灰掺量低热微膨胀水泥的研究 被引量:3
7
作者 蒋永惠 闫春霞 +1 位作者 郑飞君 王新频 《水泥》 CAS 1996年第2期12-17,共6页
采用正交试验对粉煤灰低热微膨胀水泥进行配比优选,通过提高粉磨细度,使用高温煅烧石膏,掺加复合外加剂等方法,成功地研制出粉煤灰低热微膨胀水泥(粉煤灰掺量超过60%)。通过X射线衍射(XRD)、扫描电镜(SEM)和水化热... 采用正交试验对粉煤灰低热微膨胀水泥进行配比优选,通过提高粉磨细度,使用高温煅烧石膏,掺加复合外加剂等方法,成功地研制出粉煤灰低热微膨胀水泥(粉煤灰掺量超过60%)。通过X射线衍射(XRD)、扫描电镜(SEM)和水化热测定等现代测试技术,深入探索了该水泥的水化机理。研究表明:粉煤灰中玻璃体受机械和化学等多种活化后,火山灰反应加速,生成较多的钙矾石和C─S─H凝胶,形成致密网络状的水泥石结构,有效地改善了该水泥的各种性能。 展开更多
关键词 膨胀水泥 低热微膨胀 粉煤灰 复合外加剂
下载PDF
一种避免内存爆炸的组合电路等价性验证方法
8
作者 杨军 卢永江 +2 位作者 葛海通 郑飞君 严晓浪 《电路与系统学报》 CSCD 北大核心 2007年第3期21-25,共5页
割集在组合电路等价性验证中得到了广泛的应用,已有的方法常构造能将整个电路一分为二的割集,虽然这种割集在验证后续节点时可以重用已构建的BDD,但它的排序对大多数后续节点都很差,容易引起内存爆炸问题。本文中的割集只针对要验证等... 割集在组合电路等价性验证中得到了广泛的应用,已有的方法常构造能将整个电路一分为二的割集,虽然这种割集在验证后续节点时可以重用已构建的BDD,但它的排序对大多数后续节点都很差,容易引起内存爆炸问题。本文中的割集只针对要验证等价性的某一对点,避免了上述问题。ISCAS85的实验结果表明了它的有效性。 展开更多
关键词 等价性验证 BDD 割集
下载PDF
结合半加图的算术电路等价性验证技术
9
作者 翁延玲 葛海通 +1 位作者 严晓浪 郑飞君 《浙江大学学报(工学版)》 EI CAS CSCD 北大核心 2008年第8期1345-1349,1403,共6页
为了克服现有等价性验证技术难以快速验证复杂算术电路的局限性,提出了一种利用综合引擎分析并再现算术电路优化过程的算法.该算法结合了乘法器的编码方式识别技术、加法电路的半加树提取技术和部分积加法电路的架构识别技术来提取乘法... 为了克服现有等价性验证技术难以快速验证复杂算术电路的局限性,提出了一种利用综合引擎分析并再现算术电路优化过程的算法.该算法结合了乘法器的编码方式识别技术、加法电路的半加树提取技术和部分积加法电路的架构识别技术来提取乘法电路的实现结构,以此生成与实现电路结构相似且逻辑正确的网表.针对算术电路结构的相似性,仅分析低位输出的电路架构以降低算法复杂度.实验结果表明,与传统的算术电路验证算法相比,该算法可以明显提高算术电路的验证速度,并且可以直接结合到现有的寄存器传输级(RTL)和门级网表的验证流程中,从而提高了算术电路的验证能力. 展开更多
关键词 综合 等价性验证 算术电路 半加树
下载PDF
关于后摩尔时代我国集成电路制造领域的一些思考 被引量:1
10
作者 吴汉明 郑飞君 《Engineering》 SCIE EI CAS CSCD 2023年第4期33-39,共7页
1.Background,As one of the fundamental and core industries of modern information technology,the integrated circuit(IC)is a basic and leading industry that is closely related to overall global economic and social devel... 1.Background,As one of the fundamental and core industries of modern information technology,the integrated circuit(IC)is a basic and leading industry that is closely related to overall global economic and social development.The global semiconductor industry is poised for a decade of growth and is projected to become a trillion-dollar industry by 2030(Fig.1[1]).Technological level and industrial scale are important indicators for evaluating the degree of modernization and comprehensive national strength of a country or region.Hailed as the“industrial food”for a country,IC is the foundation for cultivating and developing strategic emerging industries and promoting the deep integration of informatization and industrialization.Demand for both cutting-edge chips and high-reliability chips continues to be strong in applications deployed throughout the field,from Industry 4.0 to automotive electronics,artificial intelligence,and so forth.As the focus of current international competition,IC also plays a broad and key role in promoting national economic development and social progress,improving people’s living standards,and ensuring national security.The current competition is not related to a certain technology node or single specific technology.Rather,this core competitiveness is the overall strength of the IC industry chain and relies on the ability to track the dynamic targets of industrial development,which fully depends on the support of the global high-end basic industry. 展开更多
关键词 DOLLAR INDUSTRY STRATEGIC
下载PDF
上一页 1 下一页 到第
使用帮助 返回顶部