日志

浅谈逻辑仿真，形式验证及硬件仿真

已有 2589 次阅读| 2016-10-7 20:26 |个人分类:验证前沿资讯|系统分类:芯片设计

随着硬件设计复杂性的不断增加，为了能够最大程度的使得验证收敛，验证方法也越来越多，今天我们针对常见的几种验证方法做一些简单的分析，指出它们的常用应用环境以及一些优缺点，主要包含：逻辑仿真，形式验证，硬件仿真

一、逻辑仿真

从我们整个芯片的验证过程来讲，基于软件的逻辑仿真在验证中仍然起着举足轻重的作用，整个项目中的功能验证都是通过逻辑仿真来进行验证，下面我们就逻辑仿真的优缺点进行一个简单的阐述：

优点：

逻辑仿真的工具可以在标准的服务器上运行，不需要为它定制特定的服务器，减少了验证成本
在模块级别的功能验证上，逻辑仿真工具的编译速度和仿真速度很快，这在一定程度上会加快我们整体项目的验证速度
工程师对逻辑仿真验证过程的进行有很好的控制，可以随时暂停或者中断验证工具的运行，还可以以用户友好的GUI模式来进行debug，提高了debug的效率
验证环境的方便性，由于是基于软件仿真，我们的验证环境可以进入到DUT的任何一个需要被验证的地方，在特定时刻产生足够精确的数据包，进行仿真验证

缺点：

对于逻辑仿真，上面的很多优点让它在我们的验证过程中充当着主力角色，但是它有一个很大的缺点，那就是性能，尤其是当我们的设计文件比较大时，逻辑仿真速度会变得很慢，这让我们的验证速度大打折扣，这也是我们后来引入形式验证和硬件仿真的原因（以前我们只在整个SOC设计上应用硬件仿真，现在硬件仿真更早的被加入验证过程）

二、形式验证(属性检查和等价检查)

形式验证是一种静态的验证方式，旨在通过工具来从逻辑上来检查我们的设计文件满足/不满足某种属性，或者两个设计文件是否逻辑等价

优点：

形式验证是一种综合性的验证方式，我们可以设定一些属性，它会以一种严密的逻辑方式穷尽所有可能去尝试着证明我们的设计满足/不满足这种属性，不像我们的逻辑仿真存在一定的概率性，因为在逻辑仿真中我们不可能穷尽所有的可能去验证（可能要花费数年甚至几十年去穷尽所有可能），但形式验证可以做到而且往往只需要几十分钟或者数个小时
现在，形式验证现在可以应用在跨时钟域CDC(Clock Domain Crossing)验证，在CDC验证中，它可以识别CDC区域并进入电路中任何一个同步逻辑块中，建立CDC的稳定性模型并用于RTL的仿真中以确认没有这种不稳定的状态穿过Clock Domain的边界在DUT中继续进行传播；覆盖率收敛方面，形式验证也可以发挥很大作用，现在在我们的设计中会集成许多可配置可复用的设计模块，但是由于配置方式的不用，使得它的功能不同，覆盖率也就很难打到我们的要求(通常为100%)，形式验证可以根据对模块的配置做一个覆盖率的分析，如果可以覆盖，它会给出一个覆盖的例子，如果不可以那我们就需要高度重视去重新检查可不可以过滤掉

缺点：

形式验证一个很大的缺点是你不可以仿真DUT的一些动态行为，从它的工作远原理来讲，它是把我们的当前设计和一些标准的VIP（也可以是其他形式）来进行逻辑对等检查，并不能对于动态行为进行验证，所以形式验证的结果完全取决于我们提供的VIP的质量，如果VIP的质量很高，那我们的设计也没有问题，反之则不行，也正式因为这个原因使得它不能作为验证的主力军
形式验证的另一个比较大的缺点是随着设计复杂性的增加，需要对比的DUT的状态空间呈爆炸性增长，这使得形式验证更多的应用在模块级别，极大的限制了它在系统级别的应用

三、硬件仿真(Hardware Acceleration)

硬件仿真是指把我们的设计代码进行编译，并且综合为真实的硬件电路对应FPGA板子上去，通过真实的硬件电路进行仿真(FPGA原型)

优点：

仿真速度快，对于我们的DUT来讲，逻辑仿真工具的仿真速度大都在1KHz左右，通过用软件的虚拟核代替硬件核仿真速度可以达到1MHz，而FPGA原型却可以达到10MHz，利用硬件仿真，可以让我们提高验证速度，缩短验证的时间，让集成电路的发展沿着摩尔定律继续前进

缺点：

编译时间比较长，由于硬件仿真需要对设计文件进行逻辑综合并且把综合的结果对应到真实的硬件电路上去进行仿真加速，而对于基于软件的逻辑仿真却并不需要逻辑综合生成物理电路，这就使得它的编译时间相对逻辑仿真会很长
debug方式不是特别成熟，如果是一些比较容易发现的bug，可以借助硬件仿真进行，如果bug比较复杂仍然需要借助逻辑仿真工具进行，这使得硬件仿真速度很快，而debug又要回到慢速的逻辑仿真上面去，不能最大限度的发挥硬件仿真的速度优势

总结：随着验证技术的发展，逻辑仿真在验证中的使用变得越来越少，形式验证和硬件仿真正在一步步更早的踏入验证的的流程，发挥各自的作用，面对越来越复杂的硬件设计，仅仅用一种验证方式去做到验证收敛变得越来越困难，我们要结合各种验证方法一起来对硬件设计进行各个方面的检验，让我们的设计产品以很完美的姿态去完成它的使命