数字集成电路设计验证 量化评估、激励生成、形式化验证PDF电子书下载

第1章　绪论 1

1.1　设计验证简介 1

1.2　设计验证中的关键问题 4

1.2.1　量化评估 4

1.2.2　激励生成 5

1.2.3　形式化验证 7

1.3　章节组织结构 8

参考文献 10

第2章　寄存器传输级行为描述抽象方法 12

2.1　硬件描述语言概述 12

2.1.1　硬件描述语言的产生与发展 12

2.1.2　硬件描述语言的描述特点 13

2.2　RTL行为描述的进程分析 19

2.2.1　语法与语义限制 19

2.2.2　组合进程 21

2.2.3　时钟进程 23

2.2.4　异步进程 25

2.3　寄存器传输级行为描述抽象 26

2.3.1　行为描述中的进程 26

2.3.2　过程性语句 26

2.3.3　语句的语义行为 31

2.3.4　语句的执行条件 35

2.3.5　进程的相互关系 36

2.3.6　电路模型 38

2.3.7　行为模拟方式 40

2.4　本章总结 41

参考文献 42

第3章　基于可观测性的覆盖率评估方法 43

3.1　设计验证中的可观测性 43

3.1.1　研究设计验证中的可观测性的意义 44

3.1.2　设计验证中的可观测性相关研究 46

3.2　可观测性的DFUDO模型 48

3.2.1　工作基础 48

3.2.2　动态参数化引用-定值链 49

3.2.3　HDL设计中信号可观测性的DFUDO模型 53

3.3　基于DFUDO模型的语句覆盖率评估方法 55

3.3.1 基于DFUDO模型的语句覆盖率（OSC）的定义 55

3.3.2　覆盖率评估算法 56

3.3.3　实验及分析 57

3.4　基于DFUDO模型的分支覆盖率评估方法 63

3.4.1　基于DFUDO模型的分支覆盖率（OBC）的定义 63

3.4.2　优化的覆盖率评估算法 65

3.4.3　实验及分析 66

3.5　两种基于DFUDO模型的代码覆盖率评估方法的比较 71

3.5.1　OSC与OBC的共性 71

3.5.2　OSC与OBC的差异比较 72

3.6　可观测性的COC模型 74

3.6.1　增强型进程控制树与数据流向图 74

3.6.2　控制-观测链 76

3.6.3　基于COC模型的可观测性的定义 78

3.7　基于COC模型的语句覆盖率评估方法 78

3.7.1　实现框架 78

3.7.2　电路的行为模拟 79

3.7.3　可观测性分析过程 80

3.7.4　基于COC模型的语句覆盖率的计算 81

3.7.5　实验及分析 82

3.8　本章总结 84

参考文献 86

第4章　缺项-设计错误模型 88

4.1　设计错误模型介绍 88

4.2　实际芯片的设计验证 90

4.2.1　设计简介 90

4.2.2　接口逻辑的设计验证 91

4.2.3　处理器逻辑的设计验证 93

4.3　缺项-设计错误模型 94

4.3.1　设计错误数据的分析 94

4.3.2　缺项错误模型 96

4.3.3　缺项错误模型的测试方法 99

4.3.4　实验及分析 100

4.4　设计错误的注入 104

4.4.1　软件的变异测试系统Mothra 104

4.4.2　基于Mothra的硬件设计变异测试系统 107

4.4.3　独立的硬件设计错误注入系统ErrorInjector 108

4.5 本章总结 114

参考文献 115

第5章　基于错误传播概率的量化分析方法 118

5.1　在量化评估方法中考虑错误效果的意义 118

5.2　RTL操作的错误屏蔽概率分析 119

5.2.1　一元操作的EMP分析 119

5.2.2　二元操作的EMP分析 123

5.2.3　常见字操作的错误屏蔽概率 130

5.3　基于错误屏蔽概率的静态可观测性量化分析方法 131

5.3.1　研究静态可观测性分析方法的动机 131

5.3.2　HDL设计中内部信号的静态可观测性分析方法 132

5.3.3　根据低观测根源选择内部观测点的方法 135

5.3.4　实验及分析 137

5.4　本章总结 139

参考文献 139

第6章　模拟验证的激励生成概述 141

6.1　简介 141

6.2　遗传算法用于激励生成 142

6.2.1　遗传算法的起源和发展 142

6.2.2　遗传算法的基本结构 142

6.2.3　遗传算法的技术要点 143

6.2.4　基于模拟的激励生成与遗传算法 146

6.2.5　ARTIST系统 147

6.3　确定性激励生成 148

6.3.1　基于故障模型的测试生成 148

6.3.2　基于错误模型的激励生成 150

6.4　本章总结 151

参考文献 152

第7章　基于传输故障模型的寄存器传输级激励生成 154

7.1　行为倾向驱动引擎 154

7.1.1　电路行为的表征与展现 154

7.1.2　函数或映射的属性 155

7.1.3　抽象的行为值与RTL变量的行为 160

7.1.4　行为倾向 164

7.1.5　驱动引擎 168

7.2　传输故障模型 174

7.2.1　电路故障的层次化抽象模型 175

7.2.2　传输故障的定义与组织 176

7.2.3　传输故障与逻辑故障的对应关系 177

7.3　无回溯激励生成及算法实现 178

7.3.1　无回溯激励生成 178

7.3.2　基于行为倾向驱动引擎构造无回溯测试生成算法 184

7.3.3　简单实例分析 188

7.3.4　算法特征小结 191

7.4　实验及分析 192

7.4.1　拟定的实验方案 192

