基于FPGA,的集成电路形式化验证加速
摘要摘要：OpenCoho是一个通过可达性分析及计算对集成电路设计进行形式化验证的软件工具。它可以验证由非线性常微分方程建模的电路系统的正确性。提出基于FPGA的验证算法硬件加速方法，探讨环形振荡器电路有效性验证，通过仿真说明该方法的可行性和意义。实验结果表明，利用该方法平均验证速度提高了约10倍。
关键词关键词：形式化方法；集成电路验证；OpenCoho；FPGA
DOIDOI：10.11907/rjdk.151218
中图分类号：TP303
文献标识码：A文章编号文章编号：16727800（2015）004005203
0引言
随着电路设计复杂度的不断增强，电路验证的重要性日益突出。然而，传统验证方法不能涵盖系统所有可能出现的问题。形式化验证方法可以对其功能进行详细验证，越来越受到关注。
对于同时包含离散分量与连续分量的数字电路，要将验证的问题公式化，可以通过可达性分析解决。这种电路可以用常微分方程建模，将电路验证问题等价于计算常微分方程模型的可达状态集和检验电路在这些状态的属性。
OpenCoho是一个可以验证模拟或混合信号电路性质的形式化验证软件工具[2]（简称Coho）。其特点如下：①使用常微分方程来近似电路系统；②可以应用于非线性的电路模型[2]；③可以有效处理复杂度高的问题。Coho已经应用于Van der Pol振荡器、Yuan-Svensson触发器、Rambus环形振荡器、异步电路等典型电路。
本文介绍Coho验证电路性质的一般流程、探讨利用System Generator[4]来加速Coho的核心模块Mode的方法和技术[3]、描述Mode的硬件设计[5]，验证环形振荡器电路的有效性，并对结果进行对比分析，最后得出结论。
1Coho
1.1形式化验证
形式化模型是使用数学形式化规则将特定系统形式化而成的抽象数学模型，形式化验证即对此模型的验证。此方法可以应用于硬件系统、软件系统、网络协议、飞机系统等。一般来说，其涉及的数学模型包括有限状态机、标记变迁系统、佩特里网络等。
近年来，形式化验证成功应用于离散系统数字电路和通信协议领域。将形式化验证技术应用领域扩展到连续动力学系统尚具有一定挑战性。
混杂系统是同时包含离散行为与连续行为的动力学系统。在嵌入式系统、飞行控制器和同时带有数字信号及模拟信号的电路常用到混杂系统。越来越多的计算机成为关键安全系统的自动控制器，模拟电路对深亚微米集成电路的影响日益加大。
一般称混杂系统的形式化模型为混杂自动机。大部分非线性混杂系统的验证问题是不可判定的。对这类系统的验证要用到针对混杂系统的可达性分析。
1.2相关知识
“微分包含”经常被用于研究混杂系统。微分包含（ODI）是指具有如下形式的常微分方程（ODE）：
dxdt∈F（x，t）
其中，F（x，t）表示一个集合，而非实数空间中的一个点。
电路系统一般可以分为模拟电路系统和数字电路系统。模拟电路系统对连续电信号进行处理，数字电路系统对离散电信号进行处理。
混杂电路系统指同时具有连续动态和离散事件动态行为，且二者之间相互作用的电路系统。由于混杂电路系统是非线性的，其模型用微分包含表示，所以对混杂电路系统进行可达性研究必须用到近似方法。
过近似常用于可达性分析，其在保持原空间性质不变的基础上，对原空间进行适当扩大，使其更适合验证和计算。
过近似的优点是能验证系统的不安全性，如果扩大后的空间不满足安全性，那么原空间一定也不满足。
1.3Coho及Coho可达性验证流程
Coho是一个对用非线性常微分方程建模的系统进行可达性分析的工具。为了便于计算，Coho用过近似的方法将每一段的非线性ODI模型近似成了线性ODI模型。近似后的模型如下：
直到模型时间结束或遇到不可达情况。
2电路中的系统级建模
2.1使用System Generator进行硬件设计
System Generator是一个借助FPGA硬件设计来进行系统级建模的工具。它扩展了Simulink的许多功能，使得到的模型更适合硬件设计。在传统软件设计方法中，一般采用Matlab、Java、C语言等来描述各个功能模块，进而实现系统建模。如果在寄存器传输级中将Matlab等语言描述经人工转换为HDL语言，要求设计人员要同时掌握这两类语言，而且这个转换过程会花费大量的时间和精力，还可能会产生一些错误，从而降低了开发效率。
2.2设计流程
图1描述了System Generator设计过程。首先，在Matlab算法中完成系统建模后，通过调用System Generator将simulink模型转换成硬件可执行模型；然后，在Xilinx综合工具ISE中进行布局布线；最后，生成bit流文件并下载到FPGA中，从而完成算法设计到硬件的实现。
3Coho加速设计
3.1Coho的系统结构
Coho有两个主要组件：一个使用Matlab编写，另一个使用Java编写。图2为Coho的系统结构图。
Matlab组件提供了用户操作界面，由于需要验证的系统模型被写成了Matlab的数据格式，用户通过输入一系列Matlab函数来操作Coho。这些函数包括建立模型、定义多面体和计算可达区域。系统模型构建与可达空间模型构造也是在Matlab中完成。Java组件的主要功能是计算投影多边形和线性规划求解。Java组件和Matlab组件通过一个C程序作为管道进行通信。
3.2Mode模块
Matlab组件中的Mode模块至关重要，在Coho中被频繁调用。Coho在Mode模块消耗的时间占整个软件运行时间的40%～45%。Mode模块的功能是实现可达性计算，根据每两个相邻离散时间段的多面体是否相交，推断其是否可达，进而生成轨迹。计算多面体是否相交[8]，即判断一个多面体的顶点中是否至少有一个在另一个多面体内，其运行速度很大程度上影响整个软件的性能。Mode模块因为涉及大量的矩阵运算，所以速度并不理想。
3.3硬件加速Mode模块
图3是将Mode模块硬件化的总体设计图。Coho的Matlab组件计算多面体的顶点后将其输入到FPGA中，FPGA判断顶点是否在另一个多面体内，将结果返回Matlab组件。Mode模块的功能用System Generator辅助设计实现。设计如图4所示，F1、F2、F3是输入的激励，MCode是判断点是否在多面体内的核心算法单元，其应用的Matlab函数包括多面体每个面的方程。当有输入进入Mcode时， Matlab函数根据输入的不同对其进行相应处理，最后得出结果。
4实验与性能分析
4.1实验环境
本文在测试平台上实现了Coho算法加速器。测试平台由一台主机和一块FPGA算法加速器构成，通过PCI-E×8接口相连。主机配置为Intel四核I5处理器，4.0GB内存。硬件加速器是Xilinx公司生产的VC707原型。
环形振荡器具有不稳定性，电压在跳变过程中可能会达不到要求值，所以验证环形振荡器的有效性尤为重要。
选取一个环形振荡器作为实验对象，该振荡器由3个反相器组成，取各反相器的输出电压为侦测变量，检测其有效性。输出结果是一维向量，如果向量中的元素是同号的，表示代表电路模型的多面体相交。当系统模型验证结束时，如果没有多面体不相交，则系统模型可达，即环形振荡器有效，否则无效。
4.2FPGA综合结果
测试Coho的Mode模块在FPGA上的运行情况，结果显示硬件加速器的计算结果与软件计算结果完全一致。
从表1可以看出，相对于Coho常规执行时Mode模块占用的时间，Mode模块硬件化可获得超过10倍的加速效果；并且规模越大，节省时间越多。Coho的整体运行时间将节约35%～40%。
5结语
Coho是形式化验证领域的一个重要软件平台，目前基于通用处理器平台的Coho计算量大。针对此问题，本文在FPGA的基础上，对Coho的可达性分析算法加速，通过将Coho的核心模块硬件化，使计算速度提高了约10倍，并正确验证了一个环形振荡器的有效性。结果表明，基于FPGA的硬件加速有效提高了Coho的性能，对形式化方法在混杂系统中的应用具有重要意义。
参考文献参考文献：
[1]CHAO YAN. Coho a verification tool for circuit verification by reachability analysis[D]. Columbia：University of British Columbia，2006.
[2]CHAO YAN. Formal verification of c-element circuits[C]. Asynchronous Circuits and Systems （ASY NC），2011 17th IEEE International Symposium ，2011： 55-64.
[3]张晓梦，张涛.基于FPGA实现CT图像重建加速的设计[J].液晶与显示，2014（3）：455-460.
[4]蒋小燕，宗华姣，成旭，等.软件导刊，2013，12 （7）： 104-105.
[5]宋庆增，张金珠，武继刚.时域有限差分算法的FPGA加速技术研究[J].计算机工程与科学，2013（9）：1-6.
责任编辑（责任编辑：陈福时）