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:
- Extracts checks based on implied intent of the RTL
- Automatically sets up design environment factors, such as clocks, reset & configuration constants
- Runs formal analysis to detect violations, utilizing multiple engines to find sequential bugs quickly
- Determines root cause errors