Jasper Design Automation is a privately-held
Electronic Design Automation (EDA) company with a mission
of making full formal IC verification a competitive advantage
for its customers. Jasper formal technology delivers compelling
benefits across the design cycle, from RTL design, through
verification and regression testing, to post-silicon debug.
The company’s flagship product, JasperGold®
Verification System, is unique in delivering verification
coverage within predictable, finite schedule constraints.
JasperGold formally verifies that complex IC design blocks
meet high-level specifications, for all usage modes, without
any testbench development. JasperGold includes an integrated,
intuitive debugging environment. By isolating bugs earlier
than simulation or formal-assisted simulation tools, and
then proving the absence of bugs, JasperGold trims crucial
months off design schedules.
The Problem: Conventional Simulation Approaches
Aren't Enough
Simulation-based chip verification, by its very nature,
cannot guarantee 100% actual coverage of the input space
or certainty of functional correctness. Despite the
advances in testbench automation and coverage tools,
simulation is still a slow, manpower-intensive process.
Design teams can never do enough traditional simulation-based
verification to ensure first time functional success.With
chip iterations costing upwards of $1 million, and ensuing
delays consuming three to six months, the stakes are
high. A new solution and methodology are needed to deliver
complete verification.
The Solution: JasperGold Formal Verification
JasperGold, a block-level verification solution for RTL
designs, uses state-of-the-art formal verification technology
to exhaustively verify functional behaviors of RTL blocks
statically, without simulation or test vectors. JasperGold
analyzes a block against assertions and high-level requirements,
and either proves the assertions and requirements true
for all legal input sequences, or isolates bugs that cause
the requirements to fail. High-level Requirements (HLRs)
describe end-to-end behavior (from inputs to outputs)
that a design must always or never exhibit. A powerful
step up from implementation-specific assertions, HLRs
represent design intent, and cover large portions of
the design. Examples include: data can never be dropped
or corrupted; and, flow control credits can never be
leaked. If an HLR is proven true, no legal set of input
vectors can cause the design to fail.
JasperGold Express is a push-button version of JasperGold
for Assertion-Based Verification (ABV). JasperGold Express
is easy to use and adopt, and provides an easy migration
path for simulation-based ABV users to adopt formal
verification.
JasperGold is also used during the process of RTL design,
before blocks are checked in and long before simulation
testbenches are available. This powerful methodology
allows users to guarantee that their designs will meet
fundamental high-level requirements, derived from the
micro-architecture spec. JasperGold provides users with
insightful and specific feedback into how designs could
possibly fail, influencing design creation to improve
inherent design quality.
Production-proven with an established base of customers
engaged in leading edge design, and over 100 successful
SoC tapeouts, Jasper finally answers the chip industry's
critical need for higher design quality and dramatically
shorter schedules.
Jasper: Formal Verification Unleashed!
|
