学位论文 > 优秀研究生学位论文题录展示

并发的广义符号轨迹赋值的研究

作　者: 徐忠林
导　师: 杨国武
学　校: 电子科技大学
专　业: 计算机应用技术
关键词: 形式化验证 GSTE 进程代数并发系统
分类号: TN402
类　型: 硕士论文
年　份: 2010年
下　载: 6次
引　用: 0次
阅　读: 论文下载

内容摘要

随着数字逻辑设计的规模越来越大,复杂度越来越高,功能验证已成为设计过程中的首要瓶颈。在过去几十年中,人们对于数字电路顺序行为的验证进行了深入而广泛的研究并提出了许多行之有效的验证方法,主要分为基于模拟的和基于形式方法的验证技术[1]。然而,数字集成电路是典型的并发系统,如何实现对并发行为的有效验证就成为保证数字电路功能正确性的关键因素。本文在了解国内外形式验证技术研究成果的基础上,对当前主流形式化验证方法中的广义符号轨迹赋值(generalized symbolic trajectory evaluation, GSTE)[2-3]验证方法进行了深入的研究和拓展,修改断言图及其验证算法使之能更简洁的描述和验证数字电路的并发性质。本文在研究方法上,首先深入学习和研究了广义符号轨迹赋值相关的理论包括电路模型、电路模拟方法,符号轨迹赋值[4-5]和广义符号轨迹赋值的核心算法。并通过实例展示了断言图描述电路并发性质时的不足。其次,学习和研究了进程代数[6- 8]的表示方法后,本文提出了一个基于广义符号轨迹赋值的组合方法来克服断言图不能简洁描述电路并发性质的限制。(1)提出了一个规范语言,它能用组合的方式简洁的描述系统的并发行为。这种组合是逻辑的,不依赖于对系统实现细节的深入理解。这个语言是对广义符号轨迹赋值规范语言的拓展,它引入了一个新的meet运算符,用类似于进程代数的方式表达。(2)针对新的断言图规范,本文对经典的广义符号轨迹赋值的算法进行了修改,该算法能直接深入规范的语法结构并建立从规范的语言元素到电路状态集合的模拟关系。本文设计了一个高效而实用的方法来直接验证并发规范。第三,在平台Forte平台环境[9]下利用FL语言对改进后的并发验证算法进行编码实现和测试。实验结果表明修改后的断言图和算法是有效的,在验证并发性质时确实能够减小断言图的复杂度。最后,对全文进行系统、全面的总结,指出了下一步研究和改善的方向。并展望了形式化验证算法在电路设计领域的良好应用前景。

全文目录

摘要  4-5
ABSTRACT  5-10
第一章绪论  10-19
  1.1 概述  10
  1.2 验证的基本概念和原理  10-13
    1.2.1 验证的基本概念  10-12
    1.2.2 验证的基本原理  12-13
  1.3 验证方法学  13-17
    1.3.1 基于模拟的验证  13-15
    1.3.2 基于形式方法的验证  15-17
  1.4 研究现状与研究内容  17-18
    1.4.1 研究现状  17
    1.4.2 主要工作  17-18
  1.5 论文组织  18-19
第二章广义符号轨迹赋值  19-39
  2.1 电路模型  19-21
    2.1.1 网表  19-20
    2.1.2 Kripke 结构  20-21
  2.2 电路模拟方法  21-25
    2.2.1 二值模拟  21-22
    2.2.2 三值模拟  22-24
    2.2.3 符号模拟  24-25
  2.3 符号轨迹赋值  25-28
    2.3.1 性质规范  25-26
    2.3.2 验证算法  26-28
  2.4 广义符号轨迹赋值  28-37
    2.4.1 断言图  28-30
    2.4.2 验证过程  30-37
  2.5 本章小结  37-39
第三章并发性质的刻画的研究  39-52
  3.1 问题来源  39-41
  3.2 进程代数  41-43
    3.2.1 进程代数简介  41
    3.2.2 通信系统演算CCS  41-43
  3.3 断言语言的研究  43-48
    3.3.1 基本概念  43-46
    3.3.2 meet 运算符  46-47
    3.3.3 并发规范  47-48
  3.4 并发规范模型检验算法设计  48-51
  3.5 本章小结  51-52
第四章并发验证算法的实现的研究  52-76
  4.1 Forte 验证环境  52-57
    4.1.1 Forte 简介  52-53
    4.1.2 Exlif 格式  53-54
    4.1.3 函数语言FL  54-57
  4.2 并发验证算法的实现  57-72
    4.2.1 软件框架  58-59
    4.2.2 算法流程  59-60
    4.2.3 BDD 处理技术  60-65
    4.2.4 参数化表示技术  65-66
    4.2.5 数据结构及关键源码  66-72
  4.3 验证实验  72-75
    4.3.1 三输入端电路  72-74
    4.3.2 投票机系统实例  74-75
  4.4 本章小结  75-76
第五章结论与展望  76-78
  5.1 研究总结  76-77
  5.2 研究展望  77-78
致谢  78-79
参考文献  79-83
个人简历及硕士期间研究成果  83-84
  个人简历  83
  获奖情况  83
  参与的科研项目  83-84

相似论文

基于SystemVerilog的URAT模块功能验证,TN402
基于进程代数的面向服务软件体系结构建模,TP393.09
ARINC 659通信总线的设计与实现,TP336
基于密钥链的认证邮件协议的扩展及形式化验证,TP393.08
基于进程代数的信息化建模与仿真,TP311.52
EFSOS模型验证技术和反向建模方法的研究与应用,TP311.53
一种并发系统建模中的同步控制机制,TP13
APLA语言并发机制的研究,TP312
Isabelle定理证明器的剖析及其在PAR方法/PAR平台中的应用,TP311.11
基于实时可视化数据挖掘的高并发性能监测系统设计与实现,TP274
基于行为的Web服务相容性与可替换性研究,TP393.09
基于情态演算的UML形式化验证与OCL约束自动生成研究,TP311.52
基于GSTE理论的抽象与细化问题的研究,TN47
基于GSTE理论的反例研究,TN402
600MHz YHFT-DX取指派发部件设计优化与物理设计,TP332
供应链条件下供应商评选模型的研究与设计,F274
通信距离受限的进程代数研究,TP301.1
基于Pi演算的Web服务组合技术研究,TP393.09
基于FeaVer的Kerberos形式化验证和改进,TP311.53
基于多项式符号代数的电路形式验证,TN402