Automated RTL verification gains 10X speed and 5X capacity increases
Ascent AutoFormal’s early functional RTL verification identifies RTL design bugs using formal sequential design analysis. AutoFormal finds RTL bugs early in the design flow, before test benches are available, making debug easier, and eliminating lengthy, costly chip-level simulation cycles.
AutoFormal automatically generates functional assertions based on implied design intent, eliminating the need for designers to learn an assertion language and manually create potentially 1000s of assertions. Examples are FSM deadlocks, and coverage issues such as code reachability, constant nets, and constant assignments. The new engines automatically split runs across parallel cores, they also dynamically determine whether or not the analysis is converging for a particular check and move on to a new check when necessary. Prior to running a formal analysis, the tool automatically provides detailed RTL design information that can impact it. This ensures that relevant design elements are accurately analyzed in the first formal run, reducing RTL verification iterations. For example, in addition to clocks and resets, the tool recognizes FSMs, and also identifies elements such as latches that could prevent the detection of the FSMs.
Additionally, the tool’s hierarchical root-cause analysis minimizes debug by uncovering the root cause of bugs deep in a design. Ascent AutoFormal determines and separately classifies: root-cause errors; secondary violations due to propagation of a root-cause error; duplicate errors from multiple instances; and structural violations that can be found by an RTL linter such as Ascent Lint.
The new AutoFormal release is commercially available immediately and can be used standalone or with an RTL linter.
Real Intent – www.realintent.com
If you enjoyed this article, you will like the following ones: don't miss them by subscribing to :
