代数化符号模拟验证的应用研究

发布时间：2017-07-30 20:19

  本文关键词：代数化符号模拟验证的应用研究

  更多相关文章： 符号模拟 断言验证 代数符号计算 属性描述语言 数字系统验证

【摘要】：传统的模拟验证技术与形式化验证方法是集成电路验证理论中最重要的两类验证方法,模拟验证技术原理简单,可操作性强,应用范围广,但无法进行完全测试：形式化方法具备完全性,但应用范围受到局限。 而模拟技术与形式化方法混合验证是近十几年来验证领域方兴未艾的重要研究方向之一,它有机地结合了模拟验证方法的动态性与形式化方法无需测试矢量的优点,是一个既有理论依据又能实际运用的方法。本文重点研究代数符号计算理论与模拟验证方法的交叉与融合。 在数字集成电路设计验证领域,符号模拟通过系统的动态符号执行检查预设条件或断言的真假来进行功能的正确性验证,是一种在工程实践应用中发挥了重要作用的有效方法。目前的符号模拟特别是高层符号模拟方法,存在着符号表达结果难以判定和空间爆炸等问题,使得其本身的构建理论和应用都受到了很大的限制。基于此,本文将代数符号计算方法运用到符号模拟验证领域,作为可验证计算的核心计算方法。并针对模拟验证计算的特点,着重研究基于断言验证方法学下符号模拟算法的代数化方法面临的理论问题,分别提出基于吴特征列方法和基于Groebner基的代数化算法。主要工作和取得的研究成果如下： (1)PSL布尔层的代数化符号模拟断言验证 提出了将基于PSL布尔层断言验证的符号模拟验证问题转化为符号计算理论适用的代数问题方法,并且初步建立代数化的模拟验证的基本理论框架。首先将待验证的布尔断言表达式和系统符号执行的结构转换为适当的非线性代数方程组的形式,本文采用基于数据流的多项式代数表达方法。根据符号代数的特点,将PSL中逻辑规范中关于布尔逻辑的定义进行了修改,定义了信号逻辑与断言逻辑以适应断言验证的要求。PSL布尔层断言虽然简单,但却是本文验证方法的起始点和基础,在布尔断言与组合电路模型分别代数化的基础上,给出相应的Groebner基方法和吴方法的验证算法,并通过实例验证。 (2)PSL时序层的代数化符号模拟断言验证 提出了将基于PSL时序层断言验证的符号模拟验证问题转化为符号计算理论适用的代数问题方法,并且初步建立时序电路代数化模拟验证的基本理论框架。针对符号模拟的特点以及通过Symbolic Trajectory Evaluation (STE)技术对比,重点研究符号断言的刻画和验证问题。由于布尔值的真与假与电路信号的高与低在当前PSL规范中未加以区分,从而导致符号代数验证方法无法实施,所以首先定义了SERE的简单约束子集以及对每种时序操作符代数化,在此基础上,给出时序电路在时帧展开基础上参数化多项式集合的建模方法。最后借鉴SymbolicTrajectory Evaluation (STE)技术的断言图方法来解决PSL中时序层断言的刻画和验证问题。 (3) SystemVerilog断言的代数化符号模拟断言验证 提出了将基于SystemVerilog断言验证的符号模拟验证问题转化为符号计算理论适用的代数问题方法,首先定义了SystemVerilog断言的约束子集,并给出了每个序列以及属性的操作符代数化步骤。然后在布尔断言以及时序电路断言验证的基础上,给出基于多项式理论的电路模型与SystemVerilog断言模型建模方法,将基于模拟的验证问题转换为符号代数计算问题。最后给出相应的Groebner基方法和吴方法的验证算法,并通过实例验证。 综上所述,本文基于断言验证方法学,将符号模拟技术代数化,提出一种集成电路代数化符号模拟的断言验证方法。该方法在代数符号计算与形式化验证方法以及模拟技术之间搭建起一座桥梁,将传统模拟验证技术、形式化方法、代数符号计算相融合,有效避免纯形式化方法与传统电路验证技术之间的割裂,并为集成电路验证理论提供了一种新的解决思路。
【关键词】：符号模拟 断言验证 代数符号计算 属性描述语言 数字系统验证
【学位授予单位】：北京交通大学
【学位级别】：博士
【学位授予年份】：2015
【分类号】：O151
【目录】：

