Jasper Design Automation, Inc.
Jasper Design Automation delivers industry-leading software solutions for semiconductor design, verification, and Intellectual Property (IP) reuse, based on state-of-the-art formal technology. Customers include worldwide leaders in wireless, consumer, computing, and networking electronics industries. Jasper technology has been an essential part of 150 plus successful chip deployments. Headquartered in Mountain View, CA, the company is privately held, with offices and distributors in North America, South America, Europe, Israel, and Asia. Visit www.jasper-da.com to reduce risks, increase design, verification and reuse productivity and accelerate time-to-market.
Architects and designers specify high-level functions or whole protocols that become the basis for the design implementations. Such specifications are often represented in natural language documents, waveform diagrams, and transition tables that capture the relationship between inputs, outputs, and state transitions of the protocol. Often, however, the specs themselves are complex and can be riddled with errors and inconsistencies because it is very difficult to verify the global interaction between the individual specifications and requirements.
For years, formal users have struggled for ways to report their progress to simulation-centric managers. While the discovery rate of critical bugs is obviously a helpful metric, the bug rate itself is a very coarse measurement that doesn’t express the true value of the results obtained from fully proven or bounded proofs. Formal tool users themselves could also benefit from formal-specific coverage metrics to protect against the potential over-constraint problem and eliminate false confidence in design correctness, as well as have an empirical measurement of the ROI of their formal verification effort.
The Jasper Intelligent Proof Kits and Verification IP solutions enable SoC design teams to accelerate verification by quickly and exhaustively certifying standard protocols such as the latest AMBA 4 (AXI 4, ACE, API, APB) PCIe, DDR, LPDDR, OCP, etc. The Jasper generated protocol related properties allow early exploration and verification of protocol specification and are optimized for formal. They also plug seamlessly into the simulation environment.
The solutions can be used seamlessly with the JasperGold Formal Property Verification App to formally prove the embedded properties, thereby exhaustively verifying that the design meets the protocol specification. Intelligent Proof Kits eliminate the need to manually write properties, which require in-depth understanding of the protocol specification.
JasperGold Apps are based on Jasper's JasperGold technology and are targeted solutions that address specific design and verification challenges.
The semantics of ‘X’ are language and tool dependent. In RTL design, ‘X’ tells the synthesis tool that it doesn't matter whether a 0 or 1 is assigned during logic optimization and in verification (i.e. ‘X’ is a “don’t care”). But in simulation, ‘X’ tells the simulator that a signal value is “unknown”. This mismatch in semantics and incomplete test vectors in simulation can hide bugs that are likely to show up in silicon no matter how careful you are about considering “X optimism” or “X pessimism”.