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