在数字系统设计中断言验证的研究

论文摘要

随着微电子技术的高速发展,人们对电子产品的强大需求使得现代集成电路系统的规模和复杂度日益提高。在系统芯片(SOC)设计中,可以利用IP构成复杂的大规模系统。但是,SOC的验证已成为设计流程中工作量最大的工作。我们认为系统的验证应当是模拟仿真、形式化和半形式化等方法的混合验证过程。基于断言的验证(ABV)是把形式化方法集成到传统模拟流程中的一种有效的方法。在RTL设计中插入设计意图(断言),通过模拟或形式化技术来检查该设计是否满足这些断言。本文在总结国内外基于断言验证研究成果的基础上,提出了系统抽象后原子命题为三值的模型检验技术,研究了基于PSL的动态和静态验证方法。主要内容包括:解决了基于三值逻辑的模型检验问题。在模型检验中,状态爆炸是影响其应用的关键。本文的解决方案是对系统进行抽象,以减少其状态空间。系统模型采用不完全的Kripke结构表示,在此结构下,定义了三值CTL逻辑公式的形式化语义,并用此逻辑公式表示系统的性质。提出了基于不完全的kripke结构的三值逻辑模型检验算法,并给出了一个证明系统,在属性验证是未知情况时,从该证明系统中可推导出正例或反例,为系统能够进一步验证提供参考信息。同时,为了使该模型检验具有更广泛的应用,还提出了将模态转移系统转换成不完全的Kripke结构的方法,通过该转换再利用上述算法能够实现基于模态转移系统的三值逻辑模型检验。提出了在模型检验中空属性问题的探测方法。一个公式描述了系统所具有的属性,若公式中的一个子公式的真值对该公式的真值不会产生影响,那么这个公式就是一个空属性公式。对空属性的探测可以根据原子命题的极性(polarity),用FALSE或TRUE来替换,形成一系列子公式,然后根据对子公式模型检验的结果,就可得出结论。研究了PSL在验证中的应用。PSL具有清晰语义和简明语法,给出了描述设计属性的一个标准方法。基于PSL的断言可进行动态仿真和静态验证。本文提出了PSL的子集转换成自动机的方法,通过两个具体的实例给出了PSL断言在实际设计中的应用。

论文目录

• 摘要
• Abstract
• 第一章 绪论
• 1.1 研究的背景及意义
• 1.2 研究的现状
• 1.2.1 基于断言的验证
• 1.2.2 基于形式化方法的验证
• 1.2.3 等价性检查
• 1.2.4 模型检验
• 1.2.5 定理证明
• 1.3 作者的主要工作和创新点
• 1.3.1 作者的主要工作
• 1.3.2 创新点
• 1.4 本文的组织结构
• 第二章 三值逻辑模型检验
• 2.1 二值逻辑的模型检验
• 2.1.1 Kripke 结构
• 2.1.2 CTL 公式
• 2.1.3 模型检验
• 2.2 不完全 Kripke 结构（Partial Kripke Structure PKS）
• 2.2.1 不完全 Kripke 结构
• 2.2.2 操作符的解释
• 2.3 三值逻辑CTL 公式
• 2.4 三值时态逻辑公式的模型检验
• 2.4.1 三值逻辑公式的模型检验算法
• 2.4.2 例子
• 2.4.3 公平性约束的三值逻辑公式模型检验
• 2.4.4 模型检验的复杂度分析
• 2.5 三值时态逻辑公式的符号模型检验
• 2.5.1 三叉判定图（TDD）
• 2.5.2 在化简的OTDD 上实现的操作
• 2.5.3 基于OTDD 的符号模型检验
• 2.6 三值逻辑模型检验的正例和反例
• 2.6.1 存在路径量词的证明规则
• 2.6.2 自动证明的产生
• 2.6.3 通过证明过程产生正例的方法
• 2.6.4 全称路径量词的反例
• 2.7 应用
• 2.7.1 在硬件验证中的应用
• 2.7.2 在SOC 验证中的应用
• 2.8 小结
• 第三章 模态转移系统到不完全 KRIPKE 结构的转换
• 3.1 引言
• 3.2 模态转移系统（Modal Transition System MTS）
• 3.2.1 模态转移系统
• 3.2.2 Hennessy-Milner 逻辑公式（HML）
• 3.3 不完全 Kripke 结构下的命题模态逻辑
• 3.4 MTS 转换成PKS
• 3.4.1 MTS 转换成PKS
• 3.4.2 逻辑公式的转换
• 3.4.3 转换的正确性
• 3.4.4 基于MTS 的模型检查算法
• 3.5 MTS 转换成不完全 Kripke 结构复杂度分析
• 3.6 相关的工作
• 3.7 小结
• 第四章 模型检验中对 CTL 公式的空属性探测
• 4.1 空属性（vacuity）
• 4.2 公式的空属性探测
• 4.2.1 子公式集合的空属性探测
• 4.2.2 有极性的CTL 公式的空探测
• 4.2.3 空探测的方法
• 4.3 一个例子
• 4.3.1 总体设计
• 4.3.2 描述
• 4.3.3 模型检验及属性的空探测
• 4.4 小结
• 第五章 基于 PSL 的模型检验的关键技术
• 5.1 基于PSL 的模型检验技术
• 5.2 属性描述语言PSL
• 5.2.1 基础语言部分（FL）
• 5.2.2 布尔表达式
• 5.2.3 序列（SERES）公式
• 5.2.4 FL 公式
• 5.3 自动机的构造
• 5.3.1 PSL 的形式化语法
• 5.3.2 自动机的构造
• 5.4 小结
• 第六章 用 PSL 验证宽带交换芯片
• 6.1 SDH 技术
• 6.1.1 SDH 概念
• 6.1.2 SDH 速率
• 6.1.3 SDH 帧结构
• 6.1.4 SDH 帧中字节位置确定
• 6.2 宽带电路交换芯片
• 6.2.1 总体描述
• 6.2.2 结构框图
• 6.3 断言的必要性
• 6.4 芯片验证思路
• 6.5 验证步骤
• 6.6 断言引入
• 6.7 结果分析
• 6.7.1 验证结果
• 6.7.2 原因分析
• 6.7.3 断言心得
• 6.8 小结
• 第七章 PSL 在静态验证中的应用
• 7.1 PSL 在 VIS 中的应用
• 7.1.1 基于PSL 的VIS 验证原型系统
• 7.1.2 VIS 使用的概要
• 7.2 基于PSL 的仲裁器的验证
• 7.2.1 仲裁器的设计
• 7.2.2 仲裁器的属性
• 7.2.3 对PSL 属性的验证
• 7.3 小结
• 第八章 结论以及将来的工作
• 8.1 总结
• 8.1.1 基于三值逻辑的模型检验
• 8.1.2 CTL 公式空属性的探测
• 8.1.3 属性描述语言PSL 在基于断言的验证中的应用
• 8.2 存在的问题和将来的工作
• 附录仲裁器设计及验证中的反例
• 致谢
• 参考文献
• 研究成果