基于BDD的组合电路等价性检验方法 被引量：4

1

作者 李光辉 邵明 李晓维 《微电子学与计算机》 CSCD 北大核心 2003年第2期48-51,55,共5页

文章分析了目前常用的等价性检验方法的特点,包括功能性和结构性的验证方法;讨论了基于二叉判决图(BDD)的组合电路等价性检验方法,并分析了等价性检验过程中的误判问题及其消除方法;然后给出了一种关于带黑匣子的部分实现的隐式等价性... 文章分析了目前常用的等价性检验方法的特点,包括功能性和结构性的验证方法;讨论了基于二叉判决图(BDD)的组合电路等价性检验方法,并分析了等价性检验过程中的误判问题及其消除方法;然后给出了一种关于带黑匣子的部分实现的隐式等价性检验方法,实验结果表明了该方法的有效性。 展开更多

关键词 BDD 形式验证 等价性检验 符号模拟 三叉判决图 组合电路 专用集成电路

下载PDF 职称材料

基于符号模拟和变量划分的SAT算法 被引量：3

2

作者 闫炜 吴尽昭 高新岩 《四川大学学报（工程科学版）》 EI CAS CSCD 北大核心 2008年第3期121-125,共5页

针对SAT算法中回溯次数较多的问题,采用基于符号模拟和变量划分的方法来解决其不足。基于符号模拟和变量划分的SAT算法将一个较大的CNF分解为两个子集,每个子集所包含的变量又划分为两个互不相交的子集,仅对那些无法判断的子集,赋以符号... 针对SAT算法中回溯次数较多的问题,采用基于符号模拟和变量划分的方法来解决其不足。基于符号模拟和变量划分的SAT算法将一个较大的CNF分解为两个子集,每个子集所包含的变量又划分为两个互不相交的子集,仅对那些无法判断的子集,赋以符号值,从而限定了赋予符号值的变量范围,即可减少算法的回溯次数,又能降低内存占用率。理论及实验结果均证明,该算法是合理且有效的。 展开更多

关键词 SAT 符号模拟 合取范式 变量划分

下载PDF 职称材料

符号模拟 被引量：2

3

作者 闫炜 吴尽昭 高新岩 《计算机工程》 CAS CSCD 北大核心 2007年第20期27-29,33,共4页

符号模拟将模拟验证从布尔值扩展到符号领域,是集成电路验证行业中的重要分支。符号方法将符号值加到待验证电路的基本输入端,依次计算每个结点的布尔函数,直到在电路的输出端得到由这些初始符号变量组成的布尔表达式,并判断其是否具有... 符号模拟将模拟验证从布尔值扩展到符号领域,是集成电路验证行业中的重要分支。符号方法将符号值加到待验证电路的基本输入端,依次计算每个结点的布尔函数,直到在电路的输出端得到由这些初始符号变量组成的布尔表达式,并判断其是否具有所期望的特征。该文介绍了符号模拟的发展过程、基本技术及其所面临的BDD爆炸问题,并对消除该问题的两种技术:近似值法和参数方法,进行了讨论。介绍了具有一定自动机处理能力的符号轨迹评价方法。 展开更多

关键词 符号模拟 近似值 参数方法 符号轨迹评价方法

下载PDF 职称材料

文献分类法标记符号的发展趋势

4

作者 吴声亮 《新世纪图书馆》 1986年第4期26-27,共2页

我认为标记符号发展趋势是:一、配号以延展为主,层累为辅。知识体系的层累关系一直是由正附表类目的字形和缩格来体现的,不需要符号模拟,只要有简明的代号就行了。一切已经定形和发展较快的科学体系都可以延展配号,在同位类上、中、下... 我认为标记符号发展趋势是:一、配号以延展为主,层累为辅。知识体系的层累关系一直是由正附表类目的字形和缩格来体现的,不需要符号模拟,只要有简明的代号就行了。一切已经定形和发展较快的科学体系都可以延展配号,在同位类上、中、下予留空号,如有五个同位类,用单元序号O—9配号可只用3,4,6,7,8空出1,2,5,9作发展。 展开更多

