Ascent IIV AutoFormal

Ascent IIV AutoFormal
Automatic RTL Verification
Ascent IIV 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 IIV 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.Ascent IIV AutoFormal has the speed and capacity to handle design blocks exceeding 100K gates and provides a wide variety of complex checks including FSM deadlocks, bus issues and X-value propagation. If SystemVerilog Assertions (SVA) or VHDL Property Specification Language (PSL) is available, Ascent IIV AutoFormal can use these as constraints to improve the accuracy of the analysis.
Automatic Intent Checks

  • FSM deadlocks and unreachable states
  • 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

The intelligent hierarchical analysis in Ascent IIV 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 IIV 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, design checks, and X-verification. Ascent IIV AutoFormal comes with a powerful integrated graphical interface. Automatic VCD traces show the sequence of events that lead to an undesired condition and shows the time of failure.

Ascent IIV AutoFormal supports the Verilog, VHDL, and System Verilog languages and provides early functional verification that automatically uncovers deep and fundamental bugs in RTL code.


  • Exhaustive analysis quickly finds functional errors in early RTL
  • Minimal effort required for fast results
  • Smart reporting provides low noise results by distinguishing the root cause issues
  • Debug starts earlier before simulation testing
  • Early block level verification eliminates costly and lengthy chip-level simulation cycles