Browse Prior Art Database

Verify Machine

IP.com Disclosure Number: IPCOM000079665D
Original Publication Date: 1973-Aug-01
Included in the Prior Art Database: 2005-Feb-26
Document File: 2 page(s) / 14K

Publishing Venue

IBM

Related People

Roth, JP: AUTHOR

Abstract

There is described herein a technique for ascertaining whether or not two regular logic designs (RDESIGNS or rlds) are functionally equivalent. In this connection, reference is made to IBM Research RA 48 dated March 1, 1973, pp. 146,7 or IBM Technical Disclosure Bulletin, Vol. 15, No. 8, January 1973, pp. 2361-3, published by the IBM Corporation.

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

Page 1 of 2

Verify Machine

There is described herein a technique for ascertaining whether or not two regular logic designs (RDESIGNS or rlds) are functionally equivalent. In this connection, reference is made to IBM Research RA 48 dated March 1, 1973, pp. 146,7 or IBM Technical Disclosure Bulletin, Vol. 15, No. 8, January 1973, pp. 2361-3, published by the IBM Corporation.

In the carrying out of the technique, let it be assumed that there are two RDESIGNS A and B. Let it be further assumed that A and B are acyclic, whereby there are no feedback routes in the design, and no memory except possibly for the primary input and primary output registers. In accordance with the technique described herein, the assessment is made as to whether RDESIGN A and RDESIGN B are functionally equivalent, by impressing the first binary output value on an output of A and the opposite binary value on the corresponding output of B, such as, for example, a binary 1 for the output of A and a binary 0 for the output of B. The implications of these assignments are immediately taken, such that the technique assigns to the inputs of the blocks from which these outputs have been chosen, values which are forced by such initial assignments, etc.

It is readily apparent that the impressing of particular values on particular lines, notably the corresponding output lines, and drawing the implications therefrom, as well as assigning values to internal lines in a systematic manner assigned by the verify technique, is the process for determining whether or not it is possible to assign the same primary input pattern to each machine which gives a different primary output pattern.

In the situation where RDESIGNS A and B have feedback, i.e., the function performed by these designs depend not only upon the present primary input patterns but also, generally speaking, upon prior patterns and the resulting computations therefrom.

In the RDESIGN, i.e., the regular method of design of logic, the only feedback routes which are permitted are between the primary output register to the primary input register. In general, there may be many of these "stages" consisting of primary input registers (PIR), connections of elementary logic but without feedback followed by the primary output registers (POR), with there possibly being feedback from POR to PIR. With this type of design, the routes to "cut" in order to effect the analysis is an immediate and trivial task, i.e., all of those lines extending from register-to-register are cut for analysis. By the t...