关键词 文献分类法 标记符号 发展趋势 配号 符号序列 同位类 符号模拟 符号空间 科学体系 知识体系

下载PDF 职称材料

模拟集成电路的符号模拟——符号表达式及其生成

5

作者 许宁 《新乡师范高等专科学校学报》 2000年第4期31-33,共3页

文章系统阐述了符号模拟方法的基本思想、实现过程，并与数值模拟方法进行了比较。

关键词 符号表达式 符号模拟 数值模拟 模拟集成电路

下载PDF 职称材料

片上系统高层等价性检验研究进展 被引量：1

6

作者 胡健 李暾 李思昆 《计算机辅助设计与图形学学报》 EI CSCD 北大核心 2016年第3期371-380,共10页

针对近年来SoC领域的工作,首先分析了高层等价性检验的难点;然后从算法类型归类角度对各种高层等价性检验方法进行了概述评论,同时分析了各类算法的优缺点和现有算法的主要技术手段;最后讨论了SoC高层等价性检验方法目前面临的挑战,并... 针对近年来SoC领域的工作,首先分析了高层等价性检验的难点;然后从算法类型归类角度对各种高层等价性检验方法进行了概述评论,同时分析了各类算法的优缺点和现有算法的主要技术手段;最后讨论了SoC高层等价性检验方法目前面临的挑战,并对该领域今后的研究方向进行了展望. 展开更多

关键词 等价性检验 带数据通路的有限状态机 符号模拟 形式化方法

下载PDF 职称材料

基于符号模拟和约束逻辑编程的RTL级Verilog谓词抽象方法 被引量：1

7

作者 李暾 屈婉霞 +2 位作者 郭阳 刘功杰 李思昆 《计算机学报》 EI CSCD 北大核心 2007年第7期1138-1144,共7页

利用人工智能最新研究成果——约束逻辑编程对Verilog描述进行谓词抽象,并与目前基于SAT的方法进行了比较．首先通过符号模拟建立Verilog的形式化模型,然后结合要抽象的谓词,将谓词抽象问题转化为约束逻辑编程问题并进行求解．该方法的... 利用人工智能最新研究成果——约束逻辑编程对Verilog描述进行谓词抽象,并与目前基于SAT的方法进行了比较．首先通过符号模拟建立Verilog的形式化模型,然后结合要抽象的谓词,将谓词抽象问题转化为约束逻辑编程问题并进行求解．该方法的优点是在计算抽象系统时,不需要像基于SAT的方法那样将字级约束打散成位级约束,求解效率显著提高;提供了一个统一的框架用于描述各种约束．实验结果表明,与基于SAT的抽象技术相比,基于约束逻辑编程的抽象方法的求解速度有显著提高． 展开更多

关键词 谓词抽象 Verilog约束逻辑编程 模型检验 符号模拟

下载PDF 职称材料

卦象:哲学性与艺术性的符号——刘纲纪《周易美学》述评

8

作者 邹元江 《中国文化研究》 CSSCI 1995年第2期143-145,4,共4页

由于《周易》本是一本讲占筮的书,《易传》又试图给它作一种系统的解释说明,所以,在古代乃至到了现代,一提起《周易》就难以拂去由于其保留有由巫术而来的神秘观念和迷信色彩。在刘纲纪先生看来,千百年来对于《周易》的研究,总的而论却... 由于《周易》本是一本讲占筮的书,《易传》又试图给它作一种系统的解释说明,所以,在古代乃至到了现代,一提起《周易》就难以拂去由于其保留有由巫术而来的神秘观念和迷信色彩。在刘纲纪先生看来,千百年来对于《周易》的研究,总的而论却正是发展了它的神秘主义、甚至迷信色彩的一面(包括大陆八十年代“周易热”中出现的所谓“预测学”、“相面术”、“算命术”、“风水学”等一类伪科学书籍),而掩盖了它的自然唯物主义的光辉。比如对被西方视为“东方神秘主义”的“图象语言”(黑格尔说是“图画式的概念”)——“卦象” 展开更多

关键词 《周易》 艺术性 刘纲纪 中国艺术 哲学性质 符号模拟 卦象 《易传》 苏珊·朗格 自然唯物主义

原文传递

