硬件设计验证 基于模拟与形式的方法 simulation and formal method-based approachesPDF电子书下载

译者序 1

前言 1

致谢 1

第1章 设计验证的缘由 1

1.1　什么是设计验证 1

1.2　验证的基本原理 2

1.3　验证方法学 5

1.3.1 基于模拟的验证 5

1.3.2　基于形式方法的验证 7

1.4 基于模拟的验证与形式验证的比较 9

1.5　形式验证的局限性 10

1.6.1　并发进程 11

1.6　Verilog语言调度和执行语义简介 11

1.6.2　不确定性 12

1.6.3　调度语义 14

1.7　本章小结 14

第2章 编写验证的代码 15

2.1　功能正确性 16

2.1.1　语法检查 16

2.1.2　结构检查 22

2.2　时序正确性 24

2.2.1　竞争问题 24

2.2.2　时钟选通 25

2.2.3　时间零与零时间毛刺 26

2.2.4　域交叉毛刺 26

2.3.1　抽象的更高层次 27

2.3　模拟的性能 27

2.3.2　模拟器可识别组件 29

2.3.3　向量与标量 30

2.3.4 与其他模拟系统界面的最小化 32

2.3.5　低层次／组件层次优化 33

2.3.6　代码描述 33

2.4　可移植性与可维护性 33

2.4.1　项目代码布局 33

2.4.2　集中的资源 34

2.4.3　RTL设计文件格式 35

2.5 可综合性、可调试性与通用工具兼容性 36

2.5.1　可综合性 36

2.5.2　可调试性 37

2.6　基于周期的模拟 38

2.7　硬件模拟／仿真 40

2.8　2状态与4状态模拟 41

2.9　linter程序的设计与使用 42

2.10　本章小结 43

2.11　习题 43

第3章 模拟器体系结构与操作 46

3.1　编译器 46

3.2　模拟器 50

3.2.1　事件驱动的模拟器 50

3.2.2　基于周期的模拟器 55

3.2.3　混合模拟器 64

3.2.4　硬件模拟器与仿真器 68

3.3　模拟器的分类与比较 69

3.3.1　2状态与4状态模拟器 69

3.3.3　事件驱动的模拟器与基于周期的模拟器 70

3.3.2　零时延与单位时延模拟器 70

3.3.4　解释型与编译型模拟器 71

3.3.5　硬件模拟器 71

3.4　模拟器的操作与应用 72

3.4.1　基本模拟的文件结构 72

3.4.2　性能与调试 73

3.4.3　时序验证 75

3.4.4　设计描述 78

3.4.5　2状态与4状态 78

3.4.6　用封装的模型协同模拟 80

3.5　增量式编译 80

3.6　模拟器控制台 81

3.8　习题 82

3.7　本章小结 82

第4章 测试基准组成与设计 87

4.1　测试基准的分类与测试环境 87

4.2　初始化机制 90

4.2.1　寄存器传输级初始化 91

4.2.2　编程语言接口初始化 92

4.2.3　时刻零的初始化 94

4.3　时钟生成与同步 94

4.3.1　显式与倒换方法 94

4.3.2　绝对跃变时延 95

4.3.3　时刻零时钟跃变 96

4.3.4　时间单位与分辨率 96

4.3.5　时钟倍频器与分频器 96

4.3.6　时钟独立与抖动 97

4.3.7 时钟同步与△时延 98

4.4　激励生成 99

4.3.8　时钟生成组织 99

4.4.1　异步激励程序 102

4.4.2　指令代码或可编程激励 103

4.5　响应评估 103

4.5.1　设计状态的转储 104

4.5.2　黄金响应 107

4.5.3　时态规范的检查 114

4.6　验证实用程序 117

4.6.1　错误注入程序 118

4.6.2　错误与警告的告警机制 119

4.6.3　存储器装载与转储机制 119

4.6.4　稀疏存储器与内容可寻址存储器 122

4.7　测试基准至系统设计接口 125

4.6.5　断言例程 125

4.8　常见的实际技术与方法 126

4.8.1　验证环境配置 126

4.8.2　总线功能模型 128

4.9　本章小结 131

4.10　习题 132

第5章 测试构想、断言与覆盖 135

5.1　分层验证 136

5.1.1　系统层 137

5.1.2　单元层 138

5.1.3　模块层 138

5.2　测试规划 138

5.2.1　从体系结构规范中抽取功能 139

5.2.4　跟踪进程 142

