QuietTrace™ simplifies the debug process even further. It is a unique Visualize debugging capability that finds interesting behaviors with fewer signal events. Simplification of traces with minimal signal activity accelerates exploration and debugging tasks.
The next step is to prove properties using JasperGold and JasperCore’s multiple formal proof engines. Multiple proofs can be kicked off in parallel with ProofGrid™ and proof jobs can be managed and tracked using ProofGrid Manager™. ProofGrid and ProofGrid Manager boosts the overall performance of formal verification, leveraging the power of local machine, cluster and computer farms, while providing seamless and powerful distribution and collaboration management of the proof engines running on the network, under a unified tracking console. If the property is proved, then the overall goal of proving the property is accomplished. If it fails, there are additional techniques that can help in achieving proof convergence.
Design Space Tunneling™ and State Space Tunneling™ can accelerate the proof convergence process for challenging high-level properties. High-level properties express input-to-output block-level design intent. Proving properties at these higher levels of abstraction is far more powerful and efficient than writing and testing hundreds of lower-level, individual assertions scattered throughout the logic. Complexity Manager™ assists Design Tunneling to provide visibility inside a deep cone of logic and promotes convergence of deep formal proofs for end-to-end, high-level properties.
Proof Accelerators are easy-to-use modeling components, which significantly reduce verification complexity by speeding up formal proofs. Examples include Scoreboard™ for verifying end-to-end data integrity, an asynchronous clock-domain crossing Proof Accelerator, and more. |