数字硬件的形式化验证pdf电子书版本下载

点此进入-本书在线PDF格式电子书下载【推荐-云解压-方便快捷】直接下载PDF格式图书。移动端-PC端通用
种子下载[BT下载速度快] 温馨提示：（请使用BT下载软件FDM进行下载）软件下载地址页 直链下载[便捷但速度慢]   [在线试读本书]   [在线获取解压码]

数字硬件的形式化验证PDF格式电子书版下载

下载的文件为RAR压缩包。需要使用解压软件进行解压得到PDF格式图书。

建议使用BT下载工具Free Download Manager进行下载,简称FDM(免费,没有广告,支持多平台）。本站资源全部打包为BT种子。所以需要使用专业的BT下载软件进行下载。如 BitComet qBittorrent uTorrent等BT下载工具。迅雷目前由于本站不是热门资源。不推荐使用！后期资源热门了。安装了迅雷也可以迅雷进行下载！

（文件页数 要大于 标注页数，上中下等多册电子书除外）

注意：本站所有压缩包均有解压码： 点击下载压缩包解压工具

第一章 形式化方法 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