Skip to main content

RuleBase Parallel Edition

Formal Verification

Industrial Alliances

The IBM RuleBase development team has a close working relationship with several RuleBase user groups throughout the industry. The IBM team benefits from working closely with these user groups, who provide ongoing feedback resulting from their experience with RuleBase. This feedback is among the strongest forces shaping the direction and continuous innovation of the RuleBase technology.

Some of the RuleBase user groups are referenced below. These groups serve as corporate centers of competence (COC) for their companies in the area of Functional Formal Verification.

  • Marvell Technology Group

    In 1995, Galileo Technology (now a part of Marvell) has established the largest RuleBase user group in the industry outside IBM. This group, comprised of ~10 Formal Verification engineers, routinely applies RuleBase to verify complex logic across Galileo's product line.
    Galileo/Marvell's engineers used RuleBase to verify, among others, the designs of switching chips from the GalNet family, High-performance Router Chips for IBM PowerPC-based and MIPS-based Systems, and System Controllers for Systems-based on PowerPC 970.
    The Marvell chip design methodology uses RuleBase in two modes: (1) as a platform for Unit Verification, and (2) in late design phases, as a means for reconstructing logic bugs found in Silicon; these bugs are difficult to reconstruct using simulation.

    More information:
    • Description of the Discovery LT system controller from Marvell, featuring the IBM embedded microprocessor PowerPC 750FX/GX. Discovery LT has been subjected to heavy-duty formal verification. In particular, both the CPU interface and the DRAM interface of Discovery LT have have been successfully verified by Marvell's formal verification team, using RuleBase.

    • A press release of the Networking Technology Initiative announced by IBM and Galileo on 9/21/2000.

    • A presentation of Formal Verification in Galileo.

    • A paper by the Marvell team, describing an interesting case study with RuleBase.

  • STMicroelectronics

    STMicroelectronics has been using RuleBase since 1998. Initially, a group of three used RuleBase to verify the implementation of new features added to the ST100 DSP-MCU microprocessor core. RuleBase activity has expanded to support system-on-a-chip design methodology throughout the company, and there are now seven specialized users. Recent work focuses on thorough verification of system interconnect blocks and protocol compliance checking at standard interfaces.

    RuleBase has also been used by the STM team to systematically verify the assumptions used when proving structural equivalence between two levels of a design. Formal verification provides benefits such as early feedback to designers, increased confidence in complex implementations, and clarification of interface specifications.

  • Zoran Microelectronics

    Zoran, a 'fabless' design house, is a provider of digital solutions in the digital entartainment and the digital imaging markets. Zoran licensed RuleBase in 1998, putting the tool to use at its Israel location.
    Zoran's engineers have successfully used RuleBase to verify an MPEG video decoder, a video processing unit (responsible for MPEG video buffers control), a processor decoding function responsible for stall generation, an interrupt arbiter, an ATAPI interface, and a few smaller design blocks.
    The company's successful results with RuleBase were detailed in a paper (PDF, 108K) (DOC, 117K) released by the company and presented in the WAVe workshop at the CAV'2000 conference. A summary of this work has also been published by EETimes.

  • Mellanox Technologies

    In late 2000, Mellanox, a private, fabless semiconductor company founded in March of 1999, established an aggressive Formal Verification effort using RuleBase. Currently, the Mellanox team comprises five FV engineers.

    Mellanox is among the first companies to develop Infiniband products. The challenges of Infiniband—a point-to-point high speed switch fabric interconnect architecture with demanding requirements quality of service, fault tolerance and scalability—have led Mellanox to integrate Formal Verification and Testing Technologies in to the company's verification methodology.

    The engineers of Mellanox use RuleBase in the design of a broad offering of InfiniBand products including switches, host channel adapters, and target channel adapters.

    Mellanox successfully used the RuleBase tool as part of its verification strategy for its InfiniBridge integrated switch and channel adapter, the first ever InfiniBand device supporting both 1X (2.5Gb/s) and 4X (10Gb/s) links.

    More information:

  • Analog Devices

    Analog Devices, Inc. (ADI) is a leading supplier of mixed-signal and general-purpose DSPs. In particular, the ADI Israel Design Center is the home of one of the company's flagship products: TigerSHARC. In the development of these product lines, ADI engineers leverage high-performance development tools, including RuleBase and FoCs.

    In mid-2001, ADI determined that the sophisticated, high-performance static superscalar architecture of the company's DSPs required advanced verification solutions, in order to address the verification challenges faced by developers. Following a thorough evaluation, ADI engineers selected IBM's Formal Verification tools for inclusion in the company's verification flow. Since then, ADI engineers have employed RuleBase and FoCs in the verification of the most complicated blocks in TigerSHARC, including internal memory cache controllers, DMA link protocols, and other safety-critical logic units and mechanisms.

    The ADI Formal Verification team presently comprises two full-time and one part-time engineer. The Formal Verification staff supports the design process from initial architecture conception until the silicon implementation stage. The FV team thus has a deep perspective of the chip which, in turn, enables the application of the most advanced formal verification techniques, including abstract, chip-level architecture verification, compositional verification, and the creation of suspect scenarios detected on the test floor. Overall, the use of RuleBase Premium and FoCs by Analog Devices engineers has become a powerful part of the verification flow, and has served to increase overall assurance of design quality. See the following presentation and abstract to learn more about the synergetic application of Formal Verification and simulation in Analog Devices.

  • NoBug Consulting Inc.

    Established in 1998, the NoBug Consulting company provides design and verification services to ASIC companies in the US, Europe and Israel.
    Out of the company's 50 engineers, the company has formed a group of 10 formal verification engineers (with plans to expand the team to 20). These engineers render formal verification services, based on RuleBase, to the corporate customers of NoBug.
    NoBug is reporting that leveraging on its formal verification skills helps it establish a clear and recognized impact on design/verification quality in the company's projects.