Hardware design verification:simulation and formal method-based approache

第1章 设计验证的缘由
1.1 什么是设计验证
1.2 验证的基本原理
1.3 验证方法学
1.4 基于模拟的验证与形式验证的比较
1.5 形式验证的局限性
1.6 Verilog语言调度和执行语义简介
1.7 本章小结
第2章 编写验证的代码
2.1 功能正确性
2.2 时序正确性
2.3 模拟的性能
2.4 可移植性与可维护性
2.5 可综合性、可调试性与通用工具兼容性
2.6 基于周期的模拟
2.7 硬件模拟／仿真
2.8.2 状态与4状态模拟
2.9 linter程序的设计与使用
2.10 本章小结
2.11 习题
第3章 模拟器体系结构与操作
3.1 编译器
3.2 模拟器
3.3 模拟器的分类与比较
3.4 模拟器的操作与应用
3.5 增量式编译
3.6 模拟器控制台
3.7 本章小结
3.8 习题
第4章 测试基准组成与设计
4.1 测试基准的分类与测试环境
4.2 初始化机制
4.3 时钟生成与同步
4.4 激励生成
4.5 响应评估
4.6 验证实用程序
4.7 测试基准至系统设计接口
4.8 常见的实际技术与方法
4.9 本章小结
4.10 习题
第5章 测试构想、断言与覆盖
5.1 分层验证
5.2 测试规划
5.3 伪随机测试生成程序
5.4 断言
5.5 SystemVerilog断言
5.6 验证覆盖
5.7 本章小结
5.8 习题
第6章 调试进程与验证周期
6.1 故障捕获、范围压缩与错误跟踪
6.2 模拟数据转储
6.3 潜在故障原因的隔离
6.4 系统设计更新与维护：修改控制
6.5 回归、发布机制与流片标准
6.6 本章小结
6.7 习题
第7章 形式验证初步
7.1 集合与运算
7.2 关系、划分、偏序集与格
7.3 布尔函数与表示
7.4 布尔函数运算符
7.5 有限状态自动机与语言
7.6 本章小结
7.7 习题
第8章 判定图、等价检验与符号模拟
8.1 二叉判定图
8.2 判定图的变异
8.3 基于判定图的等价检验
8.4 布尔可满足性
8.5 符号模拟
8.6 本章小结
8.7 习题
第9章 模型检验与符号计算
9.1 性质、规范与逻辑
9.2 性质检验
9.3 符号计算与模型检验
9.4 符号CTL模型检验
9.5 计算改进
9.6 模型检验工具的使用
9.7 本章小结
9.8 习题
参考文献
缩写词汇表