VLSI设计中的形式验证方法研究

摘要

超大规模集成电路(VLSI)的设计日趋复杂，验证工作越来越繁重，验证难度也越来越大。在复杂的VLSI设计中，验证过程所需的时间约占整个设计周期的三分之二，设计过程所需要的专业验证工程师人数大约是设计工程师的两倍，功能验证已成为VLSI设计的瓶颈。传统的软件模拟和硬件仿真需要花费大量的时间，且不能完全保证功能的正确性。形式验证作为传统验证方法的补充，日益引起人们的关注。形式验证使用严格的数学推理来证明设计满足规范的部分或者全部属性，所需要的验证时间比较少，是克服验证瓶颈的可行途径。本文对VLSI的形式验证方法进行了研究，主要工作如下： 1)针对数据密集型电路的等价性验证，提出了WGL模型的改进模型——W2GL。WGL的节点是位级变量，在字级算术运算表示方面具有局限性，而W2GL能有效地表示字级算术运算。本文还证明了一个有序的、简化的W2GL模型是最小的和正则的，并提出了W2GL模型的变量排序方法及加法和乘法算法。运用这些方法和算法可以构建寄存器传输级(RTL)电路的有序的、简化的和正则的W2GL模型，进行电路优化前后的等价性验证。实验结果表明，与*BMD和WGL模型相比，W2GL模型对数据密集型电路的等价性验证不论在存储空间还是在CPU运行时间上均有明显的减少。 2)针对同时包含字级、位级变量算术运算和逻辑运算的复杂电路的等价性验证，对W2GL模型进行扩充，提出了混合WGL模型—HWGL。W2GL模型能有效地表示字级算术运算，但在表示字级逻辑运算时比较复杂，需要把字级变量拆分成位级变量。本文提出的HWGL模型既可以有效表示字级的算术运算和逻辑运算，又可以有效表示位级的算术运算和逻辑运算。对复杂电路构建HWGL模型，可实现优化前后电路的等价性验证。HWGL模型的大小与字长无关，并且需要较少的节点和构造时间。实验结果表明，对复杂的包含字级变量和位级变量的电路，HWGL比W2GL和*BMD更有效。 3)针对性质检验问题，本文在HWGL模型的基础上，提出了一种分支WGL模型—BWGL。BWGL模型是对HWGL模型的扩充，模型中用到的变量节点是HWGL，并在模型中增加了分支节点、Union节点和Intersect节点。把BWGL模型应用于性质检验，把设计中的性质描述成一个线性时间逻辑，根据时间片选择不同的检验过程验证性质是否满足。把基于BWGL的性质检验与基于BDD的VIS系统进行比较，实验结果表明，在处理器验证方面，基于BWGL的性质检验比VIS系统更有效，可以利用较少的资源在较短的时间内完成验证。另外，基于BWGL的性质检验可以同时验证数据通路和控制器，节省了大量的时间。

目录

文摘

英文文摘

声明

第1章 绪论

1.1课题的研究意义

1.2 VLSI的设计流程

1.3 VLSI的功能验证概述

1.3.1模拟验证

1.3.2形式验证

1.3.3半形式化验证

1.4形式验证方法

1.4.1等价性验证

1.4.2模型检验

1.4.3定理证明

1.5形式验证的研究现状

1.5.1基于可满足的形式验证

1.5.2基于多项式的形式验证

1.5.3基于判决图的形式验证

1.6本文的主要工作

1.7本文的组织结构

第2章W2GL模型

2.1引言

2.2现有的WGL模型

2.3 W2GL模型

2.3.1 W2GL的构建

2.3.2 W2GL的化简

2.3.3 W2GL的位级逻辑运算表示

2.4本章小结

第3章基于W2GL的数据通路等价性验证

3.1引言

3.2 W2GL的变量排序

3.2.1 W2GL局部互换算法

3.2.2启发式排序

3.3 W2GL的算法

3.3.1加法算法

3.3.2乘法算法

3.4基于W2GL的等价性验证

3.5实验结果

3.6本章小结

第4章 基于HWGL的RTL等价性验证

4.1引言

4.2目前已经存在的模型

4.2.1 BDD模型

4.2.2 WLDD模型

4.2.3 W2GL模型

4.2.4几种模型表示能力比较

4.3 HWGL模型

4.3.1字级算术操作表示

4.3.2位级逻辑操作表示

4.3.3字级逻辑操作表示

4.4基于HWGL模型的验证实例

4.4实验结果

4.5本章小结

第5章基于BWGL的性质检验

5.1引言

5.2 BWGL模型

5.2.1字级操作的语法和语义

5.2.2 BWGL的构造

5.2.3 BWGL的操作

5.3设计中的性质检验

5.4 DFG-BWGL转化

5.5性质检验过程

5.5.1 CheckComb过程

5.5.2 CheckX 过程

5.5.3 CheckXn 过程

5.6处理器验证

5.6.1处理器的功能

5.6.2验证过程

5.7实验结果

5.8本章小结

结 论

参考文献

攻读博士学位期间发表的论文和取得的科研成果

致 谢