Browse Prior Art Database

Boolean Comparison Using Correspondence Relations

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

Publishing Venue

IBM

Related People

Bahnsen, RJ: AUTHOR [+2]

Abstract

Previously, the only relationships of facilities to nets used in Boolean comparison for hardware verification have been those of simple equivalence: (facility=net) or (facility-net). The segment built for this kind of relationship is shown in Fig. 1. There are important cases, however, that are not handled by this simple relationship. One such case is the following: The input bus for one side of an adder is not directly accessible in the hardware because the final OR is buried inside the adder. For each bit position there are two nets accessible in the hardware which, if ORed together, represent a single bit of the input bus described in the flowcharts.

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 35% of the total text.

Page 1 of 4

Boolean Comparison Using Correspondence Relations

Previously, the only relationships of facilities to nets used in Boolean comparison for hardware verification have been those of simple equivalence: (facility=net) or (facility-net). The segment built for this kind of relationship is shown in Fig. 1. There are important cases, however, that are not handled by this simple relationship. One such case is the following: The input bus for one side of an adder is not directly accessible in the hardware because the final OR is buried inside the adder.

For each bit position there are two nets accessible in the hardware which, if ORed together, represent a single bit of the input bus described in the flowcharts. Rather than compromise the flowcharts by defining two facilities for the input bus, a correspondence relation of the following type is specified for each bit j: BUSIN(j)=netj1 + netj2 (+ means OR)

Boolean comparison can be extended by adding networks in cascade with the logic models. The method described here uses a different approach, which has the following advantages: 1. The method only depends on a description of the

relationship between states of subsets of facilities

and states of subsets

of nets. Because of this, models do not have to be

altered in order to perform the comparison.

2. The same relations are used for both outputs and inputs.

3. "Don't care" conditions are handled in a natural way

as part of the description

of the relationship between sets of states.

The method will be described by first indicating a current method to perform Boolean comparison. It is then shown how this method can be formulated in terms of simple binary relations defined on sets of facility states and sets of net states. These relations are then allowed to be arbitrary to permit more general Boolean comparison. Characteristic functions are used to specify the relations. Finally, the method for building the logic model for the general Boolean comparison is outlined and an example is given. Signal correspondence data is used to convert two logic models into a combinatorial logic form that is suitable for Boolean comparison. Fig. 2 illustrates the result of this processing when the signal correspondence indicates that facilities X1 to Xr correspond to nets U1 to Ur and facilitities Y1 to Yq correspond to nets V1 to Vq. Note that corresponding inputs have been tied together and corresponding outputs have been Exclusive ORed to yield check outputs C1 to Cq. Any assignment of values to X1 to Xr such that any check output C1 to Cq assumes the value 1 represents a counter example illustrating nonequivalence of the flowchart model F and the hardware model H. If no counter example exists, the two models are equivalent.

We may view the signal correspondence Xl <--> U1 as a relation, called a correspondence relation, defined on the set of states that are possible for X1 and the set of states for U1. In this case we

1

Page 2 of 4

have the simple relation X1...