Although IBM has developed some strong EDA technology over the years, the industry giant hasn't had much luck bringing it to market. But the IBM Research Lab in Haifa, Israel, is quietly making some inroads with formal-verification technology and is developing some new technology that applies formal methods to simulation.
Veteran EDA industry watchers may remember the grand splash that IBM made at the 1993 Design Automation Conference, when the company proclaimed its entry into the commercial EDA marketplace as a full-line supplier. Using its Altium value-added reseller channel, IBM offered tools like BooleDozer for synthesis, BoolesEye for formal-equivalency checking and EinsTimer for static-timing analysis.
These tools had little success, and Big Blue's foray into the commercial EDA world soon ended. Synopsys bought some of IBM's EDA technology in 1996.
The IBM Research Lab is keeping a much lower profile. That group has made no announcements about entering the EDA industry, but it has been licensing its RuleBase formal-model checker to both internal IBM groups and external customers, including Galileo Technology, STMicroelectronics, Motorola, Zoran and, most recently, the Israeli fabless semiconductor firm Mellanox Technologies. Mellanox used RuleBase to help develop what are claimed to be the first 10-Gbit/second Infiniband silicon chips.
RuleBase lets users specify temporal properties using a high-level specification language. Its model checking is based on an enhanced version of the public-domain SMV model checker. It employs automatic state-space reduction to cut down on model size, and it generates counterexamples as timing diagrams.
The Mellanox deal also includes access to new IBM technology dubbed PathFinder. This is described as a "formal design exploration" tool that lets designers graphically express behavior of interest. The user is then presented with simulation "scenarios" in which the behavior occurs. It is not necessary to specify the input sequences needed to reach these scenarios. PathFinder also lets designers examine multiple execution paths in parallel.
IBM Research Lab has not yet decided whether to position itself as a commercial EDA vendor. But in effect, it has entered the market with the Mellanox deal, which included $3.6 million in cash and equity. So if you're interested in formal verification, IBM is a company to watch. You can learn more at www.haifa.il.ibm.com/projects/verification.