Ascent AutoFormal – Automatic Formal Linting

Automatic Formal Linting Reduces Simulation Effort

Ascent AutoFormal, a multimillion gate capacity formal linting tool, identifies RTL design bugs using formal sequential analysis, expanding on Ascent Lint‘s syntax, semantic, and style checks. AutoFormal formal linting tool is complementary to other forms of design specification verification, including simulation.

The tool provides early functional verification to automatically uncover deep, fundamental bugs in RTL code. It finds RTL bugs early in the design flow, before your test benches are available, getting your RTL code ready for simulation.

This early expanded functional verification makes your debug easier, eliminating lengthy, costly chip-level simulation cycles. Debugging with AutoFormal is easy, with links to the integrated source browser, VCD viewer, the schematic viewer, and the FSM viewer.

Minimal effort is required for fast, accurate results. Ascent AutoFormal executes the following steps:

  1. Extracts checks based on implied intent of the RTL
  2. Automatically sets up design environment factors, such as clocks, reset & configuration constants
  3. Runs formal analysis to detect violations, utilizing multiple engines to find sequential bugs quickly
  4. Determines root cause errors

Formal Linting - Ascent AutoFormal

2-Step Early Functional Verification with Ascent Lint & Ascent AutoFormal

What is Formal Linting?

Formal linting uses formal verification technologies to automatically check for functional bugs associated with sequential control logic, including FSM deadlocks, coverage checks, & range violations. Formal linting generally occurs before simulation, reducing debug effort by finding elusive control logic errors early.

Multi-Million Gate Capacity & 10X+ Performance Speedup

Our new array of engines can deliver more than a 10X performance speedup over prior versions. We’ve introduced faster engines, plus we now support the automatic splitting of runs across parallel cores, for a 2-4x speedup with a nominal 8 cores.

Ascent AutoFormal now has the speed and capacity to easily handle design blocks with millions of gates.

Single core sequential
5-10x speedup

8 parallel CPU cores
2-4x speedup

To maximize bug hunting, the best engine is automatically applied based on the type of check being performed.

Benchmark: A 7M gate design completed in only 11 hours.

The new engines dynamically determine whether or not the analysis is converging for a particular check, moving on to a new check when necessary.  The result is an extremely high completion rate.

Benchmark: A 3M gate design completed 4 hours, that previously ran 96 hours and did not finish.

The completed checks give you full confidence that any bug associated with a particular check has been identified, reducing your follow-on simulation effort.

Additionally, the tool will resume analysis after a prior verification run, efficiently extending the original analysis, saving valuable analysis time and avoiding unnecessary iterations.

Root Cause Analysis Minimizes Debug

The hierarchical formal linting analysis in Ascent AutoFormal uncovers the root cause of bugs deep in the design.  These bugs often propagate to higher levels — and can be missed in simulation.

Ascent AutoFormal’s algorithms determine and distinguish:

  • Root Cause errors
  • Secondary violations due to the propagation of the root cause errors
  • Duplicate errors from multiple instances
  • Structural violations that can be caught by a linter & do not require sequential analysis

The separate classifications better focus your debug effort.

Violation Causation Tree shows Root Cause Extended Impact

One simple typo in the RTL code can propagate to cause a ripple effect of errors. In a simulation, you would observe incorrect functionality at the outputs; it could then potentially take you multiple iterations to trace back to figure out the root cause.

AutoFormal’s violation causation tree clearly identifies the root cause errors and their descendants, saving you debug time.

The example shown is of a block enable root cause and its descendants.  The block could not be entered because the conditional expression could not be true.

Thus the assignments in that block would never happen, causing dead code and constant nets. The constant nets in turn resulted in assignments not being about to take both a 1’b0 and 1’b1 value, which in turn caused other conditional blocks to not be able to be entered.