本书是全面论述数字集成电路设计验证方法的学术著作，汇集了自2000年以来中国科学院计算研究所(以下简称中科院计算所)在数字集成电路设计验证方法学研究中取得的自主创新的重要研究成果和结论。内容涉及数字集成电路设计验证的三个重要方面：量化评估、激励生成和形式化验证。

全书共15章，其中技术内容可分为三大部分。第一部分(第2～5章)量化评估，从可观测性信息和发现设计错误的能力两个角度，论述数字集成电路设计验证的量化评估方法。第二部分(第6～9章)激励生成，针对寄存器传输级的激励生成问题，从故障模型和覆盖率导向两个角度，论述确定性和非确定性的激励生成方法。第三部分(第10～14章)形式化验证，从提高处理速度的角度，论述形式化验证中的等价性检验方法和模型检验方法。

本书内容涉及数字集成电路设计验证的三个主要方面：量化评估、激励生成和形式化验证。主要包括寄存器传输级(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章 基于可观测性的覆盖率评估方法

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

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

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

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

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

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

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

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

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

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

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

第15章 总结与展望

索引