|
| Early RTL
Verification with JasperGold® Formal Verification |
| Formal Verification
Unleashed! |
| |
Overview
Formal verification with JasperGold® Verification
System is a powerful tool for RTL designers as well as
for verification engineers. JasperGold System allows RTL
designers to verify early, when it counts, and to explore
the behavior of internal and commercial IP blocks they
are incorporating. Finding a bug early in initial RTL
design instead of later in the verification stage can
shave significant time off the overall project schedule.
Not only is the repair cost less than later in the flow,
but there are no futher design dependencies added on top
of the bug to complicate the fix. Formal verification
is possible at the earliest stages of the design flow
because it does not depend upon costly testbench development
to run. Formal verification has the most exhaustive coverage
of any verification method, making it ideal for early
bug detection and removal. JasperGold formal verification
has numerous features to make formal easy for RTL designers
who don't have time to learn complicated tools or languages.
This enables powerful formal technology to be applied
by designers early in the verification flow for maximum
benefit. |
| |
Early RTL Development and Testing
JasperGold Express Verification System delivers a powerful,
exhaustive formal verification solution to users already
familiar with simulation-based ABV. Simulation ABV properties
are used to identify potential failures in the design
without costly testbench development. Jasper's unique
formal debugging environment automatically isolates the
root cause of bugs down to the individual line of code
and automatically generates waveforms as it detects bugs.
This intuitive, integrated environment greatly reduces
overall debug time. |
| |
| Running JasperGold formal early
bypasses the need for testbench development
while providing multiple benefits to the designer,
including comparing multiple implementations
of a design, coming up to speed quickly on
inherited blocks, and ensuring basic functional
correctness prior to verification handoff.
JasperGold formal verification requires no
testbench and minimal assertion coding when
used for these applications. All data exploration
is controlled through manipulation of simple
waveforms, as shown in Figure 1. At each stage
in the verification process, designers simply
freeze the desirable behavior in the waveform
and highlight the signals they want to see
changed. JasperGold Verification System generates
new waveforms based upon these instructions.
By running multiple combinations of behaviors
interactively, designers can much more quickly
perform basic sanity checks on their blocks
and effectively eliminate the ramp-up time
required to build and debug a throw-away simulation
framework. |
Debug Closure
|
 |
Figure
1 - JasperGold Formal Verification's Interactive
Waveform Debugging Envirnoment |
| |
|
|
Because the user is simply
manipulating waveforms, the only knowledge required for
debugging is the intended design behavior. As further
design constraints or functionality are explored, JasperGold
Verification System develops new scenarios that show the
behavior possible in the design. The designer can quickly
run through the list of constraints from within the waveform
viewer and identify if the set is valid behavior for the
design. If there is a problem, the designer has identified
a failure and can debug it in the very same environment
as the initial detection. Saving steps in the interactive
session makes replaying the tests on the fixed code quick
and easy, saving time and effort up front.
Identifying constraints early in the coding process further
reduces verification and development time by leveraging
them later when full verification begins. Design constraint
reuse captures the designer's intention for use downstream
in verification, saving effort. There is no need to completely
abandon the verification environment constructed for early
block debug, as there is with simulation, greatly simplifying
downstream debug efforts. Block-level constraints can
also increase the capacity of downstream formal verification,
so higher level proofs complete with less user input.
So, time saved early on in finding bugs has the potential
to multiply that savings across the entire verification
flow!
Designers commonly recognize new valid, but undocumented
behavior for the design while running JasperGold formal
verification in the early design stage. JasperGold Verification
System can export waveforms of these behaviors for documentation
purposes, further reducing the designer's efforts. This
improves communication between different groups in the
design flow and documents further directed testing requirements
in the design. |
|
| Summary |
JasperGold Verification
System removes the overhead of testbench generation and
stimulus development from early RTL design and test. For
designers using proprietary or commercial IP, JasperGold
System provides the capability of exploring and verifying
inherited RTL quickly and easily with an executable specification.
Designers can concentrate on the intended behavior of
the design as opposed to spending time determining failure
scenarios for simulation directed testing.
JasperGold Verification System's interactive analysis
and constraint environment requires no formal knowledge,
and quickly explores many scenarios to ensure basic design
functionality prior to verification handoff. Waveform
results are easily captured for documentation and communication
purposes. Most importantly, designers have higher confidence
in the RTL code's actual behavior prior to verification
handoff without the overhead of generating a "throw
away" simulation environment. Rather, the constraints
created during initial debug can be leveraged later in
the flow to provide additional information to the verification
tools. In the end, today's designers can now spend more
time designing and less time writing verification environments,
while simultaneously improving the quality of the code
provided to the verification team. |
|
| Click
here to download the PDF |
|
|
