Formality 与 Formality Ultra 

可验证由 DC 综合的最难的设计   

概览
Formality® 是一款等效性检查 (EC) 解决方案,该解决方案使用形式静态技术来确定某一设计的两个版本之间是否具有等效功能。

当今的设计规模大、复杂度高,同时面临时序、面积、功耗和进度等诸多挑战,要求最新、最先进的综合优化必须可被完全验证。

Formality 支持所有 DC Ultra 和 Design Compiler Graphical 的优化,因此可提供完全可验证的最佳结果质量。

Formality 支持对上电和断电状态、多电压、多电源和门控时钟设计进行验证。

Formality Ultra 新增创新的匹配和验证技术,能够高效地指导设计人员实现功能性 ECO,并把对设计的影响降到最低,而且还能在几分钟内对有着数百万例化单元的设计验证其 ECO 的正确性。这些功能有助于设计者在设计周期后期缩短一半用于完成 ECO 的时间,并获得费时更短且更具有可预测性的进度。

Formality 的易于使用且基于流程的图形化用户界面和自动设置模式有助于用户(即使是新用户)在最短的时间内成功完成验证。

下载数据手册

主要优点
  • 与 DC Ultra/Design Compiler Graphical 完美匹配 — 支持所有默认优化
  • 直观且基于流程的图形化用户界面
  • 可验证低功耗设计,包括上电和断电状态
  • Formality Ultra 向 Formality 中添加了 ECO 实现辅助、 快速 ECO 验证和高级调试等功能
  • 自动设置模式可以减少因设置信息不正确或者缺失而导致的“假故障”
  • 多核验证提升性能
  • 自动化的指导提高了与 DC Ultra/Design Compiler Graphical 配合的形式验证的完成度
  • 采用 ESP 技术时可验证全定制设计和存储器设计

Formality
最全面的等效性检查解决方案
Formality 可以让经 DC Ultra/Design Compiler Graphical 综合得到的设计更好地完成形式验证,DC Ultra/Design Compiler Graphical 采用拓扑技术,实现了与版图后时序、面积和功耗结果间准确的相关性,并提供重定时、反相和取消逻辑层次等高级优化功能。Formality 还与可用于预测和缓解布线拥塞的 Design Compiler Graphical 完全兼容。设计人员不再需要通过禁用 Design Compiler 的强大优化功能以通过等效性检查。DC Ultra/Design Compiler Graphical 搭配 Formality,可提供完全可验证的最优结果质量 (QoR)。

Formality 与 Formality Ultra
图 1:Formality 等效性检查解决方案

具有自动设置模式,简单易用
Formality 的自动设置模式可以通过减少因设置信息不正确或者缺失而导致的假故障来简化验证过程。自动设置应用了 Formality 中的设置信息,以匹配 DC Ultra/Graphical 所作的假设,包括命名样式、未使用的引脚、测试输入和门控时钟信息。

自动定位 RTL、网表和库等关键文件。所有自动设置信息均在摘要报告中列出。

指导设置
Formality 可以通过使用 DC Ultra/Design Compiler Graphical 自动生成的指导设置文件来解释综合优化。指导设置包括综合时可能出现的名称变更、寄存器优化、乘法器结构和很多其他设计转换信息。这种“构建即正确”的信息使得在匹配和验证阶段可使用最高效的算法,改善性能与一次性验证通过的完成度。

由 Formality 指导的设置采用标准文档格式,可以消除出现在依赖日志文件解析的工具中的不可预测性。

独立验证
指导设置流程的各个环节均已经过隐式或者显式的验证,所有内容均可在一个 ASCII 文件中查看。

图形化用户界面
Formality 提供一个基于流程的图形化用户界面,旨在实现开箱即用的可用性。可同时显示参考设计和实现设计。自动逻辑锥修剪使工具仅显示参考设计和实现设计之间的差异,降低复杂性。

Formality 与 Formality Ultra
图 2:自动逻辑锥修剪提高了调试时电路图的可读性

Hier-IQ™ 技术
获得专利的 Hier-IQ 技术提供了层次化验证的性能优势以及扁平化验证的开箱即用的可用性。

Error-ID 技术
Error-ID 可以识别出导致两个设计表示形式之间真正功能差异的确切逻辑。存在多个差异时,Error-ID 可以隔离和报告多个逻辑差异。Error-ID 也能提出可修正指定功能差异的替代逻辑;这种灵活性让设计人员可以选择最容易实现的设计变更。

失败样本显示窗口
所有失败的输入样本都可用熟悉的类似电子表格的格式查看。失败样本窗口是一种能够快速识别出表明验证失败或者不正确设置原因走向的非常理想的方式。

感知电源的验证