• 致谢5-6
• 摘要6-8
• ABSTRACT8-14
• 1 绪论14-28
• 1.1 研究背景及意义14-18
• 1.2 相关研究18-24
• 1.2.1 验证技术18-20
• 1.2.2 断言验证方法学20-23
• 1.2.3 代数化验证理论23-24
• 1.3 论文的研究内容24-26
• 1.4 论文的结构安排26-28
• 2 相关知识28-46
• 2.1 符号计算28-33
• 2.1.1 Groebner基方法28-31
• 2.1.2 吴方法31-33
• 2.2 符号模拟验证方法33-40
• 2.2.1 基本思想35-38
• 2.2.2 基于STE的符号模拟38-40
• 2.3 形式化验证方法40-45
• 2.3.1 定理证明方法41-42
• 2.3.2 等价性检验42-43
• 2.3.3 模型检验43-45
• 2.4 本章小结45-46
• 3 基于代数化符号模拟的布尔层PSL性质验证46-60
• 3.1 引言46-47
• 3.2 PSL布尔层及其代数表示47-49
• 3.3 布尔层组合电路建模49-50
• 3.4 基于Groebner基验证算法及实例50-54
• 3.4.1 基于Groebner基的验证算法50-52
• 3.4.2 基于Groebner基的验证实例52-54
• 3.5 基于吴方法验证算法及实例54-59
• 3.5.1 基于吴方法的验证算法框架54-57
• 3.5.2 基于吴方法的验证实例57-59
• 3.6 本章小结59-60
• 4 基于代数化符号模拟的SERE时序断言验证60-82
• 4.1 引言60-61
• 4.2 基于周期的符号模拟61-62
• 4.3 系统多项式表示模型62-67
• 4.3.1 算术、逻辑以及分支单元建模62-63
• 4.3.2 时序单元建模及展开63-65
• 4.3.3 时序操作符建模65-67
• 4.4 SERE转换方法67-70
• 4.4.1 代数化过程67-68
• 4.4.2 布尔层建模68-70
• 4.5 基于Groebner基算法框架70-74
• 4.5.1 基于定理证明的验证理论70-71
• 4.5.2 验证算法71-74
• 4.6 基于Groebner基验证实例分析74-77
• 4.6.1 电路及PSL建模74-76
• 4.6.2 使用Maple进行断言验证76-77
• 4.7 基于吴方法的SERE时序断言验证77-81
• 4.7.1 基于吴方法验证的算法框架77-79
• 4.7.2 基于吴方法验证的实例研究79-81
• 4.8 本章小结81-82
• 5 基于代数化符号模拟的SystemVerilog的并发断言验证82-116
• 5.1 引言82-83
• 5.2 SystemVerilog基础83-85
• 5.3 同步数字系统以及多项式表示85-87
• 5.3.1 组合逻辑模型85
• 5.3.2 时序单元建模85-86
• 5.3.3 符号模拟系统模型86-87
• 5.4 多项式集合表示SVA表达式87-96
• 5.4.1 多项式概念以及代数化87-88
• 5.4.2 时间区间及其展开模型88-89
• 5.4.3 时序的深度计算89-91
• 5.4.4 时序操作符建模91-93
• 5.4.5 局部变量表示及属性操作符建模93-95
• 5.4.6 SystemVerilog断言的约束子集95-96
• 5.5 基于Groebner基的SVA验证理论及算法96-98
• 5.5.1 基于Groebner基断言验证原理96-97
• 5.5.2 验证算法框架97-98
• 5.6 基于Groebner基断言验证实例98-103
• 5.6.1 电路及断言建模98-101
• 5.6.2 使用Maple进行计算101-103
• 5.7 基于吴方法的SVA验证理论及算法103-104
• 5.7.1 基于吴方法的SVA验证原理103-104
• 5.7.2 基于吴方法的SVA验证算法104
• 5.8 基于吴方法的SVA实例验证及实验104-113
• 5.8.1 电路及断言建模105-106
• 5.8.2 使用MMP验证断言106-107
• 5.8.3 经典仲裁器电路的实验107-112
• 5.8.4 实验讨论112-113
• 5.9 本章小结113-116
• 6 总结与展望116-120
• 6.1 研究工作总结116-118
• 6.2 未来工作展望118-120
• 参考文献120-126
• 作者简历及攻读博士学位期间取得的研究成果126-132
• 学位论文数据集132

【参考文献】

中国期刊全文数据库 前10条

1 吴文俊;ON THE DECISION PROBLEM AND THE MECHANIZATION OF THEOREM-PROVING IN ELEMENTARY GEOMETRY[J];Science in China,Ser.A;1978年02期

2 杨志;马光胜;张曙;;基于多项式符号代数方法的高层次数据通路的等价验证[J];计算机研究与发展;2009年03期

3 袁智德,宣国良;我国集成电路设计业发展的战略选择[J];经济理论与经济管理;2001年05期

4 马博;韩俊刚;;采用PSL的基于断言的验证[J];计算机工程;2007年02期

5 闫炜;吴尽昭;高新岩;;符号模拟[J];计算机工程;2007年20期

6 郑伟伟;吴为民;边计年;;基于线性规划的RTL可满足性求解和性质检验[J];计算机辅助设计与图形学学报;2006年04期

7 杨志;马光胜;冯刚;邵晶波;;应用吴方法进行高层次定界模型检验[J];计算机辅助设计与图形学学报;2008年02期

8 虞蕾;赵宗涛;;PSL逻辑及验证技术研究进展与展望[J];计算机应用研究;2010年07期

9 徐善锋,初秀琴,李玉山,来新泉;21世纪微电子芯片设计技术发展方向[J];微电子学;2001年05期

10 ;A CHARACTERISTIC SET METHOD FOR SOLVING BOOLEAN EQUATIONS AND APPLICATIONS IN CRYPTANALYSIS OF STREAM CIPHERS[J];Journal of Systems Science and Complexity;2008年02期

，

本文编号：595963