数字集成电路设计验证
2010-5
科学出版社
李晓维 等 著
411
无
实现所期望的功能特性是集成电路设计需要满足的最基本要求，功能验证是集成电路设计验证的基础技术，是集成电路设计的关键技术之一，是确保集成电路功能正确性的主要技术手段。 本书是全面论述数字集成电路设计验证方法的学术著作，汇集了自2000年以来中国科学院计算研究所（以下简称中科院计算所）在数字集成电路设计验证方法学研究中取得的自主创新的重要研究成果和结论。内容涉及数字集成电路设计验证的三个重要方面：量化评估、激励生成和形式化验证。 全书共15章，其中技术内容可分为三大部分。第一部分（第2～5章）量化评估，从可观测性信息和发现设计错误的能力两个角度，论述数字集成电路设计验证的量化评估方法。第二部分（第6～9章）激励生成，针对寄存器传输级的激励生成问题，从故障模型和覆盖率导向两个角度，论述确定性和非确定性的激励生成方法。第三部分（第10～14章）形式化验证，从提高处理速度的角度，论述形式化验证中的等价性检验方法和模型检验方法。 本书的主要技术内容汇集了李晓维研究员从2001年以来指导的博士生（李光辉、吕涛、鲁巍、邵明等）和硕士生（刘领一、赵阳、王天成等）的学位论文工作的部分成果；也包括李华伟和尹志刚的博士学位论文的部分成果。这些研究成果部分已经在本领域相关学术刊物和学术会议上发表。本书由李晓维研究员主持撰写，吕涛博士参与了第3～5章内容的整理；李华伟研究员参与了第2、6～9章内容的整理；李光辉教授参与了第10～14章内容的整理。清华大学计算机系边计年教授审阅了全部书稿，美国LJCSB计算机系主任郑光廷教授撰写了序言。在此表示衷心的感谢。 本书汇集的部分科研成果是在国家重点基础研究计划（973）课题“高性能处理芯片的设计验证与测试”（2005CB321605）、国家自然科学基金重点项目“数字VLSI电路测试技术研究”（60633060）和“从行为级到版图级的设计验证与测试生成”（90207002）等资助下完成的。研究过程中得到了中科院计算所李国杰院士、闵应骅研究员、胡伟武研究员、李忠诚研究员等领导和同事的关心和支持，得到了清华大学边计年教授、复旦大学唐璞山教授、浙江大学严晓浪教授、西安邮电大学韩俊刚教授等同行的支持和帮助，在此表示衷心的感谢。 由于作者水平和经验有限，书中难免存在不足之处，恳请读者批评指正。
《数字集成电路设计验证：量化评估、激励生成、形式化验证》内容涉及数字集成电路设计验证的三个主要方面：量化评估、激励生成和形式化验证。主要包括寄存器传输级（RTL）电路建模、基于可观测性的覆盖率评估方法、设计错误模型；基于故障模型的激励生成、基于RTL行为模型的激励生成、覆盖率驱动的激励生成；基于可满足性的等价性检验、包含黑盒电路的形式化验证，以及不可满足问题。 全书图文并茂，阐述了作者及其科研团队自主创新的研究成果和结论，对致力于数字集成电路设计验证方法研究的科研人员（尤其是在读研究生），具有较大的学术参考价值，也可用作集成电路专业的高等院校教师、研究生和高年级本科生的教学参考书。
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 软件的变异测试系统Mothra4.4.2 基于Mothra的硬件设计变异测试系统4.4.3 独立的硬件设计错误注入系统ErrorInjector4.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章 总结与展望索引
第6章介绍了寄存器传输级的激励自动生成方法的研究现状，主要包括：将遗传算法用于激励生成的非确定性方法，以及基于故障模型／错误模型的确定性激励生成方法。 第7章研究了基于故障模型的寄存器传输级激励生成方法。设计了行为倾向驱动引擎用于展现电路的行为，建立了一种新的故障模型——传输故障模型，基于行为倾向驱动引擎构造了传输故障的无回溯测试生成算法，实现了X_Pulling和TiDE两个测试生成系统，并进行了相关实验和数据分析。 第8章研究了从寄存器传输级行为描述出发，如何生成测试序列来检测有限状态机的状态转移关系。提出了有限状态机的行为阶段聚类描述，该描述可通过从寄存器传输级行为描述抽取状态信息得到。建立了一种新的行为级故障模型——行为阶段转换故障模型，进一步提出了一种基于聚类的测试生成算法。实现了基于行为阶段聚类的寄存器传输级自动测试生成系统ATCLUB，并进行了相关实验和数据分析。 第9章研究了以有效的覆盖率为导向的非确定性的激励生成方法。介绍了两种方法：第一种，采用设计验证常用的覆盖率评估准则，附加第7章提出的传输故障模型的覆盖准则，设计了混合遗传算法来进行激励生成；第二种，针对第3章所提出的可观测性覆盖准则COC模型，使用第7章提出的请求一响应策略进行无回溯的激励生成。对这两种方法分别进行了相关实验和数据分析。 第三部分（第10～14章）介绍形式化验证方法。形式化验证方法使用严格的数学推理来证明设计满足规范的部分或全部属性，引起了学术界和产业界的广泛关注。然而，形式化方法仍然受限于处理规模和运行时间，难以广泛应用于实际设计。针对这一问题，本书的工作重点探讨了增量等价性检验算法、包含黑盒的电路的设计验证方法、极小布尔不可满足子式的提取算法，以及针对电路设计的模型检验方法等。 第10章介绍基于电路的布尔推理常用方法。简介布尔函数的基本运算与数字硬件行为的建模方法。介绍布尔函数的规范表示方法——有序二叉判决图的概念、运算、变量排序方法，并讨论了BDD引擎在形式化验证中的应用。介绍布尔可满足性问题及其判定方法，并讨论了基于SAT的测试产生方法、等价性检验方法和有界模型检验方法。最后讨论静态逻辑蕴涵的算法与应用。第10章的内容为后面的章节研究形式化验证方法奠定了基础。
本书是全面论述数字集成电路设计验证方法的学术著作，汇集了自2000年以来中国科学院计算研究所（以下简称中科院计算所）在数字集成电路设计验证方法学研究中取得的自主创新的重要研究成果和结论。内容涉及数字集成电路设计验证的三个重要方面：量化评估、激励生成和形式化验证。 全书共15章，其中技术内容可分为三大部分。第一部分（第2～5章）量化评估，从可观测性信息和发现设计错误的能力两个角度，论述数字集成电路设计验证的量化评估方法。第二部分（第6～9章）激励生成，针对寄存器传输级的激励生成问题，从故障模型和覆盖率导向两个角度，论述确定性和非确定性的激励生成方法。第三部分（第10～14章）形式化验证，从提高处理速度的角度，论述形式化验证中的等价性检验方法和模型检验方法。
无