信阅平台

编辑推荐

本书是全面论述数字集成电路设计验证方法的学术著作，汇集了自2000年以来中国科学院计算研究所（以下简称中科院计算所）在数字集成电路设计验证方法学研究中取得的自主创新的重要研究成果和结论。内容涉及数字集成电路设计验证的三个重要方面：量化评估、激励生成和形式化验证。 全书共15章，其中技术内容可分为三大部分。第一部分（第2～5章）量化评估，从可观测性信息和发现设计错误的能力两个角度，论述数字集成电路设计验证的量化评估方法。第二部分（第6～9章）激励生成，针对寄存器传输级的激励生成问题，从故障模型和覆盖率导向两个角度，论述确定性和非确定性的激励生成方法。第三部分（第10～14章）形式化验证，从提高处理速度的角度，论述形式化验证中的等价性检验方法和模型检验方法。

展开

内容介绍

《数字集成电路设计验证：量化评估、激励生成、形式化验证》内容涉及数字集成电路设计验证的三个主要方面：量化评估、激励生成和形式化验证。主要包括寄存器传输级（RTL）电路建模、基于可观测性的覆盖率评估方法、设计错误模型；基于故障模型的激励生成、基于RTL行为模型的激励生成、覆盖率驱动的激励生成；基于可满足性的等价性检验、包含黑盒电路的形式化验证，以及不可满足问题。 全书图文并茂，阐述了作者及其科研团队自主创新的研究成果和结论，对致力于数字集成电路设计验证方法研究的科研人员（尤其是在读研究生），具有较大的学术参考价值，也可用作集成电路专业的高等院校教师、研究生和高年级本科生的教学参考书。

展开

精彩书摘

第6章介绍了寄存器传输级的激励自动生成方法的研究现状，主要包括：将遗传算法用于激励生成的非确定性方法，以及基于故障模型／错误模型的确定性激励生成方法。 第7章研究了基于故障模型的寄存器传输级激励生成方法。设计了行为倾向驱动引擎用于展现电路的行为，建立了一种新的故障模型——传输故障模型，基于行为倾向驱动引擎构造了传输故障的无回溯测试生成算法，实现了X_Pulling和TiDE两个测试生成系统，并进行了相关实验和数据分析。 第8章研究了从寄存器传输级行为描述出发，如何生成测试序列来检测有限状态机的状态转移关系。提出了有限状态机的行为阶段聚类描述，该描述可通过从寄存器传输级行为描述抽取状态信息得到。建立了一种新的行为级故障模型——行为阶段转换故障模型，进一步提出了一种基于聚类的测试生成算法。实现了基于行为阶段聚类的寄存器传输级自动测试生成系统ATCLUB，并进行了相关实验和数据分析。 第9章研究了以有效的覆盖率为导向的非确定性的激励生成方法。介绍了两种方法：第一种，采用设计验证常用的覆盖率评估准则，附加第7章提出的传输故障模型的覆盖准则，设计了混合遗传算法来进行激励生成；第二种，针对第3章所提出的可观测性覆盖准则COC模型，使用第7章提出的请求一响应策略进行无回溯的激励生成。对这两种方法分别进行了相关实验和数据分析。 第三部分（第10～14章）介绍形式化验证方法。形式化验证方法使用严格的数学推理来证明设计满足规范的部分或全部属性，引起了学术界和产业界的广泛关注。然而，形式化方法仍然受限于处理规模和运行时间，难以广泛应用于实际设计。针对这一问题，本书的工作重点探讨了增量等价性检验算法、包含黑盒的电路的设计验证方法、极小布尔不可满足子式的提取算法，以及针对电路设计的模型检验方法等。 第10章介绍基于电路的布尔推理常用方法。简介布尔函数的基本运算与数字硬件行为的建模方法。介绍布尔函数的规范表示方法——有序二叉判决图的概念、运算、变量排序方法，并讨论了BDD引擎在形式化验证中的应用。介绍布尔可满足性问题及其判定方法，并讨论了基于SAT的测试产生方法、等价性检验方法和有界模型检验方法。最后讨论静态逻辑蕴涵的算法与应用。第10章的内容为后面的章节研究形式化验证方法奠定了基础。

展开