Formality 与 Formality Ultra
图 3:直观查看失败样本窗口即可轻松识别问题领域

Formality 与 Power Compiler 完全兼容,支持对上电和断电状态、多电压、多电源和门控时钟设计进行验证。

参考设计模块加电时,Formality 可验证其功能性。如果实现设计加电方式不同,则会提示故障点。

Formality 可核对参考设计断电时实现设计是否断电,并在实现设计未按预期断电时检测其功能状态。有效的电源状态均在电源状态表 (PST) 中确定。

电源功耗意图通过 IEEE 1801 UPF 传达给 Formality。

Formality 与 Formality Ultra
图 4:从电路图视图中可轻松查看和调试电源连接性

加快结果产生速度
多核验证增强了 Formality 的性能。Formality 可以同时使用多达四个芯核来验证设计,从而缩短验证时间。

其他省时功能
Formality 的层次化脚本设计功能可以提供无需额外设置便可调查子模块的方法,是隔离问题和验证修复效果的理想方式。

代码阅读器可以打开 RTL 和网表源文件,高亮显示所选例化单元的出现位置。这样有助于用户将 RTL 与门级设计版本关联到一起。

错误区域关联功能让用户可以快速、直观地在一个设计中识别出与 Error-ID 在其他设计中隔离的错误相关的逻辑。

命令行编辑功能使用户在使用 Formality 命令行时可以利用历史记录和常规文本编辑器的命令。

Formality Ultra
主要优点
Formality Ultra 可以为 Formality 提供图形化界面驱动 的 ECO 实现辅助、快速 ECO 验证和高级调试。Formality Ultra 可以指导用户完成 ECO 实现,然后仅对变更了的逻辑做快速验证。

Formality Ultra ECO 流程
Formality Ultra 使用 ECO RTL 和未修改的网表。带有指导的图形化界面驱动的变更将更新到网表。实现 ECO 之后,可以仅对受到影响的逻辑锥进行快速验证,而无需对设计进行全面验证运行来验证 ECO 是否正确实现。

实现并全面验证所有 ECO 后,将生成 IC Compiler 命令列表,协助将物理变更实现到设计中。

ECO 指导
Formality Ultra 突出显示出参考设计和实现设计之间的等效网线,以及由于参考设计中 ECO 变更而导致等效性缺失的网线。这样有助于设计人员快速识别出在实现过程中应该进行哪些变更。

实现 ECO
可以使用 Formality Ultra 中的编辑命令调用 Formality Ultra 图形界面来修改现有的网表。

Formality 与 Formality Ultra
图 5:突出显示参考设计(左边)与实现设计(右边)之间的等效网络

Formality 与 Formality Ultra
图 6:在已完成的 ECO 上,电路图以黄色显示受 ECO 影响的网络,以橙色显示新的元件和网线

Formality 与 Formality Ultra
图 7:Formality Ultra 运行提示显示受 ECO 影响的设计部分已成功经过局部验证

快速的 ECO 验证
Formality 可以识别和单独验证受 ECO 影响的设计部分,确保正确实现 ECO。如果 ECO 验证失败,则可交互式“撤销”ECO,再次进行新的编辑。部分验证通过后,再实施变更。部分验证免去了验证整个设计的麻烦,可确保 ECO 正确实现,同时显著缩短实现和验证 ECO 所需的总时间。

兼容 IC Compiler
实现和验证所有 ECO 后,需进行最后的全面验证运行,以确保 ECO RTL 和 ECO 网表具有功能等效性。

Formality Ultra 可以生成兼容 IC Compiler 的 ECO 命令文件,简化物理设计阶段的实现过程。

高级调试
Formality Ultra 具有高级调试功能,可以帮助设计人员识别和调试未通过的验证。设计人员可以找到参考设计和实现设计之间的对比点,即等效(和反向等效),通过交互式修改设计来进行“假设”分析,并验证两点(或者多点)之间的等效性。

晶体管验证
ESP 搭配 Formality,可以对定制电路、嵌入存储器和复杂 I/O 进行快速验证。ESP 技术可以直接读取现有 SPICE 和 RTL 行为模型,且不需要限制性的映射和转译。

输入格式
  • Synopsys DC、DDC、Milkyway
  • IEEE 1800 SystemVerilog
  • Verilog-95、Verilog-2001
  • VHDL-87、VHDL-93
  • IEEE 1801 Unified Power Format (UPF)
指导设置格式
  • Synopsys V-SDC
  • Formality 指导文件 (SVF)
平台支持
  • Linux Suse、Red Hat 和 Enterprise
  • SPARC Solaris

如需有关 Synopsys 产品、支持服务或培训的更多信息,请访问网站:www.synopsys.com、联系您当地的销售代表或致电 650.584.5000。