Browse Prior Art Database

Automation Identification of Equivalence Points for Boolean Logic Verification

IP.com Disclosure Number: IPCOM000084919D
Original Publication Date: 1976-Jan-01
Included in the Prior Art Database: 2005-Mar-02
Document File: 3 page(s) / 16K

Publishing Venue

IBM

Related People

Donath, WE: AUTHOR [+2]

Abstract

This description relates to a method for comparing two large logical (combinational) functions to find whether the two are equivalent.

This text was extracted from a PDF file.
This is the abbreviated version, containing approximately 42% of the total text.

Page 1 of 3

Automation Identification of Equivalence Points for Boolean Logic Verification

This description relates to a method for comparing two large logical (combinational) functions to find whether the two are equivalent.

When comparing two different representations of the same Boolean functions, it can easily be the case that highly excessive computing times are required when the function is moderately complex. For this reason, "breakpoints" are introduced manually in order to enable the product of a sequence of proofs on subproblems, which together prove the equivalence. The described method relates to a method of automatically identifying certain classes of breakpoints and proving these, so that the need for manual intervention is minimized. In particular, so-called "identity" points are detected.

The method by which this is done rests on two parts:

1. Use of the Boolean analyzer described in the addendum.

2. Simulation over various patterns of input variables is used

to determine conjectures on intermediate functions f and g of

the form:

f = 0

f = 1

f = g

f = g.

It is to be noted that these conjectures may be wrong; however, if a function h does not occur in any conjecture, then no theorem of the ahove type exists for h,
i.e., the possibility that h is 0, 1, exactly the same or exactly the inverse of another function is excluded.

The conjectures are then ordered by "level"; i.e., if f is on some path to g, then a conjecture or f normally precedes a conjecture on g. The actual method by which this ordering is achieved is the following:
1. Assign to each intermediate function a sequence number such

that when f is an input of g, f has a lower sequence number

than g.
2. Each conjecture has an order number, which for conjectures on

a single function (f = 0, f = 1) is simply the sequence number

of f and for conjectures on a pair (f,g) either the larger or

the smaller of the sequence numbers of f and g.
3. The conjectures are then ordered by increasing sequence

number.

Each conjecture is then proven in turn, and appropriate substitutions are made. [i.e., if f has higher sequence number than g, and f = g, then a new function not (g) is generated and substituted for every occurrence of f]. Also, the priority number for the backward implication process in the analyzer is increased for the function f involved in an equivalence [nonequivalence] test, so that higher level functions will not attempt to prove that f = 1 or f = 0 can easily be generated.

1

Page 2 of 3

However, this change in the priority is made only if f and g belong separately to specification and implementation.

If the analyzer disproved a conjecture, then a new simulation is made where the counterexample generated is included in the simulation. A new set of conjectures are generated; however, this set includes only functions belonging to yet unproved conjectures, the conjecture which was just disproven.

The process of generating the input patterns which drive the simulation can b...