7.4.2　系统实现方式 193

7.4.3　实验结果比较分析 194

7.5　本章总结 198

参考文献 198

第8章　基于行为阶段聚类的寄存器传输级激励生成 200

8.1　寄存器传输级行为描述与有限状态机 200

8.1.1　有关RTL行为描述的若干定义 200

8.1.2　有限状态机 202

8.1.3　小结 205

8.2　电路的行为阶段 206

8.2.1　阶段变量 206

8.2.2　行为阶段转换函数 209

8.2.3　小结 211

8.3　行为阶段的聚类 212

8.3.1　对电路状态聚类的动机 212

8.3.2　基于RTL行为描述的状态聚类：行为阶段聚类 214

8.3.3　小结 224

8.4　基于聚类的激励生成 224

8.4.1　故障模型 224

8.4.2　基于聚类的测试生成算法 226

8.4.3 基于聚类的ATG系统ATCLUB 228

8.5　实验及分析 236

8.6　本章总结 239

参考文献 240

第9章　覆盖率驱动的寄存器传输级激励生成 242

9.1　基于混合遗传算法的激励生成 242

9.1.1　遗传算法的改进方法 242

9.1.2　RTL模型和系统实现框架 243

9.1.3　遗传算法设计 245

9.1.4　实验及分析 251

9.2　可观测性语句覆盖率驱动的激励生成 253

9.2.1　无回溯的激励生成方案 253

9.2.2 以基于可观测性的语句覆盖率为驱动的激励生成过程 254

9.2.3　停止判断机制 256

9.2.4　选择阈值 257

9.2.5　实验及分析 257

9.3　本章总结 259

参考文献 260

第10章　布尔函数与基于电路的布尔推理 261

10.1　布尔函数 261

10.1.1　布尔函数的运算 261

10.1.2　硬件行为的模拟 262

10.2　二叉判决图 263

10.2.1　有序二叉判决图 263

10.2.2　有序二叉判决图的运算 265

10.2.3　有序二叉判决图的变量排序 266

10.2.4　BDD在形式化验证中的应用 267

10.3　布尔可满足性 270

10.3.1　布尔可满足性问题 270

10.3.2　布尔可满足性问题的算法 272

10.3.3　SAT在基于电路的布尔推理中的应用 273

10.4　静态逻辑蕴涵 278

10.4.1　静态逻辑蕴涵的基本概念 278

10.4.2　静态逻辑蕴涵的算法 279

10.4.3　静态逻辑蕴涵的应用 281

10.5　本章总结 283

参考文献 284

第11章　基于可满足性的增量等价性检验方法 287

11.1　等价性检验介绍 287

11.1.1　研究背景及意义 287

11.1.2　等价性检验综述 290

11.2　基于可满足性的增量等价性检验方法 299

11.2.1　SAT在等价性检验中的应用 300

11.2.2　基于可满足性的增量等价性检验方法 301

11.2.3　实验及分析 305

11.3　本章总结 308

参考文献 308

第12章　验证包含黑盒的电路设计的形式化方法 311

12.1　集成电路设计中的黑盒问题 311

12.2　验证包含黑盒的电路设计的常用方法 312

12.2.1　基于BDD的方法 312

12.2.2　基于SAT的方法 314

12.3　结合逻辑模拟与布尔可满足性的验证方法 315

12.3.1　基于量化的布尔可满足性验证方法 315

12.3.2　逻辑模拟与布尔可满足性算法的结合 317

12.3.3　算法的改进 319

12.3.4　实验及分析 320

12.4　包含黑盒的电路设计验证方法在逻辑错误诊断中的应用 323

12.4.1　错误诊断方法的相关研究 324

12.4.2　结合逻辑模拟与布尔可满足性的错误诊断方法 331

12.4.3　实验及分析 334

12.5　本章总结 336

参考文献 336

第13章　极小布尔不可满足问题 339

13.1 引言 339

13.2　识别MU式的算法 340

13.3　提取MU子式的近似算法 344

13.3.1　自适应核搜索算法 344

13.3.2　利用蕴涵图的近似提取算法 347

13.3.3　利用蕴涵图提取MU子式的算法误差模拟实验 350

13.3.4　AMUSE方法 351

13.4　提取MU子式的精确算法 355

13.4.1　利用线性规划的提取算法 355

13.4.2　遍历子句的算法及预先局部赋值优化策略 358

13.4.3　实验及分析 360

13.5　本章总结 362

参考文献 362

第14章　模型检验在电路设计验证中的应用研究 364

14.1　模型检验简介 364

14.1.1　有限状态转移模型 364

14.1.2　时态逻辑 366

14.1.3　模型检验 370

14.1.4　满足时态逻辑公式状态集合的不动点表征 372

14.2　符号模型检验中转移关系的分组策略 373

14.2.1　布尔函数的支撑变量 373

14.2.2　二叉判决图的结点与支撑向量 374

14.2.3　基于支撑向量海明距离的转移关系分组策略 375

14.2.4　实验及分析 376

14.3　结合ATG和SAT的无界模型检验前像计算方法 377

14.3.1　系统前像计算方法及动机 378

14.3.2　ATG过程减少状态变量上的赋值 379

14.3.3　实验及分析 380

14.4　基于SAT的电路属性检验 382

14.4.1 RTL设计到CNF的转化 383

14.4.2　针对电路的SAT求解器优化 384

14.4.3　多时帧搜索策略 389

14.4.4　实验及分析 390

14.5　本章总结 392

参考文献 392

第15章　总结与展望 395

15.1　总结 395

15.2　展望 397

参考文献 401

索引 402