集成电路形式化验证的FPGA加速技术研究

• 作 者: 丁广泓
• 发表日期: 2015年01期
• 关键词: 现场可编程门阵列 集成电路验证 可重构计算 可达性分析工具 形式化方法

模拟和混合信号电路已经广泛应用于电子消费、电通讯、电子医疗等很多领域。但是,在深亚微米设计中,物理效应可能会破坏常见的数字抽象化后的电路行为。本文采用混杂系统的方法对模拟和混合信号电路模型进行形式化的验证。提出了电路级验证的形式化方法,此方法是基于变迁验证问题的可达性分析问题,利用非线性常微分方程的改进节点分析模型对电路的动力学行为建模,计算从给定初始状态向前探索能达到的所有可能的电路行为。模拟电路行为的性质确保完全正确的发现设计的缺陷。并针对由非线性常微分方程建模的电路系统的验证需求,提出了一种新的集成电路形式化验证的硬件方法,采用FPGA作为硬件加速部件,加速Coho形式化验证算法的计算。采用Sysgen工具重新改写Coho形式化验证算法,将Coho形式化验证算法的求解变成对应的硬件电路的设计问题,通过设计合适的硬件完成形式化验证的计算。实验结果表明,与Coho验证算法的软件执行时间相比,硬件实现可以获得10倍左右的性能加速。本研究能够进一步扩展Coho的应用领域,尤其是扩展到以前因为计算性能无法应用的领域。