3 Ways Two-Phase Linting — RTL & Automatic Formal — Cuts RTL Verification Time

By Lisa Piper, Technical Marketing Director, Real Intent

Ascent AutoFormal – Automatic Formal Linting

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.

RTL Verification - Structural + Formal Linting

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.

Download White Paper PDF

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.

RTL Verification - RTL + Formal Linting

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.