Skip to content
3 Ways Two-Phase Linting — RTL & Automatic Formal — Cuts RTL Verification Time
By Lisa Piper, Technical Marketing Director, Real Intent
I. Introduction: RTL Verification — Linting Challenges
RTL Linters are designed to catch bugs in a design using static methods, enabling designers to catch issues early — prior to simulation — and ensure high quality RTL. Linting is the most cost-effective RTL verification technology per bug fix. From a technology perspective, there are two distinct types:
- RTL (Structural) Linting Static Sign-Off uses search and analysis to find all targeted failures early. RTL Linting enforces a broad range of coding guidelines, prevents synthesis issues and functional bugs, and enforces coding styles for readability and re-use.
- Formal Linting (Automatic) uses formal technologies to detect bugs associated with sequential control logic, such as FSM deadlocks, dead code, and range violations – including finding corner case functional bugs. It also automates the error prone and time-consuming process of writing assertions.
Two phases of linting
Design teams today typically use an RTL verification flow that utilizes RTL static sign-off (structural linting), followed by simulation to verify sequential logic. However, as companies face competitive challenges to design and verify new products even faster and more efficiently, traditional RTL linting flows must evolve to meet these challenges:
- Structural RTL Linting, although very fast, does not detect sequential control logic bugs, and simulation cannot guarantee full coverage.
- Sequential logic can cause a ripple of secondary effects, making debug unwieldy.
Structural and formal linting are complementary. Together they provide a complete linting solution, enabling both the elimination of critical control bugs and making the design more readable and portable.
II. 3 Ways RTL + Automatic Formal Linting Address RTL Verification Challenges
1. Two-Phase Linting Catches More RTL Verification Issues Early
RTL linting (structural) is widely adopted because it is very fast, has clear value, and is easy to use.
Even so, RTL linting does not address control logic issues that require sequential analysis. Additionally, trying to get coverage closure for control logic using simulation is a lengthy and challenging process for complex design. It is also difficult to know if coverage closure is ever reached.
Formal technology has the necessary sequential analysis to find all control logic issues. However, using traditional formal tools requires deep expertise and extensive manual effort to write complex assertions. Thus, it is generally relegated to a formal verification expert.
There is an opportunity for the designers to use automated formal linting during their design process to leverage “exhaustive coverage of formal” with minimal time investment – and no manual writing of assertions.
- Formal linting detects corner-case functional issues early, identifying coverage issues that can be missed in simulation and cannot be detected with structural linting.
- Formal linting has high value control and coverage checks, including FSM deadlocks, unreachable state checks, bus contention, floating bus, range violation, constant net, dead code, and toggle tests, etc.
A two-phase process — RTL Linting + Formal Linting — improves design quality early, before simulation, greatly reducing simulation time and effort by minimizing iterations.
2. Automatic Formal Linting — Breaking Capacity/Performance Barriers
With formal analysis, capacity, performance, and quality of results (QoR) are tightly linked. High capacity and performance are critical to running formal linting during design.
Control logic typically crosses multiple blocks. The RTL’s controlling logic provides the actual constraints so that only legal scenarios are tested, and the results are precise. E.g., when testing when an array can be accessed beyond its range, formal analysis verifies that the driving logic constrains the index to values within the range.
This can only be achieved with sufficient capacity. Otherwise, designers must manually write assertions to properly constrain the block-level inputs – something that is time-consuming and error-prone.
Unfortunately, traditional formal tools are limited to a maximum capacity of a million gates; they are slower to produce results. This combination has made them impractical for designers to use as part of RTL verification during design.
The most advanced automated formal linting tools have now broken the multi-million gate capacity barrier, with 10-20 times the speed of traditional tools.
- The capacity and speed improvements are achieved by tuning the engines exclusively for formal linting, rather than relying on general assertion-based RTL verification engines.
- The performance is further accelerated with parallel processing capabilities.
The higher capacity and performance of advanced automated formal linting technologies make it feasible for designers to catch control logic bugs during design, reducing total RTL verification time.
3. Formal Linting Root Cause Analysis — Cuts Debug Time by Over Half
Formal linting debug can be challenging due to the sequential analysis across hierarchies. One aspect of sequential logic is that a single issue can cause a ripple of secondary effects that will go away when the root cause is fixed. This is because a functional issue at time “x” can cause the logic to traverse different paths that result in secondary violations at time “x + delta”.
The most advanced formal linting tools can now provide root cause analysis that distinguishes root cause (primary) errors from secondary violations. Additionally, duplicate errors that occur from multiple instantiations of faulty logic are suppressed. They also separate out structural violations that are easily caught by RTL linting.
Root cause analysis enables designers to focus on the debug of the primary failures — cutting the overall debug time by more than half.
Formal linting tools also provide waveforms to show the shortest sequence that causes the violation, and a finite state machine (FSM) viewer that facilitates debug of FSM issues. Source browser and violation details further help debug.
The time it takes to resolve debug greatly impacts the total turn-around time, so highlighting the bugs to fix and providing debug tools will cut the RTL verification debug time in half.
III. Conclusion: 2-Phase Linting — RTL & Formal — Key to “Shift Left”
RTL structural linting and formal linting complement one another to provide a complete two-phase RTL linting sign-off solution. Together they detect both logical and sequential functional bugs prior to simulation, reducing overall RTL verification time and effort.
Two-phase linting is part of the industry move to ‘shift left’ to find bugs earlier in the flow. Catching errors before simulation time reduces iterations because you start with a higher quality RTL – the low-level functional issues are already fixed, the code is more readable, more synthesizable, and compatible with downstream tools.
Bug fix costs increase 10X at each stage
And now, recent breakthroughs in capacity/performance have made it feasible for designers to use formal linting to also catch sequential control logic bugs during design. Furthermore, root cause analysis, VCD waveforms, and FSM views have dramatically reduced the debug time of complex sequential issues.