第一章 形式化方法

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.4.3 小结

参考文献

第二章 数字硬件的规范描述和验证

2.1 设计过程和设计规范

2.1.1 系统设计方法

2.1.2 VHDL硬件描述语言

2.2 形式化描述和验证

2.2.1 形式化系统

2.2.2 硬件形式化验证的基本概念

2.3 交互定理证明系统概述

2.3.1 Boyer-Moore定理证明器

2.3.2 PVS原型验证系统

2.3.3 斯坦福时态逻辑证明器(STeP)

2.4 用XYZ／E时态逻辑语言描述和验证硬件的行为

2.4.1 用XYZ／E描述个基于微处理器的容错系统

2.4.2 用XYZ系统验证硬件的行为

参考文献

第三章 高阶逻辑系统及其在硬件验证中的应用

3.1 ML语言简介

3.1.1 类型和函数

3.1.2 关联、声明和递归

3.1.3 类型和多态类型

3.1.4 λ-表达式和高阶函数

3.1.5 ML的标准库

3.2 HOL系统的逻辑及证明

3.2.1 HoL系统的项

3.2.2 HOL系统的理论

3.2.3 用HOL系统证明定理

3.3 目标制导的证明方法

3.3.1 基本证明对策

3.3.2 用归纳法证明定理

3.3.3 对策的组合与假设条件表的管理

3.3.4 基本逻辑门的理论

3.4 H0L系统的定理库的重用

3.4.1 taut库

3.4.2 reduce库

3.4.3 arilh库

3.5 一个高速并行加法器的设计和验证

3.5.1 条件和加法器(CSA)的算法

3.5.2 CSA加法器的设计

3.5.3 用高阶逻辑系统证明CSA加法器设计的正确性

3.6 一个微处理器的验证

3.6.1 微处理器实现的描述

3.6.2 微处理器的行为的描述

3.6.3 微处理器的形式验证

参考文献

第四章 模型检验

4.1 分支时态逻辑

4.1.1 Kripke结构

4.1.2 分支时态逻辑CTL

4.1.3 固定点

4.1.4 有限状态自动机

4.2.1 固定点的计算

4.2 CTL模型检验

4.2.2 公正性

4.3 二叉判定图

4.3.1 布尔函数与二叉判定图

4.3.2 变量顺序的影响

4.3.3 深度优先BDD构造算法

4.3.4 变量再排序

4.3.5 变量筛选

4.4 符号模型检验

参考文献

第五章 验证与综合系统VIS

5.1 VIS系统简介

5.2 VIS系统的设计输入和Verilog语言

5.2.1 VIS系统支持的Verilog的特点

5.2.2 用Verilog描述设计的几个问题

5.2.3 交通灯控制器

5.3 用VIS系统进行形式化验证

5.3.1 BLIF-MV转换为内部有限状态机表示

5.3.2 模型检验操作

5.4 用VIS系统验证微处理器PIC的设计

5.4.1 PIC微处理器简介

5.4.2 用VHDL语言设计PIC

5.4.3 用VIS系统验证PIC

参考文献

第六章 基于自动机理论的形式化验证

6.1 Buchi自动机

6.2 轨迹语义与同步积

6.3 Buchi自动机和验证

6.3.1 自动机包含

6.3.2 互模拟

6.3.3 测试语言包含

6.3.4 测试自动机所接受的语言是否为空

6.4 时间自动机

6.4.1 时间自动机及其语义

6.4.2 积自动机

6.5 时间自动机的状态最小化算法

6.5.1 计算转移的最早发生时间和最晚发生时间

6.5.2 时间自动机最小化算法

6.5.3 实时系统的验证

参考文献