Browse Prior Art Database

Implementation Verification Program

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

Publishing Venue

IBM

Related People

Adams, JB: AUTHOR [+7]

Abstract

The implementation verification program (IVP) is a design verification tool. Its basic use is to determine whether two logic design models are functionally equivalent. If the two models are not equivalent, an input pattern (that is, a "counter example"), demonstrating a difference between the models is produced. IVP is based on analysis which does not require any test cases. By contrast, other design verification techniques which are based on simulation do require user specified test cases. IVP is a definitive procedure; that is, if no counter example is found, the two models under consideration are guaranteed to be equivalent. In other words, IVP's verification is complete in the sense that the logic is verified to the same extent as is the case with exhaustive simulation.

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

Implementation Verification Program

The implementation verification program (IVP) is a design verification tool. Its basic use is to determine whether two logic design models are functionally equivalent. If the two models are not equivalent, an input pattern (that is, a "counter example"), demonstrating a difference between the models is produced. IVP is based on analysis which does not require any test cases. By contrast, other design verification techniques which are based on simulation do require user specified test cases. IVP is a definitive procedure; that is, if no counter example is found, the two models under consideration are guaranteed to be equivalent. In other words, IVP's verification is complete in the sense that the logic is verified to the same extent as is the case with exhaustive simulation. Consequently, the question of "How much should a model be simulated?" is eliminated in the case of using IVP for design verification. Data to IVP is characterized as follows:

1. A low level description of the logic representing the

reference model, called Model 1.

2. A low level description of the implementation logic, called

Model 2.

3. Signal correspondence data, relating key nets in Model 1

to their counterparts in Model 2.

4. Control statements telling the program which operations are

to be performed and what options are to be used.

If either Model 1 or Model 2 contain high level blocks (macro blocks), these blocks must be expanded into primitive level blocks prior to the entry into IVP. A block diagram of IVP is shown in Fig. 1. The two models of logic to be compared are contained in the data sets called Model 1 and Model 2. The signal correspondence data is written by the user into the file denoted by SCR. Modeling and structural analysis programs 11 convert the external input data into a set of internal segment models which are used as input to the equivalence check program 12. These programs also convert the SCR file into the Function Variable Map (FVMAP) file for subsequent use by all IVP programs.

The modeling program in box 11 processes Model 1 and Model 2 and transforms them into internal form. In the internal form of these models, all external names are replaced by internal indices. An Index file is created to relate each internal index to its associated external name. This way, the programs in the system are not affected by the length of names used by the user.

The structural analysis program in box 11 determines if the logic in each model is combinational by checking whether any loops exist in it. In the case of sequential logic, the user can indicate "cuts" to break feedback loops by using the signal correspondence input. The program determines if all loops have been broken, and produces a list of all remaining loops (if a...