数字电路的仿真与验证PDF电子书下载

第1章　绪论 1

1.1 数字集成电路的设计流程 1

1.2 数字集成电路的设计方式 2

1.2.1 自上而下的设计和自下而上的设计 3

1.2.2 基于单元与基于平台的设计 3

1.2.3 芯片的正向设计 4

1.3 系统芯片的设计 6

1.4 电路设计的仿真与验证 9

1.4.1 仿真的层次 10

1.4.2 形式验证 11

第2章　电路模型 13

2.1 电路模型的相关概念 13

2.1.1 数字系统的抽象级 13

2.1.2 功能与结构模型 14

2.2 在逻辑级的功能模型 15

2.2.1 真值表和立方体 15

2.2.2 逻辑函数的二元判定图表示 16

2.2.3 功能模型的程序描述 17

2.3.1 寄存器传输语言的结构 18

2.3 在寄存器级的功能模型 18

2.3.2 RTL中的时序模型 20

2.3.3 内部RTL模型 21

2.4 结构模型 21

2.4.1 结构模型的外部表示 21

2.4.2 结构模型的性质 22

2.4.3 结构模型的内部表示 24

2.5 模型的层次 25

第3章　电路的逻辑仿真 28

3.1 仿真的原理 29

3.2 编译仿真与事件驱动仿真 30

3.2.1 编译仿真 31

3.2.2 事件驱动仿真 33

3.3 元件延迟与冒险检测 34

3.3.1 元件输出值的计算 35

3.3.2 延迟模型 36

3.3.3 冒险检测 39

3.4 门级事件驱动仿真 43

4.1.1 功能仿真的类型 47

第4章　高层次仿真及工具软件 47

4.1 功能仿真 47

4.1.2 功能仿真的途径 48

4.2 高层次仿真 49

4.2.1 VHDL语言的基本结构 49

4.2.2 VHDL仿真系统的结构 52

4.2.3 VHDL内部模型的建立 54

4.2.4 VHDL仿真算法 60

4.3 仿真工具软件ModelSim 64

4.3.1 ModelSim仿真软件的特点 64

4.3.2 使用ModelSim进行设计仿真 65

第5章　电路的开关级仿真 71

5.1 开关级网络 72

5.2 稳态响应 74

5.2.1 布尔节点和晶体管状态 74

5.2.2 三元状态 77

5.3 稳态响应的分析 79

5.4.1 有关根路径的一种代数 80

5.4 稳态响应的代数表示 80

5.4.2 从路径到方程 81

5.4.3 不动点方程的形式 83

5.4.4 不动点方程的例子 84

5.5 仿真方程的求解 85

5.5.1 求解稀疏方程的不动点 85

5.5.2 基于增量的解方法 87

5.6 仿真程序 89

5.7 基于组的仿真 93

5.7.1 估计一个组的稳定状态 94

5.7.2 节点的信息量 96

5.7.3 节点信息量的迭代估计 97

5.7.4 仿真时的电路结构分析 100

第6章　模型检验 103

6.1 验证的建模 103

6.2 计算树逻辑的语法 104

6.3 计算树逻辑的语义 106

6.4 CTL公式间的等价性 110

6.5 CTL验证的例子——进程互斥 111

6.6.1 标签算法 114

6.6 模型检验算法 114

6.6.2 模型检验算法的程序实现 116

6.7 符号模型验证系统 118

6.7.1 验证系统的结构 119

6.7.2 验证系统中的模块 120

6.7.3 验证系统在互斥访问中的应用 121

6.8 具有公正性的模型检验 123

6.9 CTL的不动点特性 125

6.9.1 单调函数 127

6.9.2 SATEG的正确性 128

6.9.3 SATEU的正确性 129

6.10 符号模型检验 131

6.10.1 状态集的表示 131

6.10.2 迁移关系的表示 133

第7章　二元判定图的结构 136

7.1 二元判定图的概念 136

7.2 二元判定图的约简 139

7.3.1 BDD的遍历 144

7.3 二元判定图的程序实现 144

7.3.2 BDD约简的程序实现 145

7.3.3 由布尔表达式经运算生成BDD 146

7.3.4 生成BDD的ITE算法 149

7.4 二元判定图的变量编序 151

7.4.1 变量编序对二元判定图的影响 151

7.4.2 静态变量编序 152

7.4.3 动态变量编序 155

8.1.1 局部变量交换的效果 160

8.1 变量编序中变量交换的效果分析 160

第8章　二元判定图的性质与应用 160

8.1.2 使用低界值的过滤法 164

8.2 最优编序 165

8.3 ZBDD的定义与操作 170

8.3.1 ZBDD的定义与性质 170

8.3.2 ZBDD的操作 171

8.3.3 ZBDD在布尔立方集代数中的应用 173

8.3.4 用ZBDD进行多项式的表示与操作 177

8.4 多级逻辑综合与ZBDD 183

8.4.1 二元立方集的ZBDD表示 183

8.4.2 立方集表示的分解 184

8.5 使用BDD进行电路测试 187

8.6 小结 189

第9章　组合电路验证 190

9.1 组合与时序电路的相关表示 190

9.2 组合电路的验证方法 194

9.3 引入断点 195

9.4 组合电路验证方法的实现 197

9.4.1 验证的步骤 197

9.4.2 计算潜在的断点 198

9.4.3 检测断点 199

9.4.4 选取断点 201

9.5 组合电路验证的部分实验结果 202

9.6 小结 205

第10章　时序电路验证 206

10.1 时序电路的验证方法 206

10.2 时序电路的等价性 208

10.3 可重置电路 213

10.4 利用功能依赖 213

10.5 时序电路验证方法的实现 215

10.6 检测功能依赖性 217

10.7 时序电路验证的部分实验结果 221

10.8 小结 223

第11章　系统芯片SOC的验证 224

11.1 系统芯片的结构 224

11.2 系统芯片的设计过程 225

11.2.1 SOC的设计流程 225

11.2.2 软核的设计流程 227

11.2.3 硬核的设计流程 228

11.2.4 系统集成 229

11.3.1 验证策略与验证目标 230

11.3 芯核的验证 230

11.3.2 测试平台的建立 233

11.3.3 芯核时序验证 234

11.3.4 芯核接口的验证 235

11.4 SOC的系统级设计及验证 236

11.4.1 SOC的系统级设计 236

11.4.2 SOC的系统级验证 237

附录　名词缩写表 244

参考文献 246