Jasper introduces updates to its formal verification and design tools

Jasper Design Automation , determined not to be left aground by the outrushing economic tide, is attempting to extend their market reach into new areas beyond the enclaves of experts that have in the past defined formal verification use. Previously we’ve written about Jasper’s ideas regarding formal property-proving as a design tool. Today, the company has introduced several product improvements and one packaging change, intended to expand their available market even farther.

The underlying themes stay the same. Jasper wants to make its tools more widely accessible, and to encourage designers to employ them in new areas. The first—and possible most pressing, given the current environment—idea is Jasper Core. In essence, Jasper Core is a stripped-down product for seasoned formal-verification users. It leaves out the interactive features of the flagship Jasper Gold, but includes the dozen or so proof engines and control systems that lie at the heart of the Gold product. Hence it is a batch-oriented, rather than an interactive, tool that Jasper CTO Rajeev Ranjan says is "an economic application of licenses." From which I read that you can actually use Jasper Core for less front-end investment than would be required for Gold.

In addition to the new, more economical use model, Jasper is announcing two major enhancements to both the Core and Gold products: ProofGrid, and ProofPower. Each focuses on the dual tender-spots in the formal story–speed and capacity–but each in a different way.

ProofGrid is a parallelization supervisor for the proof engines in the Jasper product. It allows you to dispatch separate tasks on separate CPUs, blades, or servers. Unlike most of the multithreading announcements from other EDA vendors recently, ProofGrid works in a way that minimizes intertask communications, and hence can distribute a job across a network, not just across CPUs on a single motherboard.

ProofGrid can separate tasks out by the property they are evaluating. More elegantly, it can dispatch different proof engines working on the same property to different processors. More clever still, it can dispatch different steps in a single proof engine to different processors. And the dispatch is dynamic. That is particularly important because of the parallel way the Jasper engines work. When you ask Core or Gold to evaluate a property, ProofGrid fires up all the appropriate proof engines for which it has available processors, to see which one will finish first—in essence, speculatively executing all but one of them. Once an engine terminates, the property is evaluated, so ProofGrid terminates all the other engines working on the same property and releases them back into the pool. This approach allows ProofGrid to keep a substantial number of servers active across a network, and to reduce evaluation times, while not dying of data thrashing.

ProofPower, in contrast, is a package of under-the-hood improvements in the Jasper code aimed at increasing evaluation speed and reducing memory footprint. Ranjan said that, for example, there was a new design-traversal algorithm that reduced the state space the proof engines had to cover for a given property. There are improvements to the engines themselves. And Jasper has added some new, more abstract structures to its vocabulary, allowing the engines to treat such structures as memory instances or multipliers as functional units rather than dealing with them as complex circuits.

The last major part of this compound announcement is an enhancement to ActiveDesign, Jasper’s foray into the design world. Company vice president of marketing Holly Stump says the point of ActiveDesign is that it is a development tool, not a verification tool. She says that it is particularly showing its value in integration of third-party IP. With ActiveDesign, designers can test their understanding of how a piece of IP actually works without having to construct a test bench, without running exhaustive simulations, and without the risk of missing the corner case where the IP behaves badly. The interactive formal tool can also detect situations in which new surroundings or even just new configuration parameters may break an important property of an IP block. And all this can be done without users having to acquire a detailed understanding of the circuitry within the IP block.

Aiding in that enterprise is the new bit: QuietTrace. One of the problems with using the waveform viewer in ActiveDesign is that it shows you all of the activity on the signals you are watching, whether that activity is relevant to the property you are checking or not. QuietTrace filters out transitions that are not relevant to the proof at hand—ignoring, for example, transitions on signals that do not influence the property, or values on a bus if the evaluation of the property does not depend on the content of bus traffic.

Together, Jasper hopes that the new additions to the product line will extend the company’s reach into more budget-constrained verification groups; and deeper into design, IP evaluation, and IP integration teams who are starting to find formal proof a valuable weapon in their attempt to create correct designs with third-party blocks.