EDA startup pursues formal validation

EDA startup pursues formal validation
By Richard Goering, EE Times
July 18, 2001 (6:32 p.m. EST)
URL: http://www.eetimes.com/story/OEG20010718S0068

MOUNTAIN VIEW, Calif. — A privately funded EDA startup, Veritable Inc., is quietly providing "formal validation" tools that can statically and dynamically check properties and generate CPU instruction streams. Aside from a small booth at the Design Automation Conference last month, Veritable has had no public exposure, but the company has been developing its technology with several key customers during the past three years.

Formal validation is a new category of tool that marries traditional analysis techniques with formal verification, said Prab Varma, president of Veritable, based here. "We're tackling the problems of handling large designs using property-checking techniques that are checking RTL [register-transfer-level code] vs. behavior," Varma said. "The reason we call it formal validation, not formal verification, is that we're trying to give a practical bent to it."

Veritable today is shipping Verity-Check, a static property checker for RTL code, and Verity-CPU, which generates targeted and random instruction streams for CPU verification. Soon to come is Verity-Validation, a dynamic functional property checker.

Veritable was co-founded by Varma and by Will Kaku, who serves as vice president of engineering. Varma previously held vice president of engineering positions at Duet Technologies and Crosscheck Technology. Kaku held management posts at Crosscheck, Compass, Teradyne EDA and elsewhere.

The company has 12 employees and one named customer, Arcadia Design Systems Inc., a CPU design house. Varma said that Veritable products are being used in production flows today and have been involved in at least three silicon tapeouts.

Veritable is far from the only company offering RTL property-checking tools, but the company has some unique capabilities, Varma said. "We offer the widest range of automatic checks of any tool," he claimed. "We also believe we have the most scalable and highest-pe rforming solution. We've run on real customer designs as large as 4 million gates."

Veritable's tools are property checkers, not model checkers, Varma said. "We have some similarities to cycle-bound model checking, but we're not using traditional model-checking algorithms." The technology is all internally developed, he said, and has not yet resulted in any published papers.

Verity-Check offers four levels of property checks. While run-times vary greatly according to a design's complexity and properties, Varma said that one 4 million-gate design for a server chip set was checked in around two hours.

When an error is found, Verity-Check opens the source code file and highlights the offending line of code. For certain properties, it can also generate a counterexample in the form of a testbench. This allows users to run simulation and locate the problem in a waveform viewer.

Verity-CPU uses the same underlying technology as Verity-Check, but the mission is different. Verity-CPU generates an asse mbly language program that's loaded into the simulator model of a CPU memory. The program contains instructions that are used as a testbench in HDL simulation.

Pricing for Verity-Check starts at $15,000. Verity-CPU is sold only as part of a services package because Veritable needs to customize the software to the target CPU's instruction set. Varma said it's been used on three CPUs in the consumer electronics area.

Varma said the upcoming Verity-Validation product represents a new type of tool — a property-checking tool that will generate an HDL testbench. Rather than a random testbench, it will be targeted at specific properties, he said. Ideally, users will run the testbench to compare their RTL with the original behavioral description.