RTL级符号模拟系统

9

作者 况翔 宋国新 《华东理工大学学报（自然科学版）》 EI CAS CSCD 北大核心 2004年第6期673-676,共4页

给出了一组从VerilogHDL到可符号执行代码的转换规则,并且提出了ProcessQueue机制。通过运用符号模拟的方法和二叉决策图技术,给出了一个RTL级的符号模拟系统的实现方法。本系统能够有效地对RTL级Verilog算法进行符号模拟,并且支持带有... 给出了一组从VerilogHDL到可符号执行代码的转换规则,并且提出了ProcessQueue机制。通过运用符号模拟的方法和二叉决策图技术,给出了一个RTL级的符号模拟系统的实现方法。本系统能够有效地对RTL级Verilog算法进行符号模拟,并且支持带有时间延迟的If结构的符号模拟。 展开更多

关键词 二叉决策图 VERILOG硬件描述语言 符号模拟

下载PDF 职称材料

基于符号模拟的电路中错误诊断方法研究

10

作者 齐芳 吴尽昭 《现代电子技术》 2009年第16期1-3,7,共4页

错误诊断是在逻辑芯片中预测潜在错误点的过程。为了快速有效地诊断电路中的错误,提出一种将符号模拟技术应用到基于区域模型的错误诊断法上的新思想,具体方法是通过对要诊断的电路进行区域划分,然后利用符号模拟方法依据两种测量标准... 错误诊断是在逻辑芯片中预测潜在错误点的过程。为了快速有效地诊断电路中的错误,提出一种将符号模拟技术应用到基于区域模型的错误诊断法上的新思想,具体方法是通过对要诊断的电路进行区域划分,然后利用符号模拟方法依据两种测量标准对各个区域候选者进行可疑度的等级排序,从而对电路中所含错误进行判断。可疑度越高的区域,其作为错误候选者的可能性越大。该方法利用符号模拟技术,不需要对向量空间进行穷尽的列举,因而在空间和时间上是有效的。 展开更多

关键词 区域模型 符号模拟 错误诊断 测量标准

下载PDF 职称材料

计算机辅助技术

11

《电子科技文摘》 2000年第11期131-133,共3页

Y2000-62352-24 0019379硅上嵌入系统的计算机辅助设计技术=CAD tech-niques for embedded systems-on-silicon[会,英]/Wolf,W.//1999 IEEE International Conference on ComputerDesign.—24～29(PC)Y2000-62352-451 0019380有效状态... Y2000-62352-24 0019379硅上嵌入系统的计算机辅助设计技术=CAD tech-niques for embedded systems-on-silicon[会,英]/Wolf,W.//1999 IEEE International Conference on ComputerDesign.—24～29(PC)Y2000-62352-451 0019380有效状态空间研究=Session 2.3.2:efficient state-space exploration[会,英]//1999 IEEE InternationalConference on Computer Design.—451～474(PC)本部分收入3篇论文。题名为:利用状态指令改进证明搜索,出现环路时利用非说明符号模拟证明调度和不变检验的有效定点计算。 展开更多

关键词 计算机辅助设计技术 开发与应用 不变检验 方案设计 嵌入系统 符号模拟 定点计算 计算机辅助技术 计算机研究 铁路线路

原文传递

面向敏捷硬件设计的符号模拟器设计与实现

12

作者 邹鸿基 李暾 +1 位作者 罗丹 方雨德 《计算机工程与科学》 CSCD 北大核心 2021年第12期2098-2104,共7页

敏捷硬件设计方法中,RTL建模常使用自定义的描述语言,并将设计转换为某种中间格式,为设计验证带来了新挑战。符号模拟技术是(限界)模型检验、等价性检查和测试生成等验证技术的基础,为构建敏捷硬件设计方法验证技术基础,针对PyRTL语言... 敏捷硬件设计方法中,RTL建模常使用自定义的描述语言,并将设计转换为某种中间格式,为设计验证带来了新挑战。符号模拟技术是(限界)模型检验、等价性检查和测试生成等验证技术的基础,为构建敏捷硬件设计方法验证技术基础,针对PyRTL语言及其中间格式,设计并实现了一个符号模拟器。介绍了符号模拟器的设计原理、转换规则等关键技术。实验结果表明了所实现的符号模拟器的正确性。 展开更多

