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

论文摘要

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

论文目录

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