When we spend hours, days, or even weeks putting our hearts and minds into creating something, we have a tendency to emphasize its strengths and minimize its weaknesses. This is why verification engineers have a blind spot for their own verification platforms. This blind spot, or bias, often leads to overlooking those areas where bugs may lurk, only to emerge at the worst possible time when errors are most costly and take longer to fix. Compounding the problem is that these “late bugs” become progressively more expensive to detect, fix, and revalidate as the design under test (DUT) grows in complexity and the project nears completion.
Every verification engineer has learned this lesson one way or another. Every verification engineer eventually comes to realize that they need an easy way to overcome that bias and uncover those hidden or unforeseen bugs.
An increasingly popular approach has been to employ a comprehensive, constrained-random, coverage-driven testbench development flow, such as the Universal Verification Methodology (UVM). Indeed, when random stimulus generation is well executed it often finds bugs “that no one thought of.” However, this method’s success is limited to smaller DUTs as it is essentially impossible to do an exhaustive analysis of large, complex DUTs within a realistic project schedule. You simply can’t write enough constrained-random tests to cover everything, leaving numerous state spaces and control logic combinations unverified and opening up the possibility of corner-case bugs escaping and Trojan paths going undetected.
In contrast, formal verification tools develop a mathematical model of a given DUT, enabling formal analysis to exhaustively verify all inputs and outputs against the expected behaviors of all the states in a DUT, for all time. Until recently, such analysis could be done only on very small DUTs, but advances in formal algorithms and their corresponding “engine” implementations make it possible to verify millions of gates of logic, including, in some cases, whole systems. The result is that formal-based RTL analysis effectively provides an exhaustive, unbiased “audit” of any DUT. It finds corner case bugs or defunct code that can be missed by other, non-exhaustive verification methods.
A MULTI-TOOL FOR FORMAL ANALYSIS
The problem with formal is that it can be hard to do. That’s why we developed the formal verification apps for the most common verification tasks; including clock-domain crossing (CDC), reset domain crossing (RDC), X-state propagation, finite state machine (FSM) traversal, and dead code analysis. Because the formal apps automate these analysis tasks, you don’t have to know how to write assertions or understand how formal analysis works under-the-hood. Each of these automated tasks are integrated into a holistic, formal analysis workflow that allows you to use what you need when you need it, just like a Swiss Army Knife®.
Analysis results are presented as familiar, easy-to-understand waveforms, annotated state diagrams, and straightforward text log files that can be read by both human and machine. The best part is that this automation can be run before a testbench exists — only the DUT RTL is needed, truly enabling a “shift left” in the verification schedule.
To give an idea of the utility of this approach, let’s briefly look at some common verification challenges and how specific Questa® Formal Apps handle them.
Non-deterministic cycle delays at the receiving side of an asynchronous clock-domain can cause random hardware failure.
The Formal CDC App ensures proper structural protection at all critical asynchronous boundary crossings. Formal CDC-FX enables metastability injection during asynchronous boundary crossing events in functional simulation runs, and Formal RDC detects CDC issues in the reset network.
X-state propagation can cause random hardware failure.
The Formal X-Check App identifies all sources of X and determines the possibility that they can propagate to critical control points and output ports.
RTL structural problems causing functional test failures.
The Formal AutoCheck App checks the design for synthesizability, undriven logic, unconnected ports, uninitialized registers, clocks used as data, latches inferred, combinational logic loops, resets used on both polarities.
Essential RTL functionality issues hindering simulation bring-up.
The Formal AutoCheck App checks for finite state machines (FSM) with unreachable states and missing arcs, unreachable blocks of code, multiple drivers on logic, array entries that cannot be indexed, and indexes beyond the array size.
To speed up the RTL code coverage closure phase.
The Formal Cover Check App exhaustively confirms unreachable code coverage items, allowing users to identify such items as either waiver items or RTL bugs.
A logic fix or RTL change creates new bugs.
The Formal SLEC App (for sequential logic equivalence checking) exhaustively ensures that functionalities that should be the same or different are as expected.
AMBA bus protocols may not be stressed enough.
The Formal AMBA QFL App ensures AMBA protocol compliance.
Thorough testing of a secure data path is very difficult.
The Formal Secure Check App ensures the confidentiality and integrity of secure data.
Integration of IPs and blocks takes up unnecessary team resources.
The Formal Connect Check App ensures the connectivity spec is followed, without requiring any simulation tests.
Control status registers access policies are very difficult to test adequately.
The Formal Register Check App ensures that critical control registers are read and written according to policy specs.
APPLYING THE AUTOMATED FORMAL SOLUTION
Here are three snapshots of how these formal-based methodologies were successfully applied by customer verification teams using Questa® Formal Apps.
1. A customer’s FPGA design and verification process consisted of code reviews, constrained-random verification, and lab verification. All of their RTL and gate-level timing simulations were passing, but when they got their design into the lab, the DUT’s behavior was unstable. They urgently needed to find the root cause of the issues. They ran formal-based CDC analysis on the DUT using the Formal CDC App. The app immediately uncovered what's illustrated in the figures below.
Figure 1-Combinatorial logic before their synchronizers
Figure 2-Asynchronously asserted reset, synchronously de-asserted
Figure 3-Synchronous de-asserts, and several missing synchronizers
As illustrated in figures 1, 2, and 3, their prior design review and verification methods had failed to prevent and find these issues, so they adopted Formal CDC verification as their Plan of Record.
2. A second customer had an intermittent bug occurring in an existing, safety-critical design: the triple-mode redundancy (TMR) logic was not always “voting” correctly. It took them four months to find the bug using a combination of updated simulations and hardware debugging. This was seen as taking too long so the team explored whether an inexperienced user could use formal property checking to find the issue in less time. Indeed, using automated, formal-based design analysis and property checking tools, two properties were created and the issue was uncovered in 16 hours.
3. Similar to the first customer, everything was running well for a third customer until their DUT was realized in the lab. They were effectively running CDC analysis already, so CDC bugs were probably not present. They had used the simulator’s “x prop” option and thought they were safe. However, they found that RTL simulation does not actually propogate X.
For example, considering the figure below, what is the correct value of reg_a?
Figure 4-Determining the correct value of reg_a
To solve this problem, they used a formal-based, automated app that’s focused on searching for “X optimism” in logic. Specifically, the Formal X-Check App searches for all X corruption in the DUT, where X sources are typically from primary/secondary sources (i.e., unresolved registers). The engineers were initially skeptical this would work, but the app quickly found unresolved Xs deep in the design. Thus, they were able to find bugs using a formal-based solution that they would not have been able to find otherwise.
Formal apps provide a multiple set of tools that are uniquely useful for formal verification experts and novices alike. Novices don’t have to know how formal’s complex mathematical algorithms work, nor do they need to write properties. Experts gain an easier, more automated way to invoke the powerful operations they’ve come to trust. In both cases, the formal apps workflow eliminates the human bias inherent in human-made verification platforms, resulting in an automated, unbiased “auditor” of the many facets of RTL quality. In addition, this unbiased auditor helps teams proactively “shift left” in the verification schedule.
The Questa® Formal Apps workflow may just be the greatest invention since the Swiss Army Knife®.
Back to Top