SAN FRANCISCO — Formalized Design Inc., a startup in the formal verification area with research bases in Paris and Chandler, Ariz., has hit the ground running with three separate tools already available.

The company is making strong claims for the algorithms and data representation behind its verification tools, stating that they result in software that is 10 to 50 times faster than anything available from competitors. In addition, the company claims that the tools can operate on larger design blocks and can handle multipliers more efficiently than competing tools.

Jim McHood, president and chief executive officer of Formalized Design, would not discuss the technology behind the company's three tools, but he did say that it was not based on binary decision diagrams (BDDs) — the representation used by many other commercially available tools. "We're not patenting it and it's secret," he said. "We've chosen to protect it as a trade secret."

The company's founders include McHood, who worked at Intel Corp. for more than 20 years, as well as Nam Nguyen from Bull and Leonard Drucker from Zycad. Formalized Design currently has 12 employees split between Paris and Chandler. The engineering team has developed two other formal tools in the past, one of which is believed to have been for Bull. But McHood stressed that the earlier development work had no relation to the software that eventually became VFormal. VFormal, which was based on research at Bull and STMicrolectronics, was brought to market by Compass Design Automation and is now sold by Avant!

Formalized Design's three tools are: LEQ, a logic equivalency and property verification tool; Labs, a logic abstraction tool; and MC-Check, a multi-cycle model-checking tool.

LEQ includes built-in commands for property checking to verify such things as mutual exclusivity on a bus, shorts, high impedance paths, scan path connectivity, scan reordering and clock-tree synthesis. LEQ can be used to compare the equivalency of RTL and gate-level descriptions, and can verify the design correctness of any multiplier implementation.

According to Formalized Design, LEQ is the only formal tool that can verify a 64-bit x 64-bit multiplier and large RTL to gate-level comparisons without partitioning a design into small blocks. "We can typically handle up 10 times to 20 times larger blocks of logic" than other formal tools, McHood said.

The company's literature states that its algorithms demonstrate linear performance and memory utilization characteristics as design complexity increases, whereas BDD derivatives and symbolic simulation methods demonstrate exponential behavior.

The tool also isolates the difference between two designs. "We can find 75 percent of design errors in 15 minutes or less," said McHood. "The diagnostic capability is good enough to avoid the need to go to simulation — although you can if you want."

The Labs tool accepts transistor- or gate-level inputs and automatically produces synthesizable RTL VHDL or Verilog that is formally equivalent. Inputs can be in the form of EDIF, Spice, Verilog or VHDL. It can work with static and dynamic designs, and copes with both synchronous and asynchronous designs.

Labs can be used for reverse engineering and retargeting of chip designs. The use of Labs and LEQ together allow equivalency checking between RTL and transistor-level representations of circuits.

MC-Check verifies within specified or infinite cycle periods that bus protocols and design behavior are implemented correctly. For RTL designs, a Verilog-like language called Assertion Assistant allows expressions of time to be included in constructs. Assertion Assistant is used to describe proposed assertions which must "always be true," "should never be true" or are "sometimes true."

The three tools all run under Sun and Hewlett-Packard workstations, and will run on PCs with Windows NT in the next few months. Each tool is priced at $75,000, with discounts available for multiple purchases.