Cadence INCISIVE ENTERPRISE VERIFIER Datasheet - page 3
3
www.cadence.com
INCISIVE ENTERPRISE VERIFIER
simulation, acceleration, and emulation
later in the design cycle, with all the
metrics being combined into a unified
view for a true, total coverage picture.
This effectively leverages the strengths of
all the technologies to further improve
quality.
EXECuTaBlE VERIFICaTIoN PlaN
Incisive Enterprise Verifier incorporates
Desktop Manager, a subset of Incisive
Enterprise Manager, to drive the
verification process right from the
planning stage. When combined with
the guidelines in the planning and
management component of the included
Incisive Verification Kit, your team
can automatically capture verification
objectives from their written verification
plan, create a vPlan executable
specification, and automatically compare
progress against the vPlan. Furthermore,
the combined results from formal
analysis and dynamic simulation can be
automatically backannotated and overlaid
next to each other in the vPlan report to
assure all points of interest have been
covered by at least one class of engine.
aSSERTIoN-dRIVEN SIMulaTIoN
The same assertions used in formal
analysis can be automatically reused by
Incisive Enterprise Verifier to generate
new dynamic simulation stimulus for the
design. You can replay these automatically
generated HDL tests—in effect, a
“synthetic testbench”—to recreate
the assertion or failure behavior using
dynamic, simulation-based ABV.
CoVER PoINT TaRGETING
This capability is a unique application of
Incisive Enterprise Verifier‘s constraint
solver and formal engines in combination
with dynamic simulation. Users can select
a cover point of interest, the formal
engines figure out an optimal way to
reach the selected state, and then Incisive
Enterprise Verifier automatically creates
and drives required stimulus back into
the simulator. This speeds verification
of designs faster than possible with
the traditional application of trivial
directed tests.
GuIdE PoINTING
This capability uses formal analysis to hit
deep states in the design not otherwise
possible. Guide pointing allows you to
specify intermediate states along the
way to a deep state. It’s a classic “divide
and conquer” approach to use your
knowledge to break down the problem.
Incisive Enterprise Verifier then uses
formal analysis to hit these intermediate
states (guide points) specified in
sequence.
In effect, guide points are a sequence of
covers, where the tool proves reachability
to each guide point. As each guide
point is hit, the design is initialized by
simulation to this state to start exploration
to hit the next guide point in the
sequence. Once the final guide point is
hit, Incisive Enterprise Verifier formally
explores all the active assertions present in
the environment.
SEaRCh PoINTING
With search pointing, you can run a
dynamic simulation to a point of interest
and then apply the formal engines to
explore the state space from that point
in time. This process can be repeated to
alternate runs of simulation and formal
analysis. This enables verification of much
larger designs/state spaces than possible
with standalone formal methods.
auToMaTIC FoRMal aNalySIS
Incisive Enterprise Verifier’s automatic
formal analysis capability automatically
extracts from the design common
assertions that can easily be overlooked
or that are just plain tedious to write by
hand. Either way, because the checks are
automatically created, they are generated
consistently across the entire RTL code
base, and the correctness of the assertions
is guaranteed. The bonus here is that
no time will be required to debug these
assertions themselves. Instead, you are
free to focus solely on debugging failures
or incorrect RTL behavior.
Anyone on a design or verification team
can and should run automatic formal
analysis on all designs in the same way
you run code coverage in dynamic
simulations; i.e., just turn it on and let the
machine do the work. It’s a simple and
low-effort verification activity that can
catch bugs “for free.”
lEadING-EdGE FoRMal ENGINES
WITh SMaRT auToMaTIoN
A combination of complementary,
state-of-the-art formal engines from
production-proven technologies and
world-renowned researchers deliver
the industry’s highest performance and
capacity. To optimize formal analysis
performance even further, built-in
Figure 3: The Desktop Manager can create an executable vPlan from your written specification; this plan
drives all of your formal and dynamic simulations, with the coverage results from multiple runs automatically
backannotated into the vPlan for a “total coverage” view