时序逻辑电路的形式验证方法研究

发布时间：2021-10-10 13:44

　　近年来，由于电路规模不断增大和电路功能日趋复杂，使得大规模集成电路的设计很难保证逻辑设计的正确无误。为了设计和建立高可靠性的VLSI系统，必须对VLSI的设计和实现进行有效的验证。目前主要的验证方法有模拟验证和形式验证两种，模拟验证是当前工业界使用的主要方法，但是由于单纯的模拟验证已不能满足VLSI设计和制造的需要，形式验证的方法越来越引起人们的重视。 模型检验（Model checking）方法是一种很有前途的形式验证方法，它的验证方法是通过对有限状态空间的遍历来确认规范说明（Specification）是否得到满足。这种方法具有高度自动化，执行速度快，能产生反例来帮助调试等特点，比较适合于VLSI的验证。 有效地建立和表示时序逻辑电路的状态转移关系是应用模型检查方法验证时序逻辑电路的关键技术之一。作者详尽地讨论了如何用二元判决图（BDD）表示时序逻辑电路的状态转移关系，在此基础之上，作者考察了一种单位时延的电位异步时序电路，提出并实现了表示其稳定状态转移关系的算法。 符号模型检验（Symbolic Model checking）是时序逻辑模型检验的技术一种具体方法... 

【文章来源】：中国科学院大学(中国科学院计算技术研究所)北京市

【文章页数】：76 页

【学位级别】：硕士

【文章目录】：
摘要
Abstract
目录
第一章 综述
    1.1 引言
    1.2 验证的基本概念
    1.3 验证方法综述
        1.3.1 模拟验证
            1.3.1.1 模拟验证的基本原理
            1.3.1.2 事件驱动模拟和基于周期的模拟
            1.3.1.3 硬件加速和硬件仿真
            1.3.1.4 模拟验证的特点
        1.3.2 形式验证
            1.3.2.1 形式验证的基本过程
            1.3.2.2 模型检验
            1.3.2.3 定理证明
            1.3.2.4 形式验证方法与模拟验证方法的比较
第二章 二元判决图及其在电路验证中的应用
    2.1 引言
    2.2 二元判决图
        2.2.1 二元判决图的基本概念
        2.2.2 简化有序二元判决图(ROBDD)的性质
        2.2.3 目前对BDD研究的新进展
    2.3 符号模型检验的BDD表示和操作
        2.3.1 用BDD表示基本的布尔操作
        2.3.2 用BDD表示的量词操作
        2.3.3 用BDD表示集合和状态转移关系
第三章 符号模型检验技术
    3.1 引言
    3.2 计算树逻辑(CTL—Computation Tree Logic)
    3.3 Kripke结构上幂集运算的不动点特性
    3.4 符号模型检验技术
        3.4.1 用BDD表示被验证系统
        3.4.2 符号模型检验的基本算法
    3.5 公平性约束检验(Fairness Constraints)
第四章 用符号模型检验技术验证时序逻辑电路
    4.1 引言
    4.2 同步时序逻辑电路的BDD表示
    4.3 异步时序逻辑电路的BDD表示
第五章 符号模型检验系统的设计和实现
    5.1 引言
    5.2 SCSMV输入语言的语法规则和编译器的设计
        5.2.1 词法规则
        5.2.2 语法规则
    5.3 SCSMV的数据结构和算法实现
    5.4 实验结果
第六章 结束语
    6.1 结论
    6.2 将来的工作
附录
参考文献
致谢
作者简历


【参考文献】：
期刊论文
[1]专用集成电路的设计验证方法及一种实际的通用微处理器设计的多级验证体系[J]. 杨文华,罗晓沛.  计算机研究与发展. 1999(06)



本文编号：3428491