Paris, France, February 17, 2004 - IBM announced today a new verification platform that will allow engineers to harness the power of parallel computing, thereby enabling them to rapidly verify complex chip designs and ensure their new devices work the way they should.
RuleBase PE is a breakthrough static assertion-based verification solution, where a design is validated against its functional specification, as captured by user-specified "assertions". It is based on parallel formal and semi-formal verification algorithms that were developed in IBM Research labs at Haifa, Israel and is available to customers and partners through IBM Engineering & Technology Services.
"RuleBase PE, built on IBM's new parallel formal verification technology, is an industrial-strength tool that gives designers and verification engineers an upper hand when it comes to finding evasive design bugs throughout the design cycle," said Dr. Yaron Wolfsthal, manager of the IBM Formal Methods group at the IBM Haifa Labs, where RuleBase Parallel Edition was conceived. "We can verify large-scale designs at a fraction of the time required by other formal verification techniques."
RuleBase Parallel Edition offers support for the new PSL/Sugar standard property specification language. IBM RuleBase technology has been a cornerstone of the formal verification field since the early 1990s, and was among the first industrial formal verification solutions made available to engineers.
Over the last decade, RuleBase has been leveraged to verify ASICs and microprocessors developed by IBM and partners. The new RuleBase Parallel Edition platform takes advantage of the traditional strengths of IBM's technology, while embodying the results of IBM's newest research in the area of formal verification.
Using IBM's new static analysis methods, RuleBase Parallel Edition can verify a logic design against a set of PSL/Sugar assertions that represent the desired behavior of the design. To this end, RuleBase Parallel Edition employs two complementary schemes of parallel formal verification. The first scheme, 'fine-grained parallel FV' includes algorithms for the decomposition of a large verification task into smaller, tractable subtasks. These subtasks are solved in parallel by coordinated verification threads and are then conjoined to produce the solution for the original task. The second scheme, 'coarse-grained parallel FV' uses a sophisticated engine dispatcher, capable of distributing multiple verification tasks across a set of collaborating verification engines. To maximize verification performance, RuleBase Parallel Edition implements parallel formal verification on top of a large server farm via job-brokering software such as Load Sharing Facility (LSF) or Condor. In addition, RuleBase Parallel Edition provides a single, central point for controlling all verification tasks, thus optimally exploiting the computing power available in the underlying (possibly heterogeneous) network of workstations.
Parallel formal verification supports exhaustive state-space search and partial ("semiformal") search alongside traditional simulation of the design. Using a combination of these verification modalities, RuleBase Parallel Edition achieves a very high level of coverage, which can rapidly detect evasive design flaws that would have been very difficult to find using other verification methods.
"RuleBase Parallel Edition is the next-generation solution for making assertion-based verification a productive and extensive verification solution for the engineering community," Dr. Wolfsthal added. "By marrying massively parallel computing with formal verification, we have addressed two major problems: the size of the design it can verify and the time needed to verify that design. With RuleBase Parallel Edition, we have enabled the engagement of large simulation farms to achieve better, faster and more cost-effective formal verification."
RuleBase Parallel Edition runs on AIX, Solaris, and Linux and supports the standard property specification PSL/Sugar. IBM offers a demand-based licensing scheme to help users affordably leverage the unique capabilities enabled by the new tool.
Visit the IBM Formal Methods Homepage at: http://www.haifa.il.ibm.com/projects/verification/Formal_Methods-Home/index.html