图书介绍
数字硬件的形式化验证PDF|Epub|txt|kindle电子书版本网盘下载
- 韩俊刚，杜慧敏著（西安邮电学院） 著
- 出版社： 北京：北京大学出版社
- ISBN：7301053320
- 出版时间：2001
- 标注页数：269页
- 文件大小：8MB
- 文件页数：283页
- 主题词：集成电路(学科: 自动检测系统) 集成电路 自动检测系统
PDF下载
下载说明
数字硬件的形式化验证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 分支时态逻辑CTL143
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
第五章 验证与综合系统VIS189
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语言设计PIC225
5.4.3 用VIS系统验证PIC227
参考文献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