|
 |
|
JasperGold
Verification System Family
The First Verification Solution to Ensure Correctness Where it Matters Most |
 |
‘DEEP FORMAL’ ENSURES CORRECTNESS WHERE IT MATTERS MOST
While formal ABV is a powerful way to increase bug detection and ramp code quality quicker, for full end-to-end proofs, JasperGold Verification System provides confidence where it counts. Designed around Jasper’s unique Design Tunneling formal infrastructure, JasperGold Verification System provides the highest level of exhaustive proof confidence available today. Properties can be specified as end-to-end block-level microarchitecture statements known as High-Level Requirements. These properties express input-to-output block-level design intent. Proving properties at higher levels in the design exhaustively tests far greater logic than even hundreds of individual ABV assertions scattered throughout the logic. Proofs such as these provide the highest level of design confidence available from commercial formal verification tools today. JasperGold Verification System consistently performs exhaustive verification proofs on properties where other tools fail to converge. The end result is a 10x proof capacity advantage over any other formal verification solution available today.
Included with JasperGold Verification System is Jasper’s family of Parameterizable Property Macros (PPMs). These easy-to-use modeling components are leveraged when complex design logic may result in extended run times or large memory consumption and limit the ability to achieve full proof verification. The models provide formal-safe, engine-specific modeling optimizations which significantly reduce the complexity of the formal analysis. Often users can simply drop these models into their design to get proofs to converge. They can also be used together with Design Tunneling to converge on an exhaustive solution that would otherwise be unobtainable. Models include such components as:
• Datapath modeling
• Scoreboarding
• FIFOs
• Memories
• and more! |
Figure 2: Deep Formal High-Level Requirements |
JasperGold Verification Family Key Benefits
- Dramatically reduces risk of bug escapes and design respins
- Improves verification productivity through rapid bug detection and elimination without a testbench
- Enables fast ramp-up from simulation-based ABV to full formal verification
- Provides strongest verification assurance for aggressive design schedules
- Minimizes RTL integration time by ensuring high quality design blocks
- Provides highest verification ROI through low effort / high quality exhaustive verification
- Ensures correctness where it matters most in your design
|
| |
|
 |
|
|
|
|
|
|
|
|
|
|
|
 |
|
|
|
