Browse Prior Art Database

Switching Circuit Verification

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

Publishing Venue

IBM

Related People

Roth, JP: AUTHOR

Abstract

Switching circuits provide well-known means for realizing logical and arithmetic functions. Designed originally in relay contacts, there has been a resurgence due to designs in large-scale integrated technologies (1), particularly using field-effect transistors. As with logic gate circuits, verification of the correctness of field-effect transistor designs is an important problem. A technique is described for determining the equivalence of two switching-circuit designs.

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

Page 1 of 3

Switching Circuit Verification

Switching circuits provide well-known means for realizing logical and arithmetic functions. Designed originally in relay contacts, there has been a resurgence due to designs in large-scale integrated technologies (1), particularly using field-effect transistors. As with logic gate circuits, verification of the correctness of field-effect transistor designs is an important problem. A technique is described for determining the equivalence of two switching-circuit designs.

If S and T are switching circuits with a one to one correspondence between pairs of terminal nodes, each terminal pair of the circuit defines a logical function, defined by the set of all conditions for which a closed path exists between the nodes. The technique described determines equivalence of circuits S and T by seeking the equivalence/ nonequivalence set of input conditions yielding a closed path in one network and no closed path in the other.

A counter example to their equivalence, if one exists, is constructed in the following manner. Each node is labeled by Lee's algorithm (2) but allowing for multiple values if there are multiple paths between nodes. A first, shortest path is selected, and variable values are assumed to close the path between terminal nodes p and q in circuit S. Next, these values for variables are applied to corresponding elements in the second circuit. If a closed path exists in circuit T, return to circuit S and construct the next closed path. This process is repeated for different paths in circuits S and T, until a particular closed path in circuit S finds no corresponding closed path in circuit T for the same variable value assignments. If there is no closed path in circuit T, as determined by assignments in circuit S, proceed to complete assignments of variable values in circ...