Skip to main content

RuleBase Parallel Edition

Formal Verification

Results & Impact

In addition to the numerous publications and recognitions, the development team is proud that RuleBase provides real value and impacts numerous IBM design projects across IBM product lines. Typically, in the design projects that use RuleBase, designers and verification engineers find evasive design bugs throughout the design cycle. This is especially valuable in early design stages when other verification means have not yet been ramped up and in very late design stages when simulation techniques have already provided their maximum input.

The following are some specific examples of the impact RuleBase has had on IBM ASIC, processor, and system development programs:

Contributions to Formal Verification of Game Processors
IBM is actively supporting the gaming industry by providing advanced game processor technology to major players in this industry:

  • "IBM microprocessors power all three next-generation gaming consoles including Microsoft Xbox 360, Nintendo Revolution, and Sony PlayStation 3",
    IBM Press Kit, 2005
  • "IBM delivers Power-based chip for Microsoft Xbox 360 worldwide launch",
    IBM announcement, October 25, 2005
  • "What do the Nintendo GameCube's Gekko, Cray's X1 supercomputer chips, NVIDIA's latest GeForce processor, and the next-generation Microsoft XBox and Sony PlayStation all have in common? All of them use chip technology licensed from or manufactured by IBM"
    POWER to the People: History of Chip Making at IBM, Nora Mikes, 28 April 2004.

Game processors are very sophisticated engines that present demanding requirements to designers. The design of such processors requires functional verification of the highest possible quality. To meet this challenge, IBM teams are using formal verification; in one specific case reported here, 95% of a game processor was formally verified with RuleBase PE.

Formal Verification of IBM Power5 Servers
In May 2004, IBM announced the next generation of IBM eServer® iSeries™ servers: the IBM eServer i5 520 and the IBM eServer i5 570. The new eServer i5 server is the industry's first server based on IBM POWER5™ Technology. Parts of this server technology, codenamed "Squadron", were formally verified using RuleBase PE.

Formal Verification of ASIC Cores
IBM offers predesigned cores which allow designers to focus on product differentiation rather than on implementing standard functions. With these cores, where performance, function, and timing parameters have already been resolved, development time can be significantly reduced. IBM's extensive portfolio of cores offers many proven industry-standard functions ready to integrate into customers' ASIC design. To assure high quality, RuleBase was used to formally verify IBM's Ethernet, Infiniband, PCI Express, and other cores.

Formal Verification of the Gigahertz Processor
On December 14, 2001, IBM announced the high-end pSeries 690 server, code-named Regatta. As part of the Regatta development effort, teams in Austin, TX and Haifa, Israel aggressively deployed RuleBase to formally verify the complex 1.3 GHz Power4 processor that drives Regatta. Initial results from this first-of-a-kind formal verification effort were reported in the CAV '99 conference.

Formal Verification of RS/6000 Servers and Supercomputers
The RS/6000 family combines the benefits of UNIX computing with IBM's leading-edge RISC technology in a broad product line -- from powerful desktop workstations to parallel RS/6000 SP systems that can handle demanding scientific tasks (e.g., "Deep Blue"). RuleBase has been used by IBM engineers in Poughkeepsie, NY; Austin, TX; and Haifa, Israel since 1996 to verify safety-critical units in the RS/6000 server product line, including logic units of the following:

More details on this work are available.

Formal Verification of the AS/400

The IBM AS/400 server family, a 64-bit reduced instruction set architecture (RISC), is the IBM mid-range offering aimed at medium-to-large businesses. These servers, developed in Rochester, MN, comprise up to twelve-way, symmetric multiprocessing PowerPC AS processors and offer high-performance CPU power along with reliability and security. Since 1996, RuleBase has been extensively used by IBM engineers in Rochester, MN and Haifa, Israel to formally verify safety-critical units of the AS/400 system. This includes formal verification at both the architecture and the implementation level. For example see:

Formal Verification of IBM System/390
The IBM System/390 Parallel Enterprise Server is the industry leader for "main-frame class" computers. It can handle the workload of up to 50,000 users and more than 30,000,000 transactions per day. Design and verification teams in the S/390 development laboratories located in Boeblingen, Germany and Poughkeepsie, NY, have used RuleBase since 1996, leading to the detection of numerous bugs. Most recently, RuleBase has been used in the verification of the G6 S/390 server. An interesting verification technology developed jointly by the Boeblingen team and the RuleBase Haifa team is based on the integration of formal verification and simulation. It has also been used extensively in other verification projects in IBM. This technique has been recently described in IBM's Journal of R&D.

Formal Verification in the Desktop Computer Product Line (NetFinity)
The IBM Netfinity product line comprises a family of SMP servers that are based on Intel processors. This product line offers scalable solutions for workgroups, small-to-medium businesses, and up to 8-way enterprise-wide servers. Since 1997, RuleBase has been used by IBM engineers in Rochester, MN and Haifa, Israel to formally verify Netfinity servers at the architecture level, which entails a pre-implementation modeling and analysis of the Netfinity specification, including cache coherence protocols, data-consistency, and I/O.
More details on this work are described in a paper presented in DAC 2000. The Pecos system, which this work targeted, was announced by IBM on 8/17/2001.

Formal Verification Applied to SoC Design
The IBM CoreConnect bus architecture is a standard SoC (System on a Chip) architecture that serves as the foundation for the IBM Blue Logic™ product line and for devices developed by IBM Microelectronics for non-IBM customers and licensees. This architecture eases the integration and reuse of processor, system, and peripheral cores within the standard product and custom SoC designs. Elements of this architecture include the processor local bus (PLB), the on-chip peripheral bus (OPB), a bus bridge, and a device control register (DCR) bus. An important component of this architecture is the PLB arbiter, which arbitrates up to 8 PLB masters and supports address pipelining. In 1999, a verification team in Raleigh, North Carolina, engaged in the formal verification of the PLB arbiter using RuleBase.
The results have been documented in a paper presented in DAC 2000.