Startup promises ‘pure’ formal tool for verification
Santa Cruz, Calif. – An easy-to-use, “pure” formal verification tool that overcomes existing capacity limits is what revitalized EDA startup Jasper Design Automation is promising as it rolls out its JasperGold product this week. Formerly called Tempus Fugit, Jasper has new top management, new funding and new technology for what it calls “specification-level” verification.
Tempus Fugit was at the Design Automation Conference last year, previewing technology for verifying standard interface protocols. But JasperGold goes well beyond interfaces, promising exhaustive block-level verification from high-level, specification-level requirements as well as lower-level assertions.
Since last year, Jasper has raised $7.1 million and hired EDA veteran Kathryn Kranen as its president and chief executive officer. The Mountain View, Calif.-based company has also recruited Harry Foster, the former chief architect at Verplex Systems and the current chairman of the Accellera formal verification committee, as its new chief methodologist.
“Now we're really launching,” said Kranen. “We're taking what we know about standard inter-faces and building into the tool an intelligence that used to require PhD users.” Jasper's technology, she said, is the “first real breakthrough” to solve both capacity and ease-of-use problems. “I feel we are defending the honor of formal verification,” she said. “Most companies have sacrificed the goal of 100 percent exhaustive proof.” While many vendors have adopted a “semiformal” approach that uses simulation, Jasper thinks that “pure formal”-which does not rely on simulation-is the way to go, Kranen said.
Jasper has gotten the attention of Gary Smith, chief EDA analyst at Gartner Dataquest, who has been deeply skeptical about the large number of companies crowding into the RTL verification market. “It does look like a breakthrough,” he said of the Jasper product. “Formal verification is an important enough tool that there is room for a better technology.”
There are, however, dozens of established EDA companies with formal and semiformal tools, including a number of assertion and property checkers. Jasper must compete in this overpopulated marketplace with a new tool that requires some extra Verilog coding and interactivity on the part of the user.
Jasper's technology is based on a “precognitive engine” that claims to overcome capacity limitations. It does this through “state-space tunneling,” a technique that guides the formal proof engines to analyze only those portions of a design relevant to proving each requirement. Thus, the company claims, there's no restriction to a small proof radius, as found in other formal tools.
JasperGold is an interactive tool, and it employs “relevance directives” that let the user direct the precognitive engine, much as floor planning guides placement and routing. “The user plays a game with the tool,” said Vigyan Singhal, who founded Tempus Fugit and is now Jasper's vice president of engineering. “With the interaction between the user and the tool, the tool knows more about where to tunnel into the design.”
What is perhaps most different about JasperGold is its ability to execute specifications that provide a higher level of abstraction than assertions. “An assertion can be very ad hoc-it can just be a set of statements,” said Foster, the company's chief methodologist. “A specification is a much more complete definition of what I'm trying to do.”
Foster said that specifications describe end-to-end (input-to-output) behavior, while assertions typically do not. Specifications, he said, describe complex behavior at a high level of abstraction, typically requiring additional behavioral modeling. Finally, Foster observed that specifications can handle both control and data path, whereas assertions typically can't verify data paths.
JasperGold, however, is for blocks that do not undergo data transformations or perform mathematical computations. “It's not for the computational part of DSP,” said Singhal.
 |
Available in June
Blocks tend to be 20,000 lines of register-transfer-level Verilog code or less, Kranen said.
JasperGold will be available June 1 starting at $225,000. Jasper also sells “proof kits” for a number of standard interfaces, including PCI, PCI-X, PCI Express, Firewire, ARM Amba, USB, AGP, DDR, Gigabit Ethernet and others.
This, said Kranen, is “the largest body of formal verification IP [intellectual property] in the industry.”
To use JasperGold, designers must first capture specification-level requirements in Verilog or translate them from other languages. There's about a 10 percent additional effort beyond the original design, Kranen said. But she said that's much better than block-level simulation, where the testbench can be far larger than the original Verilog code. With JasperGold, the specification requirements are typically 10 times smaller than the RTL block, she said.
People will still do system-level simulation, Kranen acknowledged. “This is an enabling technology to verify you have absolutely clean blocks. It dramatically shortens the system simulation time,” she said.
Interactive operation
JasperGold is not a pushbutton process. Kranen described a flow in which the precognitive engine analyzes the design and comes back to the user with suggestions on how to eliminate irrelevant portions. The user sets forth assumptions that help the tool navigate the state space. Users also tell the tool whether a given waveform, or combination of events, is legal.
JasperGold will either show that a specification is 100 percent proven, or present waveforms that are counterexamples. The tool can also generate a monitor to use in simulation. It works with one specification at a time. “It's enabling the designer to build a formal testbench,” said Foster. “This is basically what a PhD had to do in the past.”
It's now up to Kranen to turn Jasper into a thriving commercial enterprise. Her track record is promising. While she was president and CEO of Verisity, that company grew from six to 80 people and gained an 84 percent share of the functional verification automation-software market. Prior to Verisity, Kranen spent seven years at Quickturn Design Systems, most recently as vice president of North American sales.
Kranen declined to say how many people work at Jasper Design Automation, although she noted that six members of the engineering team have PhDs in formal verification. “I was amazed at the technologists here,” she said. “It's in the wind that there's a breakthrough here.”
“This is the largest set of talent I've ever seen working in one area,” said Foster.
The company has a Web site at www.jasper-da.com.
Leave a ReplyCancel reply
This site uses Akismet to reduce spam.Learn how your comment data is processed.
Advertisement
