Jasper Design Automation is introducing the latest release of its JasperGold/JasperCore formal verification system at Yokohama, Japan’s EDSF 2010 beginning Jan. 28. This JasperGold/JasperCore release delivers new deep proofs and bug-hunting, while adding value across the entire spectrum of formal verification design applications, from architectural and RTL verification to post-silicon debug.

The new release has been tested with leading IC design teams at major microprocessor, graphics processor, IP, and telecom/networking companies.

A new collaborative engine architecture automatically leverages information between engines to boost performance and obtain convergence on complex proofs. Other engines have increased JasperGold/JasperCore’s industry-leading capacity to handle even larger designs, and increase convergence.

JasperGold now features a design explorer dialog where you can access a tree structure of the design logic starting from signals or properties. Design exploration facilitates greater understanding of the design structure and provides an interface to construct the analysis region, thus enabling a smooth transition to Jasper’s Design Tunneling feature for the proof of the most complex properties.

The typical design methodology calls for appropriate control logic that prevents X propagation past "barrier" points. This flow detects Xs and displays a trace demonstrating the effect of their propagation on user-defined target signals. JasperGold detects functional errors not easily found in simulation, including incorrect clock-gating resulting in Xs for register values and incorrect control logic allowing Xs to propagate to output data buses for “valid” data.

A new path sensitization analysis feature allows engineers to analyze the relationships between various signals, including cause and effect between their activities. In today’s complex designs, it is often difficult to understand how signals interact with each other; e.g., an input potentially affecting the value of the output. JasperGold now detects if a signal can actually affect the value of another signal in the design and displays such a trace if it can be found.

Another JasperGold first is the addition of automatic memory abstraction in the Visualize flow, for even greater performance. Visualize automatically generates and manipulates waveforms without a testbench, answering “what-if” design questions and providing visual confirmation of design functionality which is especially useful for RTL development and debug.