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

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

作　者: 郭建
导　师: 韩俊岗
学　校: 西安电子科技大学
专　业: 微电子学与固体电子学
关键词: 模型检验断言三值逻辑属性描述语言空属性
分类号: TP311.52
类　型: 博士论文
年　份: 2008年
下　载: 146次
引　用: 2次
阅　读: 论文下载

内容摘要

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

全文目录

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

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

内容摘要

全文目录

相似论文