论文部分内容阅读
随着集成电路设计的发展和不断更新换代,电路设计周期缩短,使得芯片的验证愈加重要。同时与日俱增的电路复杂程度也使得验证愈加困难。传统的芯片验证方法是基于模拟仿真的方式,通过测试用例,观察在给定的输入下是否能得到期望的输出。这种方法验证周期长且覆盖率有限。形式化验证是一种基于数学推理的验证方法。它将系统和其规范抽象成数学模型,通过推理得出系统是否满足规范。形式化验证方法能达到100%的覆盖率,且能给出相关反例。但该方法由于计算复杂度的问题,只适用于较小规模的电路验证,规模增大后会带来状态爆炸的问题。为提高验证效率和验证规模,需要使用良好的数据结构和算法验证模型构筑验证系统。本文从常用形式化验证数据结构和关键算法出发,结合相关技术的对比,讨论了将AIG和SAT求解器应用到模型检测算法GSTE中的方法,以期望提高验证的规模和效率。同时本文对GSTE算法的理论做了若干补充。文中首先简要介绍了几种常用的模型检测方法并分析了其优缺点,其次介绍了GSTE模型检测方法,包括它对STE的扩展以及断言图等内容,并对其理论做了一定补充,证明了一种缩小断言图存储空间方法的正确性。通过对模型检测常用数据结构BDD的分析,基本找出了其验证范围限制的原因并确立了以AIG为主要数据结构的策略。同时,文中使用量词调度的方法,有效控制了验证过程中AIG的规模,并对调度方法进行一定改进,使调度更加快速有效。在使用AIG的同时,本文设置了若干阈值,在合适的时间使用BDD对AIG进行化简并在可行时,直接使用BDD继续验证。通过和基于BDD的方法对比,使用AIG可以很大程度上减少内存消耗,从而给提高验证规模带来可能。针对使用AIG仍然可能存在的状态爆炸问题,本文在AIG验证遇到瓶颈时,结合使用SAT求解器完成验证中关键的计算步骤,即量词消除,解决了AIG状态爆炸问题。并且文中通过使用针对SAT求解器验证的优化,有效地减少了量词消除所需时间,整体上提高了验证效率。通过与基于BDD的GSTE模型检测方法的性能对比,证明了结合AIG和SAT求解器的验证方法有效地提高了验证规模,并且在验证例如SPDIF_ENCODE等规模较大电路时有更好的验证性能。