FOREWORD 前言 第1章绪论 1.1 设计验证简介 1.2 设计验证中的关键问题 1.2.1 量化评估 1.2.2 激励生成 1.2.3 形式化验证 1.3 章节组织结构 参考文献 第2章寄存器传输级行为描述抽象方法 2.1 硬件描述语言概述 2.1.1 硬件描述语言的产生与发展 2.1.2 硬件描述语言的描述特点 2.2 RTL行为描述的进程分析 2.2.1 语法与语义限制 2.2.2 组合进程 2.2.3 时钟进程 2.2.4 异步进程 2.3 寄存器传输级行为描述抽象 2.3.1 行为描述中的进程 2.3.2 过程性语句 2.3.3 语句的语义行为 2.3.4 语句的执行条件 2.3.5 进程的相互关系 2.3.6 电路模型 2.3.7 行为模拟方式 2.4 本章总结 参考文献 第3章基于可观测性的覆盖率评估方法 3.1 设计验证中的可观测性 3.1.1 研究设计验证中的可观测性的意义 3.1.2 设计验证中的可观测性相关研究 3.2 可观测性的DFUDO模型 3.2.1 工作基础 3.2.2 动态参数化引用一定值链 3.2.3 HDL设计中信号可观测性的DFUD0模型 3.3 基于DFUD0模型的语句覆盖率评估方法 3.3.1 基于DFUDO模型的语句覆盖率（OSC）的定义 3.3.2 覆盖率评估算法 3.3.3 实验及分析 3.4 基于DFUDO模型的分支覆盖率评估方法 3.4.1 基于DFUDO模型的分支覆盖率（OBC）的定义 3.4.2 优化的覆盖率评估算法 3.4.3 实验及分析 3.5 两种基于DFUDO模型的代码覆盖率评估方法的比较 3.5.1 OSC与OBC的共性 3.5.2 OSC与OBC的差异比较 3.6 可观测性的COC模型 3.6.1 增强型进程控制树与数据流向图 3.6.2 控制－观测链 3.6.3 基于COC模型的可观测性的定义 3.7 基于COC模型的语句覆盖率评估方法 3.7.1 实现框架 3.7.2 电路的行为模拟 3.7.3 可观测性分析过程 3.7.4 基于COC模型的语句覆盖率的计算 3.7.5 实验及分析 3.8 本章总结 参考文献 第4章缺项－设计错误模型 4.1 设计错误模型介绍 4.2 实际芯片的设计验证 4.2.1 设计简介 4.2.2 接口逻辑的设计验证 4.2.3 处理器逻辑的设计验证 4.3 缺项－设计错误模型 4.3.1 设计错误数据的分析 4.3.2 缺项错误模型 4.3.3 缺项错误模型的测试方法 4.3.4 实验及分析 4.4 设计错误的注入 4.4.1 软件的变异测试系统Mothra 4.4.2 基于Mothra的硬件设计变异测试系统 4.4.3 独立的硬件设计错误注入系统ErrorInjector 4.5 本章总结 参考文献 第5章基于错误传播概率的量化分析方法 5.1 在量化评估方法中考虑错误效果的意义 5.2 RTL操作的错误屏蔽概率分析 5.2.1 一元操作的EMP分析 5.2.2 二元操作的EMP分析 5.2.3 常见字操作的错误屏蔽概率 5.3 基于错误屏蔽概率的静态可观测性量化分析方法 5.3.1 研究静态可观测性分析方法的动机 5.3.2 HDL设计中内部信号的静态可观测性分析方法 5.3.3 根据低观测根源选择内部观测点的方法 5.3.4 实验及分析 5.4 本章总结 参考文献 第6章模拟验证的激励生成概述 6.1 简介 6.2 遗传算法用于激励生成 6.2.1 遗传算法的起源和发展 6.2.2 遗传算法的基本结构 6.2.3 遗传算法的技术要点 6.2.4 基于模拟的激励生成与遗传算法 6.2.5 ARTIST系统 6.3 确定性激励生成 6.3.1 基于故障模型的测试生成 6.3.2 基于错误模型的激励生成 6.4 本章总结 参考文献 第7章基于传输故障模型的寄存器传输级激励生成 7.1 行为倾向驱动引擎 7.1.1 电路行为的表征与展现 7.1.2 函数或映射的属性 7.1.3 抽象的行为值与RTL变量的行为 7.1.4 行为倾向 7.1.5 驱动引擎 7.2 传输故障模型 7.2.1 电路故障的层次化抽象模型 7.2.2 传输故障的定义与组织 7.2.3 传输故障与逻辑故障的对应关系 7.3 无回溯激励生成及算法实现 7.3.1 无回溯激励生成 7.3.2 基于行为倾向驱动引擎构造无回溯测试生成算法 7.3.3 简单实例分析 7.3.4 算法特征小结 7.4 实验及分析 7.4.1 拟定的实验方案 7.4.2 系统实现方式 7.4.3 实验结果比较分析 7.5 本章总结 参考文献 …… 第8章基于行为阶段聚类的寄存器传输级激励生成 第9章覆盖率驱动的寄存器传输级激励生成 第10章布尔函数与基于电路的布尔推理 第11章基于可满足性的增量等价性检验方法 第12章验证包含黑盒的电路设计的形式化方法 第13章极小布尔不可满足问题 第14章模型检验在电路设计验证中的应用研究 第15章总结与展望 索引

展开