Browse Prior Art Database

Generalized Method for Multi-way Equivalence Checking Using Boolean Functional Decomposition

IP.com Disclosure Number: IPCOM000050357D
Original Publication Date: 1982-Oct-01
Included in the Prior Art Database: 2005-Feb-10
Document File: 3 page(s) / 40K

IBM

Abstract

Boolean decomposition of Boolean functions (or logical networks) may be used as an aid to a generalized multi-way equivalence checking process. The method is based on "signal correspondence" and "equivalence class" concepts. IVP (Implementation Verification Program) is a system of programs which performs structural and Boolean analysis of logical circuits. IVP's main application is the determination of whether or not corresponding circuits in two different logic models are functionally equivalent.

This text was extracted from a PDF file.
At least one non-text object (such as an image or picture) has been suppressed.
This is the abbreviated version, containing approximately 55% of the total text.

Page 1 of 3

Generalized Method for Multi-way Equivalence Checking Using Boolean Functional Decomposition

Boolean decomposition of Boolean functions (or logical networks) may be used as an aid to a generalized multi-way equivalence checking process. The method is based on "signal correspondence" and "equivalence class" concepts. IVP (Implementation Verification Program) is a system of programs which performs structural and Boolean analysis of logical circuits. IVP's main application is the determination of whether or not corresponding circuits in two different logic models are functionally equivalent.

The IVP system handles automatically the use of multi-way equivalence classes with members which relate to one another through the Identity, Complementarity, and Equivalence relations. However, an equivalence class could contain Boolean expressions as members. These expressions define more complex Boolean relations, and therefore allow for a relaxation of the restrictive rules under which functional comparison can be performed. In fact, the 1-1 correspondence requirement is not needed to be enforced in some cases, such as the case of comparing non-isomorphic combinational sub-machines. For instance, suppose that a given equivalence class consists of three members as follows: A/B X&Y T with "/" and "&" denoting "OR" and "AND" functions, respectively. Here, a user has specified that the Boolean expression A/B is expected to be equivalent to the Boolean expression X&Y and to the variable (net) T. There is no requirement specified here relative to variables (nets) A, B, X, and Y, individually.

To accommodate a more general discussion, consider the diagram in Fig. 1. Here, a user has specified that f=EXP1 (a,b)

g=E...