第一章 形式化方法 1
1.1 什么是形式化方法 1
1.2 形式化方法的意义和局限性 4
1.2.1 形式化方法的意义 4
1.2.2 形式化方法的局限性 8
1.3 对形式化方法发展的评述 10
1.3.1 系统规范 10
1.3.2 形式化验证 12
1.4 形式化方法向工业界的转移和发展趋势 18
1.4.1 形式化方法向工业界的技术转移 18
1.4.2 形式化方法的发展趋势 19
1.4.3 小结 21
参考文献 23
第二章 数字硬件的规范描述和验证 26
2.1 设计过程和设计规范 27
2.1.1 系统设计方法 28
2.1.2 VHDL硬件描述语言 31
2.2 形式化描述和验证 35
2.2.1 形式化系统 37
2.2.2 硬件形式化验证的基本概念 40
2.3 交互定理证明系统概述 43
2.3.1 Boyer-Moore定理证明器 44
2.3.2 PVS原型验证系统 47
2.3.3 斯坦福时态逻辑证明器(STeP) 52
2.4 用XYZ／E时态逻辑语言描述和验证硬件的行为 53
2.4.1 用XYZ／E描述个基于微处理器的容错系统 55
2.4.2 用XYZ系统验证硬件的行为 58
参考文献 62
第三章 高阶逻辑系统及其在硬件验证中的应用 64
3.1 ML语言简介 65
3.1.1 类型和函数 66
3.1.2 关联、声明和递归 68
3.1.3 类型和多态类型 70
3.1.4 λ-表达式和高阶函数 73
3.1.5 ML的标准库 75
3.2 HOL系统的逻辑及证明 76
3.2.1 HoL系统的项 76
3.2.2 HOL系统的理论 78
3.2.3 用HOL系统证明定理 80
3.3 目标制导的证明方法 83
3.3.1 基本证明对策 84
3.3.2 用归纳法证明定理 86
3.3.3 对策的组合与假设条件表的管理 88
3.3.4 基本逻辑门的理论 95
3.4 H0L系统的定理库的重用 96
3.4.1 taut库 96
3.4.2 reduce库 98
3.4.3 arilh库 101
3.5 一个高速并行加法器的设计和验证 105
3.5.1 条件和加法器(CSA)的算法 105
3.5.2 CSA加法器的设计 109
3.5.3 用高阶逻辑系统证明CSA加法器设计的正确性 111
3.6 一个微处理器的验证 115
3.6.1 微处理器实现的描述 117
3.6.2 微处理器的行为的描述 126
3.6.3 微处理器的形式验证 128
参考文献 138
第四章 模型检验 140
4.1 分支时态逻辑 141
4.1.1 Kripke结构 141
4.1.2 分支时态逻辑CTL 143
4.1.3 固定点 146
4.1.4 有限状态自动机 147
4.2.1 固定点的计算 151
4.2 CTL模型检验 151
4.2.2 公正性 156
4.3 二叉判定图 158
4.3.1 布尔函数与二叉判定图 159
4.3.2 变量顺序的影响 163
4.3.3 深度优先BDD构造算法 164
4.3.4 变量再排序 170
4.3.5 变量筛选 176
4.4 符号模型检验 178
参考文献 187
第五章 验证与综合系统VIS 189
5.1 VIS系统简介 189
5.2 VIS系统的设计输入和Verilog语言 190
5.2.1 VIS系统支持的Verilog的特点 192
5.2.2 用Verilog描述设计的几个问题 194
5.2.3 交通灯控制器 196
5.3 用VIS系统进行形式化验证 203
5.3.1 BLIF-MV转换为内部有限状态机表示 203
5.3.2 模型检验操作 213
5.4 用VIS系统验证微处理器PIC的设计 224
5.4.1 PIC微处理器简介 224
5.4.2 用VHDL语言设计PIC 225
5.4.3 用VIS系统验证PIC 227
参考文献 230
第六章 基于自动机理论的形式化验证 231
6.1 Buchi自动机 231
6.2 轨迹语义与同步积 236
6.3 Buchi自动机和验证 238
6.3.1 自动机包含 238
6.3.2 互模拟 239
6.3.3 测试语言包含 247
6.3.4 测试自动机所接受的语言是否为空 250
6.4 时间自动机 251
6.4.1 时间自动机及其语义 251
6.4.2 积自动机 255
6.5 时间自动机的状态最小化算法 258
6.5.1 计算转移的最早发生时间和最晚发生时间 258
6.5.2 时间自动机最小化算法 264
6.5.3 实时系统的验证 266
参考文献 268