Formality Equivalence Checker Comprehensive, Fast, Intuitive

Overview
Formality® 2007 is an equivalence-checking (EC) solution that uses formal, static techniques to determine if two versions of a design are functionally equivalent. EC tools verify large designs quickly and completely without the use of test vectors. Formality supports all major hardware description languages, database formats, flows, and implementation design optimizations to provide the most comprehensive verification solution available. Superior completion, time to results, and ease of use make Formality the number one customer-chosen EC verification solution.

Key Benefits

• Exhaustive verification, without test vectors, in a fraction of the time consumed by traditional dynamic techniques
• Proves functional correctness of register retiming, complex datapath, phase inversion, ECO, and low power implementations — from within a single product
• Extends leading performance advantage with built-in distributed verification
• Reduces user setup with verified automated guidance
• Expands verification productivity to every engineer with flow-based graphical interface
• Maximizes the life of your current hardware investments with leading capacity and performance
• Verifies full-custom and memory designs when including ESP technology

Figure 1. Synopsys full-chip equivalence checking.

The Most Comprehensive Verification Solution
Advanced Datapath Verification
Formality’s revolutionary arithmetic proof engine provides the fastest arithmetic verification performance and completion. While traditional EC solutions are limited by increasing bit widths and complexity, Formality’s solution is fully scalable. Optimizations, such as adder tree rebalancing, resource sharing, and operator merging can be easily verified using Formality.

Retimed Design Verification
Retiming shifts registers across combinational logic to transfer the associated delay from a path with negative slack to a neighboring path with available slack. Circuit retiming introduces changes that strike at the fundamental techniques used by the typical equivalency checking tool. Formality’s breakthrough technology allows you to realize the QoR benefits of full-chip register retiming in a fully verifiable flow.

ECO Verification and Implementation
Formality can help debug and implement functional ECOs by identifying areas of logic that need to be changed to bring two design representations into functional correlation. Additionally, Formality can be used to prove that ECOs have not had any unintentional functional impact.

Figure 2. Problem areas can be easy identified by visual inspection of the Failing Pattern Window. In this example, the constant value of test_se for all failing patterns indicates that it is essential to the failure and, in this case, needs to be set as a constant 0 to disable test.

Low Power Verification
Formality’s built-in capabilities verify that low-power optimizations have not changed a design’s intended functionality. Additionally, Formality contains support for RTL-driven low power implementation.

Transistor Verification
ESP solutions combine with Formality to offer fast verification of custom circuits, embedded memories, and complex I/Os. ESP technology directly reads existing SPICE and behavioral RTLmodels and does not require restrictive mapping or translation.

Formality’s Ease of Use
Formality can account for design optimizations automatically through the use of guided setup scripts generated during implementation. Guided setup includes information about name changes, register optimizations, multiplier architectures, and numerous other transformations that may occur during design implementation. Correct-by-construction setup improves performance and first-pass completion by utilizing the most efficient algorithms during matching and verification. Formality guided setup is a standard, documented format that removes dependencies found in tools relying on log file parsing. In the Formality flow, all information is independently proven and is available for your review.

Hier-IQ™ Technology
An advanced way to verify designs, patented Hier-IQ technology provides the performance benefits of hierarchical verification with flat verification’s out-of-the-box usability. Hier-IQ technology is a primary reason for Formality’s market-leading capacity and performance.

Error-ID Technology
Error-ID identifies the exact logic causing real functional differences between two design representations. Error-ID can isolate and report several logic differences when multiple discrepancies exist. Error-ID will also present alternative logic that can be changed to correct a given functional difference; this flexibility allows you to select the change that is easiest to implement.

Failing Pattern Display Window
View all failing input patterns in spreadsheet-like format and select which pattern to apply to the design. The failing pattern window is an ideal way to quickly identify trends indicating the cause of a failing verification or improper setup.

Graphical User Interface
Formality provides a flow-based environment designed to promote out-of-the-box usability. All verification and design engineers will benefit from Synopsys’ industry knowledge by operating within an environment specifically created to match the way experienced verification engineers think.

Accelerated Time to Results
Distributed Verification
Formality’s leading single processor performance advantage can be multiplied with the addition of distributed verification. This inherent Formality feature verifies your design using up to four processors simultaneously to reduce your verification time.

User-Set Effort Levels
In Formality, you have full control over how much time and/or effort is spent verifying your design. A quick verification pass before addressing the more complex points allows you to start debugging any differences straight away.

Figure 3. Formality’s Error-ID technology enables you to quickly find, isolate, and repair functional differences.

True Incremental Capability
To minimize iterations, matching and verification are run incrementally. Incremental matching allows you to layer available matching techniques and experiment with matching rules. Incremental verification allows analysis of current results while continuing the verification of points not yet proven.

Other Time Saving Features
Formality’s Hierarchical Scripting provides a method to investigate sub-blocks without additional setup and is ideal for isolating problems and verifying fixes.

Formality’s Source Browsing opens RTL and netlist source files to highlight occurrences of a selected instance. This can help users correlate between the RTL and gate-level design versions.

Error Region Correlation provides a quick, visual identification of the logic from one design that correspond to the errors isolated by Error-ID within the other.

Command Line Editing allows you to take advantage of history and common text editor commands when working from Formality’s command line.

Accurate Results
Simulation vs Synthesis Interpretation
When simulation and synthesis semantics differ, design intent is unclear. Formality’s RTL parsers will by default consider these occurrences to be errors. This is the safest approach; synthesis interpretation may miss real design errors. Once you have determined that a particular coding style is safe, Formality can be directed to obey the synthesis semantic.

Independent Verification
Value links between implementation and verification tools significantly improve performance and ease of use, yet all designs continue to be read and elaborated using independent technology. Every aspect of a guided setup flow is either implicitly or explicitly verified, and all content is available for inspection.

Input Formats
Synopsys DC, DDC, Milkyway
SystemVerilog 3.1a
Verilog-95, Verilog-2001
VHDL-87, VHDL-93
Spice (Formality-ESP)

Guided Setup Formats
Synopsys V-SDC
Formality Guide Files (SVF)

Platform Support
Sun Solaris
HP-UX
IBM AIX
Linux Suse, Red Hat and Enterprise