视频加载中...

注：本推文中的很多内容参考研究生期间所写形式验证章节of教材 《模拟集成电路与数字集成电路设计工具实用教程》( 已出版）。

Formality简介

在现在的数字集成电路设计流程中，有很多步骤都需要进行验证。随着数字集成电路的规模、复杂度，以及在验证过程中需要的仿真矢量的不断增加，用传统的仿真器进行验证越来越成为整个设计过程中的瓶颈之所在。

为了确保设计达到所需要的各方面的要求，需要数量众多的仿真矢量。而数量众多的矢量、日益增大的设计规模，都增大了验证过程中需要交换和处理的数据量。此外，由于电路尺寸和复杂度的增加，对于每一个激励，逻辑仿真工具都要进行更多的处理，也是导致这个瓶颈的因素之一。

在这样一种背景下，形式验证（Formal Verification）技术显示出了较多的优点。本推文将对Synopsys的形式验证工具Formality的功能、特点、使用流程以及脚本进行讲解。

Formality的基本特点

所谓形式验证，就是通过比较两个设计在逻辑功能上是否等同的方法来验证电路的功能。这种方法的优点在于它不仅提高了验证的速度，可以在相当大的程度上缩短数字设计的周期，而且更重要的是，它摆脱了工艺的约束和仿真testbench的不完全性，更加全面地检查了电路的功能。

Formality是形式验证的工具，你可以用它来比较一个修改后的设计（如ECO）和它原来的版本，或者一个RTL级的设计和它的门级网表，再或者综合后的门级网表和 做完布局布线及优化之后的门级网表在功耗上是否一致 。

Formality有下面一些特点：

跟事件驱动的仿真器相比，能更快验证出两个设计在功能上是否等同；不依赖于矢量，因此能提供更完全的验证；可以实现 RTL-to-RTL 、 RTL-to-gate 、 gate-to-gate 之间的验证；有定位功能，可以帮助你找出两个设计之间功能不等同的原因；可以使用的文件格式有 VHDL 、 Verilog 、 Synopsys 的 .db 格式，以及 EDIF 网表等；可以实现自动的分层验证；使用 Design Compiler 的工艺库；同其他 Synopsys 工具一样，提供两种界面：图形用户界面 GUI 和命令行界面，其中 GUI 界面启动命令为： formality ，命令行界面启动命令为： fm_shell 。