ARM selects Jasper for formal verification of IP
-- EDN, May 19, 2009
Jasper Design Automation has announced that ARM has adopted its JasperGold verification system. John Goodenough, ARM director of design technology, commented, “ARM is applying Jasper technology to the design and verification of increasingly sophisticated IP, with a view to increased assurance levels, reduced verification effort, and lower risk and support costs.”
JasperGold is enabling ARM to address IP development needs through application of formal verification to complex processor designs, utilizing JasperGold’s proof engines as well as productivity enhancers such as advanced visualization as well as the company’s Design Tunneling and Proof Accelerators technologies. Goodenough stated, “JasperGold capabilities will assist in proving complex IP such as the ARM Cortex™ family of products, in reducing the burden of constrained random simulation, and in formalizing IP specifications for new IP.” JasperGold is being used by design teams in multiple ARM design centers worldwide.
JasperGold provides rapid bug detection and debug as well as end-to-end full proofs of expected design behavior; it is a formal verification tool that enables seamless scalability from formal assertion-based verification (ABV) to exhaustive end-to-end proofs of microarchitecture-level properties. Jasper’s Proof Accelerators speed up formal proofs to significantly reduce verification complexity, and combined with Design Tunneling can perform full proofs on properties that have previously failed to converge.
Jasper supported ARM to achieve an ambitious set of verification goals, including the establishment of a methodology for developing, debugging, and proving high-level properties. Goodenough said, “ARM utilizes multiple verification methodologies and strategies including formal verification. Success with formal verification is highly dependent on good methodology. JasperGold provides the supporting methodology and workflows that allow us to tackle more complex and higher value properties than previously. Complete proofs of appropriate high-level properties will further increase assurance levels of ARM products.”
