Automatic RTL Verification – Ascent AutoFormal2018-12-28T23:55:11+00:00

Ascent AutoFormal – Automatic RTL Verification

White Paper: Bulletproofing FSM Verification

Automatic RTL Verification

Ascent AutoFormal is a state-of-the-art automatic RTL verification tool. It finds bugs using an intelligent hierarchical analysis of design intent. Since no testbench is needed, it is an easy and efficient method to find RTL bugs earlier in the design flow before they become more expensive to uncover. The analysis distinguishes the root cause for issues, and minimizes iterations and debug time.

When the tool is launched, Ascent AutoFormal performs a comprehensive analysis of each of the design elements in the RTL code to generate functional assertions. These assertions are then analyzed by an array of engines to provide quick and exhaustive verification of a design’s functional behavior.

High Capacity & Accuracy

Ascent AutoFormal has the speed and capacity to handle design blocks exceeding 1M gates and provides a wide variety of complex checks including FSM deadlocks, coverage checks, synthesis directive checks, bus issues and X-value propagation. If SystemVerilog Assertions (SVA) are available, Ascent AutoFormal can use these as constraints to improve the accuracy of the analysis.

Automatic Intent Checks

  • FSM deadlocks and unreachable states, transition checks
  • Bus contention and floating busses
  • Full- and Parallel-case pragma violations
  • X-value propagation
  • Array bounds
  • Constant RTL expressions, nets & state vector bits
  • Dead code
  • SystemVerilog unique, unique0, and priority checks for if and case constructs

Integrated Debug Environment

Debug with AutoFormal is easy with links to the integrated source browser, a VCD that shows the sequence of events that leads to the failure, and a causation tree that identifies the dependencies of failures.

Ascent AutoFormal comes with iDebug, the powerful integrated graphical interface for database driven debug. Source links are provided to iVision, a tightly integrated source browser. Automatic VCD traces show the sequence of events that lead to an undesired condition and shows the time of failure. In addition to facilitating debug, iDebug also tracks status and user provided comments.Ascent AutoFormal supports the Verilog, VHDL, and System Verilog languages and provides early functional verification that automatically uncovers deep and fundamental bugs in RTL code.

Click to enlarge

Smart Reporting with Specialized Categories

The intelligent hierarchical analysis in Ascent AutoFormal uncovers the root cause of bugs deep in the design that propagate to higher levels, and that could be missed in simulation. It conveniently resumes from a previous verification run for an efficient extension of the analysis. This saves valuable analysis time by avoiding unnecessary iterations.

Ascent AutoFormal is unique for its smart reporting that distinguishes real issues from structural warnings, secondary errors and duplicate errors. For easier debug review, specialized report categories are available for coverage, FSMs, language checks, and design checks.


  • Exhaustive analysis quickly finds functional errors in early RTL
  • Minimal effort required for fast results
  • Targeted re-invoke enables running a subset of checks to verify RTL fixes
  • Smart reporting provides low noise results by distinguishing the root cause issues
  • Status tracking
  • Debug starts earlier before simulation testing
  • Early block level verification eliminates costly and lengthy chip-level simulation cycles