Using formal techniques to help tackle SoC verification challenges
Formal techniques can be applied to various parts of the verification challenge, including low-power and clock domain-crossing issues
Today’s complex SoCs present enormous verification challenges. Today’s leading designs routinely exceed hundreds of millions of logic gates. Meanwhile, advanced low-power design techniques, such as frequency and voltage scaling, and sophisticated power-management techniques, mean that all those gates must be verified in numerous operating modes and states.
This problem cannot be solved by running more simulation cycles alone. Verification teams are now applying a divide-and-conquer approach, using static and formal verification techniques to address specific issues within a design, reducing the amount of logic that remains to be tackled with logic simulation. These techniques can help to find bugs earlier in the design cycle. They’re also useful for discovering hard-to-find corner case scenarios, since they are less reliant upon the user to define the complex scenarios necessary to trigger such bugs.
In formal verification, the user defines certain properties of a design using an assertion language, and then relies on formal verification tools’ powerful proof engines to conclusively show that these properties hold true, are proven false, or are irrelevant.
Formal tools currently address verification tasks such as:
- Identifying RTL issues such as functional correctness and completeness before a simulation test environment is available
- Checking that the logic of a design expressed in two different ways, for example at two different levels of abstraction, or as the result of two different synthesis strategies, is equivalent
- The correctness of interconnection schemes
- Whether designs are logically equivalent before and after power-management circuitry is introduced
- The consistency of clocking schemes that cross between power-management domains
By using formal verification at key points in the verification process, challenging design bugs can be caught earlier, resulting in a higher quality design, schedule improvements and greater predictability of the verification process.
The Synopsys approach
Synopsys has introduced a set of static and formal tools, as part of its Verification Compiler suite, each of which are targeted at a different aspect of design verification. Given that verification is such a large part of the overall design flow now, it makes sense for Synopsys to leverage its existing design and verification infrastructure, as well as ensuring as much commonality as possible among the tools, to make them easy to use for non-specialist verification engineers.
Figure 1 Synopsys’ VC Static and Formal tools are built on a common next-generation technology platform (Source: Synopsys)
The key elements in Synopsys’ VC Static and Formal tools include greater performance and capacity than previous offerings; common databases and engines; shared analysis, debug and reporting capabilities; and strong commonality with Design Compiler, PrimeTime and VCS through common hardware inference, language support and TCL scripting strategies.
Formal methods in use
VC Formal is the product name of the formal technologies in the Synopsys VC Static and Formal technologies suite.
Figure 2 VC Formal (Source: Synopsys)
VC Formal supports a number of verification strategies:
- Assertion-based verification – a formal proof-based technique to verify SVA/PSL (assertion language) properties or assertions, to ensure correct operation.
- Connectivity checking, to verify interconnect schemes at the full-chip level. A flexible input format ensures ease of flow integration. Powerful debugging, including value annotation, schematic viewing, source-code browsing and analysis reporting, speeds analysis. Automatic root-cause analysis of disconnected net checks saves debug time.
Figure 3 Connectivity checking in VC Formal (Source: Synopsys)
- Sequential equivalency checking, to compare blocks or designs that have previously been too disparate for typical formal comparison. This allows comparison of designs, even after insertion of power gating, or synthesis retiming.
- Formal scoreboard, to verify the data integrity of datapath designs. This ensures that data is transported through a design without being lost, re-ordered, corrupted or duplicated.
- Certitude integration, to provide property-coverage measurements within the formal environment. This integration can also identify weaknesses in the formal environment, such as missing or incorrect properties or constraints.
Figure 4 Integration with Synopsys’ Certitude functional qualification system (Source: Synopsys)
- Advanced debug interface, built on standard RTL and waveform visualization solutions, including schematic value annotation for connectivity checking.
- Interactivity – on-the-fly assertion and constraint editing, incremental build and solve, and proof progress feedback allows instant understanding and control of VC Formal’s activities – without the need to restart.
VC Formal Coverage Analyzer
Who tests the testers? Put another way, how can you know whether your verification strategy is covering enough of a design’s logic and operating modes to root out the difficult bugs that you are hoping it will catch?
Coverage metrics provide a way to measure the correctness and completeness of a simulation test environment. Any areas of the design with poor code coverage results will not be tested by the testbench. The question is whether this matters: if the poorly covered logic is only present for use in extreme error cases, it still needs to be verified to ensure correct operation in that case. But if the code is ‘dead’, for example representing an unused function, it is unreachable and therefore can be legitimately left uncovered.
The problem for verification engineers is to identify the blocks for which poor code coverage matters. The problem is exacerbated by code reuse, which tends to increase the unreachable code that could be excluded.
VC Formal Coverage Analyzer uses formal techniques to determine which structural coverage metrics are attainable, and to automatically exclude metrics which cannot be reached.
Figure 5 The code coverage challenge (Source: Synopsys)
The Coverage Analyzer integrates with the simulation engine and coverage reporting and debug solutions, helping verification teams focus on critical aspects of chip operation that are currently unreachable and so need further testing. It also does the opposite, showing that designers can safely ignore aspects of the design that it can prove are unreachable.
Among the key features of VC Formal Coverage Analyzer are:
- Structural coverage analysis, providing automatic extraction and application of formal unreachability analysis to line, condition, toggle and FSM state-transition coverage goals.
- Automatic exclusion and coverage metric adjustment, generating an exclusion file containing all unreachable coverage goals for review that can imported into VCS and Verdi to automatically adjust final coverage metric reporting.
This tool checks the integrity of clock signals as they move across the multiple clock domains used in advanced SoCs.
Clock domain crossing (CDC) verification for large SoC designs at the flat full-chip level is challenging. Previously, users were forced to adopt hierarchical or block-based methodologies, which risk missing inter-block, design-level CDC bugs.
It can also be challenging to ensure consistency between a CDC verification strategy and a design implementation flow, which creates opportunities for bugs to be missed. Bugs can also be missed if the CDC verification strategy is not tuned to the design style used on a chip or a block, since this can mean that an excessive number of violations are reported, making it more difficult to spot the real bugs.
Any tool attempting CDC verification needs to understand the way that low-power implementation strategies infer and synthesize additional logic, which can introduce CDC bugs.
Synopsys’ VC CDC tool has a number of relevant features:
- It uses Synopsys Design Constraints set-up to access the list of clocks, asynchronous clock groups, constants in design (like scan mode), boundary (input/ output) port clock relationships and the like. This information is automatically extracted from the SDC file.
- It can reuse Design Compiler scripts for VC CDC design read and design query.
- It automatically recognizes and identifies synchronizer types and variants, such as multi flip-flop, data mux, logic-based, clock gating, handshake and FIFO, and adapts this recognition based on design style.
- It eliminates false accepts and false detects as part of CDC verification, under the control of a synchronizer-detection configuration approach based on design style and methodology.
- Has root cause analysis help and visual debug.
- Works with VC LP, Synopsys’ low-power static checking engine, to predict the impact of the introduction of low-power implementation structures after synthesis.
- Handles reset verification, checking for synchronous de-assertion of reset, cascaded synchronizers and reset convergence.
- Offers reporting filters and waivers.
The introduction of multiple, aggressively-managed power domains, and techniques such as power gating, retention, low-Vdd standby, and dynamic voltage scaling, is making the verification of low-power SoCs exponentially more challenging than for designs that are simply On or Off. The introduction of multiple operation modes adds another dimension of complexity.
Such designs have to be verified in all their power domains, at all combinations of supply voltages, and all power states and modes, as well as for all the specified transitions into and out of the various operating modes.
Low-power design techniques add new design elements at various stages of the design flow. Architectural design bugs that violate the principles of low-power design may exist even at RTL. Isolation cells are typically synthesized automatically. Retention-register connections must be validated after synthesis and again after place and route. Multi-voltage designs require the appropriate power and ground pins to be connected to the specified supply rails.
VC LP is a multi-voltage, low-power static rule checker that can help check low-power design intent expressed in the IEEE 1801 Unified Power Format (UPF). It can also validate that UPF design intent has been implemented as expected, and works correctly.
The tool includes:
- Power intent consistency checks, using syntax and semantic checks to validate the consistency of UPF before implementation.
- Architectural checks at RTL for signals violating power architecture rules.
- Structural and power and ground checks, to validate the insertion and connection of isolation cells, power switches, level shifters, retention registers and always-on cells throughout the implementation flow.
- Functional checks on isolation cells and power switches.
- Hierarchical power-state analysis, with automatic derivation of a hierarchical power-state table that defines all the power states, transitions and sequences.
- Complex power-state table debug.
VC LP is integrated with VC CDC and VC Formal, so that users only need to load a design once for any or all of the three products.
Static and formal verification techniques are an increasingly important part of verifying complex, and especially low-power, SoCs. Static techniques enable design teams to quickly and directly verify design intent very early in the design cycle, and also to verify that specifications are met before design handoffs. Formal techniques can tackle focused tasks, such as checking the way a chip’s blocks are interconnected, effectively providing a more certain context for other verification efforts – as well as reducing the overall amount of logic that can only be checked through simulation.
Find out more about Synopsys’s suite of formal verification tools within Verification Compiler here:
David Hsu is a director of product marketing in the Verification Group at Synopsys, and is responsible for the marketing of Synopsys’ low power, static and formal verification solutions. He has over 25 years of experience in design and test automation R&D, business development and product marketing. Prior to Synopsys, Hsu worked at FormFactor, Compass Design Automation, and VLSI Technology. Hsu holds an MSCS degree from Stanford, a BSCS degree from MIT, and an MBA from Santa Clara University.