Synopsys Cloud
Cloud native EDA tools & pre-optimized hardware platforms
Request a Free Trial →
System-on-chip (SoC) designs continue to increase in complexity and move to advanced nodes to meet the connectivity and functionality demands of today’s smart everything applications. This results in aggressive optimizations, increasing die sizes, and more sophisticated architectures. To meet ambitious design needs while facing shrinking time-to-market windows and the already-challenging prospect of catching errors throughout the design and testing process, design teams need to constantly push the limits of power, performance, and area (PPA).
Functional verification tools can help detect and correct some of these errors. However, with the push to optimal PPA, engineers often need to scale down optimizations to sacrifice quality of results (QoR). A more predictable technique is needed to respond quickly to frequent, unexpected functional changes and determine if an alternate design representation would behave the same way as a verified version.
This is where the concepts of formal equivalence checking and functional engineering change order (ECO) come in.
Read on to learn more about the basics of equivalence checking and functional ECO, current challenges in the equivalence checking process, and its many benefits. You’ll also gain some perspectives into how Synopsys’ unique, machine learning (ML)-powered equivalence checking approach and Synopsys Formality® ECO solution deliver an array of advantages compared to traditional techniques, and some insights into where the future is headed.
What is Equivalence Checking?
A segment of a broader discipline known as formal verification, equivalence checking uses different mathematical modeling techniques to infer if two design representations behave in the same way. It consists of three basic steps: setup, mapping, and comparing.
In the first phase of the process, inputs such as the verified reference design, library elements, and the revised design are weaved in and data structures are created to initiate the next steps. In the mapping phase, different points of the design are mapped and compared, usually using logic cones or blocks of combinational logic that drive compare points on registers, primary output ports, and black-box input pins. Lastly, during the comparison phase, the mapped points are carefully examined to see if they behave in the same way in each design representation or if there are any failures detected, in which case they need to be resolved in the design and rerun through this process.
What is Functional ECO?
Functional ECO is the method of applying logic directly to the gate-level netlist equivalent of the register-transfer logic (RTL) change. This modification is either done to fix an error that was found in the RTL version of the design, optimize the design, or revise the design based on a customer requirement. A post-synthesis version is then patched directly to the design rather than re-implementing the design, avoiding additional cost and time.
Given the varied nature of changes that may be needed, dealing with ECOs can be a time of high stress, long work hours, and uncertainty. ECOs tend to appear only later in the design cycle and typically have a high level of complexity involved — impacting state machines, clock reset paths, etc. EDA tools save time and reduce the scope of cumbersome tasks, such as synthesis, to focus only on portions impacted by the ECO and verify equivalence of the RTL and patched gate-level implementation. Current automated solutions in the industry face several limitations in the journey from ECO RTL ready to ECO done, impacting turnaround time (TAT), multiple handheld iterations, and sacrificing QoR.
How Equivalence Checking Addresses Verification Challenges
Chip designers rely on a gamut of different optimization solutions and techniques to deliver differentiated products and meet PPA goals— from retiming and multibit banking to advanced data-path optimization. These optimizations allow designers to achieve better QoR through a range of benefits, but not without a catch: they also cause hard verifications (when two designs are dissimilar) that ultimately stress the traditional equivalence checking technologies.
Having so many steps in a complex SoC design often leads to variations that affect the chip’s overall behavior. If teams can’t verify their optimizations, they are of limited use. Additionally, many existing equivalence checking products require significant setup time just to get the verification running, with optimizations having to be dialed back to achieve verification success. These challenges, combined with the increasing arithmetic content in today’s high-performance designs, require a comprehensive, nonrepetitive solution—from synthesis to signoff —to meet shortening time-to-market windows.
Fortunately, design teams can achieve the best PPA and out-of-the-box results with Synopsys Formality® equivalency checking. Formality overcomes QoR obstacles by deploying a guided-based verification flow that works closely with Synopsys Design Compiler® and Synopsys Fusion Compiler™ to gain insight on both setup implementation and the type of optimization being performed. With a unique built-in ML-driven adaptive distributed verification approach, teams can achieve fast, accurate, and complete verification with minimal intervention.
Guided Setup
For any signoff solution, not only is it important to completely verify all optimizations for the best QoR, but also evaluate the speed at which a designer can signoff. A guided approach allows users to take full advantage of advanced optimizations from Synopsys Design Compiler, Synopsys Fusion Compiler, and Synopsys IC Compiler™ II while ensuring reliable completion and quick setup.
The process looks like this: the “recipe” of the arithmetic optimization is recorded as “guidance” during the implementation stage (generated by Synopsys Design Compiler or Synopsys Fusion Compiler) for rapid setup of the verification environment and to avoid multiple iterative runs. This information is then read into the Formality solution with the RTL and corresponding netlist. In the next stage, the guidance is independently processed and pre-verified. Lastly, Synopsys Formality applies the guidance to simplify the final verification step. This correct-by-construction information improves performance and first-pass completion by utilizing the most efficient algorithms during matching and verification.
Streamlining Chip Design Signoff with ML-Driven Equivalence Checking
Formality solver technologies have evolved over the years to enable verifications of the most complex, high-performance designs. Synopsys Formality utilizes a collection of solvers in parallel through a distributed processing (DPX) approach, specifically targeted at verifying datapaths, that allows for both faster verifications and resolution of hard verifications. With “smarter” adaptive distributed verification, the solution offers a comprehensive set of alternative strategies that are deployed adaptively rather than separately, allowing teams to achieve up to 5x runtime improvement when running experiments on even their most challenging designs. The unique combination of automatic setup, best-in-class solver technologies, and distributed capability allows Synopsys Formality to achieve the best verifiable QoR in the marketplace.
A New Way of Solving Functional ECO
While equivalence checking is important to catch a wide range of errors introduced during the SoC design process, functional ECOs provide a critical, late-stage optimization step for designs. Because these changes are applied so late in the design cycle, there is less chance for teams to verify and improve these changes timely. Customers routinely need to correct multiple ECOs for numerous designs, making TAT a critical metric for any ECO tool. Today, many existing industry tools give the false perception that a full ECO RTL compile is required to kickstart an automatic ECO process. Synopsys Formality ECO changes this requirement.
By starting the ECO generation process as soon as the ECO RTL is ready, Synopsys Formality ECO offers a fundamentally new methodology of automating functional ECOs and leveraging existing capabilities of Synopsys Design Compiler and Synopsys Fusion Compiler to save valuable time during late-stage ECOs. Utilizing a targeted synthesis technology to focus only on the regions of change between the original RTL and ECO RTL, the solution leverages Formality equivalence checking engines to create tiny patch sizes that are constrained to meet timing requirements — all without compromising QoR of the patch.
As expectations for complete verification and QoR rise, Synopsys’ R&D team continues to experiment with different design characteristics and training models, thus continuously advancing Synopsys Formality equivalence checking and Synopsys Formality ECO capabilities. With Synopsys Formality solutions, teams never need to start afresh and scale down optimizations to sacrifice QoR.
Looking Ahead
Imagine if chip design verification could be done out of the box with no setup iterations and verification restarts. Now imagine a distributed system that can scale to multiple workers and reduce weeks of mundane work hours spent repeating processes every time a change needs to be made.
We are merely at the cusp of uncovering Synopsys Formality’s true potential. Applying predictability and automation to the chip design process without depending on manual intervention has already shown us tremendous success. Shortening the equivalence checking cycle with a learning-based approach and achieving first-time-right ECOs creates an array of advantages for design teams to achieve the best verifiable QoR no matter how complex the design is.
If we can already achieve such possibilities with accurate results, imagine what else ML can unravel in this space once we begin experimenting with customer-specific training data. Stay tuned!