关键词 符号模拟器 PyRTL 敏捷硬件设计 验证

下载PDF 职称材料

一种自动验证网络安全协议的互模拟方法 被引量：1

13

作者 杨军 孟海涛 《内江师范学院学报》 2008年第12期56-58,共3页

为了解决进程接收具体信息的输入所带来的无穷种迁移问题,采用一种称为"符号化"的方法,提出了进程符号环境和符号化和格局标号迁移语义,为Spi演算设计了符号互模拟关系—符号Reded互模拟.结果表明:该符号互模拟关系对传统的... 为了解决进程接收具体信息的输入所带来的无穷种迁移问题,采用一种称为"符号化"的方法,提出了进程符号环境和符号化和格局标号迁移语义,为Spi演算设计了符号互模拟关系—符号Reded互模拟.结果表明:该符号互模拟关系对传统的互模拟关系是可靠的,符号化的标号转移语义将进程无穷输入导致的迁移限期为有穷种迁移.因此使得基于该关系的安全协议自动验证算法得以实现. 展开更多

关键词 密文通信协议 进程演算 符号互模拟

下载PDF 职称材料

非对称_(χ-)演算的符号互模拟验证算法

14

作者 黄银强 钟发荣 《微电子学与计算机》 CSCD 北大核心 2006年第9期193-196,共4页

非对称χ-演算是一种移动计算模型。文介绍非对称χ-演算的语法和符号操作语义,给出非对称χ-演算的符号互模拟的验证算法,该算法根据算法输出的谓词等式系,求解最大符号解。并证明算法正确性,这在一定程度上为今后的自动机验证提供了... 非对称χ-演算是一种移动计算模型。文介绍非对称χ-演算的语法和符号操作语义,给出非对称χ-演算的符号互模拟的验证算法,该算法根据算法输出的谓词等式系,求解最大符号解。并证明算法正确性,这在一定程度上为今后的自动机验证提供了理论基础。 展开更多

关键词 进程代数 非对称X-演算 符号互模拟 符号迁移图 验证算法

下载PDF 职称材料

数据传送进程的符号互模拟

15

作者 林惠民 《软件学报》 EI CSCD 北大核心 1995年第A01期1-9,共9页

本文提出数据传送进程的符号迁移语义，引入符号互模拟的概念，证明了两个进程在传统意义下互模拟当且仅当它们符号互模拟。我穷域上的数据传送进程的传统迁移图是无穷的而其中相当的一部分的符号迁移图是有穷的，文章的结果为在有穷时... 本文提出数据传送进程的符号迁移语义，引入符号互模拟的概念，证明了两个进程在传统意义下互模拟当且仅当它们符号互模拟。我穷域上的数据传送进程的传统迁移图是无穷的而其中相当的一部分的符号迁移图是有穷的，文章的结果为在有穷时间和空间内判定这类进程的互模拟关系开辟了可能性。 展开更多

关键词 进程代数 数据传送进程 符号互模拟 程序

下载PDF 职称材料

符号化模拟电路仿真器的图形界面开发与应用

16

作者 李骥 《信息技术》 2010年第5期114-117,120,共5页

符号化模拟电路仿真器可以快速导出模拟电路频域指标关于每个电路参数的解析表达式。介绍了基于符号化仿真器开发的图形界面。它能以三维图形的方式实时直观地呈现出各种电路设计指标关于多个电路参数的灵敏度,突破了传统数值电路仿真... 符号化模拟电路仿真器可以快速导出模拟电路频域指标关于每个电路参数的解析表达式。介绍了基于符号化仿真器开发的图形界面。它能以三维图形的方式实时直观地呈现出各种电路设计指标关于多个电路参数的灵敏度,突破了传统数值电路仿真工具在多参数协同优化应用中的局限性,使设计者能快速准确地选择适当的参数组合以达到最佳设计指标,可应用在模拟集成电路生产良率提升,芯片面积、功耗优化等方面。 展开更多

关键词 符号化模拟电路仿真器 GUI OPENGL

下载PDF 职称材料