基于GSTE模型检测的信号并串转换模块功能验证的研究

摘要

随着集成电路设计的发展和不断更新换代,电路设计周期缩短,使得芯片的验证愈加重要。同时与日俱增的电路复杂程度也使得验证愈加困难。传统的芯片验证方法是基于模拟仿真的方式,通过测试用例,观察在给定的输入下是否能得到期望的输出。这种方法验证周期长且覆盖率有限。形式化验证是一种基于数学推理的验证方法。它将系统和其规范抽象成数学模型,通过推理得出系统是否满足规范。形式化验证方法能达到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等规模较大电路时有更好的验证性能。

目录

封面

声明

中文摘要

英文摘要

目录

第一章 绪论

1.1 研究背景

1.2 国内外发展现状

1.3 研究内容与研究意义

1.4 文章结构组织

第二章 相关理论与背景技术

2.1 常见模型检测

2.2 基于BDD的GSTE模型检测工具简介

2.3 对基于BDD的GSTE工具的分析与本文基本思路

2.4 工作平台及实验环境

2.5 本章小结

第三章 基于AIG的GSTE 模型检测

3.1 AIG简介

3.2 使用AIG的模型表示

3.3 使用AIG完成POST计算

3.4 使用AIG的cons验证

3.5 使用AIG的局限

3.6 本章小结

第四章 结合AIG和SAT的GSTE模型检测

4.1 SAT求解器

4.2 AIG与CNF范式的转化

4.3 使用SAT求解器的量词消除

4.4 基于电路分解的量词消除

4.5 使用SAT求解器和使用AIG、BDD的比较

4.6 本章小结

第五章 实验结果与分析

5.1 SPDIF_ENCODE模块及其断言图设计

5.2 实验与数据分析

5.3 本章小结

第六章 总结与展望

6.1 全文总结

6.2 下一步的工作与展望

致谢

参考文献

攻读硕士期间取得的研究成果