5.2.3　建立测试用例 142

5.2.2　功能分级优先 142

5.3　伪随机测试生成程序 145

5.3.1　用户接口 145

5.3.2　寄存器与存储器分配 146

5.3.3　程序构造 147

5.3.4 自检机制 148

5.4　断言 148

5.4.1　定义所断言的内容 149

5.4.2　断言组成 149

5.4.3　编写断言 150

5.4.4　内建商用断言 158

5.5　SystemVerilog断言 159

5.5.1　立即断言 159

5.5.2　并发断言 160

5.6　验证覆盖 167

5.6.1　代码覆盖 168

5.6.2　参数覆盖 173

5.6.3　功能覆盖 175

5.6.4　条目覆盖与交叉覆盖 179

5.7　本章小结 180

5.8　习题 180

第6章 调试进程与验证周期 185

6.1　故障捕获、范围压缩与错误跟踪 185

6.1.1 故障捕获 186

6.1.2　范围压缩 186

6.1.3　错误跟踪系统 190

6.2　模拟数据转储 191

6.2.2　时态窗口 192

6.2.1　空间相邻点 192

6.3　潜在故障原因的隔离 193

6.3.1　参考值、传播与分支点 194

6.3.2　正向与反向调试 194

6.3.3　跟踪图 195

6.3.4　时间框架 196

6.3.5　负载、驱动源与锥形跟踪 198

6.3.6　存储器与阵列跟踪 199

6.3.7　零时间回路结构 200

6.3.8　系统设计的4个基本视图 201

6.3.9　典型调试器的功能 202

6.4　系统设计更新与维护：修改控制 204

6.5 回归、发布机制与流片标准 206

6.7　习题 208

6.6　本章小结 208

第7章 形式验证初步 215

7.1　集合与运算 215

7.2　关系、划分、偏序集与格 216

7.3　布尔函数与表示 222

7.3.1　对称布尔函数 224

7.3.2　不完全指定的布尔函数 226

7.3.3　特征函数 227

7.4　布尔函数运算符 229

7.5　有限状态自动机与语言 232

7.5.1　积自动机与状态机 234

7.5.2　状态等价与状态机最小化 236

7.5.3　有限状态机的等价 239

7.5.5　深度优先搜索 240

7.5.4　图算法 240

7.5.6　宽度优先搜索 243

7.6　本章小结 245

7.7　习题 246

第8章 判定图、等价检验与符号模拟 249

8.1　二叉判定图 250

8.1.1　二叉判定图上的运算 253

8.1.2　变量排序 259

8.2　判定图的变异 263

8.2.1　共用二叉判定图 263

8.2.2　边属性二叉判定图 264

8.2.3　零抑制二叉判定图 265

8.2.4　有序功能判定图 267

8.2.5　伪布尔函数与判定图 268

8.2.6　二叉瞬时图 270

8.3　基于判定图的等价检验 271

8.4　布尔可满足性 275

8.4.1　消解算法 276

8.4.2　基于搜索的算法 278

8.4.3　蕴涵图与学习 280

8.5　符号模拟 283

8.5.1　符号验证 285

8.5.2　输入约束 286

8.5.3　利用特征函数的符号模拟 288

8.5.4　参数化 289

8.6　本章小结 291

8.7　习题 292

9.1　性质、规范与逻辑 296

第9章 模型检验与符号计算 296

9.1.1　使用自动机的时序规范 297

9.1.2　时态结构与计算树 298

9.1.3 命题时态逻辑：LTL、CTL*与CTL 301

9.1.4　公平性约束 306

9.1.5 CTL*、CTL与LTL的相对表示性 306

9.1.6　SystemVerilog断言语言 307

9.2　性质检验 307

9.2.1　使用自动机的性质规范 307

9.2.2　语言包含 309

9.2.3　CTL公式的检验 310

9.2.4　有公平性约束的检验 312

9.3　符号计算与模型检验 313

9.3.1　符号有限状态机表示与状态遍历 314

9.3.2　反例的生成 318

9.3.3　等价检验 318

9.3.4　语言包含与公平性约束 321

9.4　符号CTL模型检验 325

9.4.1　不动点计算 325

9.4.2 有公平性约束的CTL检验 329

9.5　计算改进 331

9.5.1　早期量化 332

9.5.2　一般化余因数 334

9.6　模型检验工具的使用 335

9.7　本章小结 336

9.8　习题 336

参考文献 340

缩写词汇表 358