Browse Prior Art Database

SVERIFY Design Verification Method Using Structure

IP.com Disclosure Number: IPCOM000083464D
Original Publication Date: 1975-May-01
Included in the Prior Art Database: 2005-Mar-01
Document File: 2 page(s) / 15K

Publishing Venue

IBM

Related People

Roth, JP: AUTHOR

Abstract

One of the fundamental problems in design, in particular of computers, is to guarantee that the design is correct. To say that the design is correct actually reduces to the question of determining whether or not one design is equivalent to another, which is assumed itself to be correct. VERIFY/(1)/ is an algorithm which has been programmed and used for the purposes of verifying the correctness of design. Its running time on the average increases exponentially with the complexity of the logic itself.

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

Page 1 of 2

SVERIFY Design Verification Method Using Structure

One of the fundamental problems in design, in particular of computers, is to guarantee that the design is correct. To say that the design is correct actually reduces to the question of determining whether or not one design is equivalent to another, which is assumed itself to be correct. VERIFY/(1)/ is an algorithm which has been programmed and used for the purposes of verifying the correctness of design. Its running time on the average increases exponentially with the complexity of the logic itself.

The measure of complexity is monotonic with the number of primary inputs, as well as the number of circuits and the number of their interconnections. With the IBM Model 91, it was possible to verify all the designs which were run with 32 inputs or less. The running time varies roughly linearly with the number of outputs, so that the number of outputs was not critical.

On the other hand, in new and more sophisticated systems, it may be necessary to be able to verify blocks of the design containing as many as 50,000 circuits. As it stands, VERIFY would never be able to begin to undertake such a task. With the herein described SVERIFY, however, it may very well be possible to handle logics containing tens of thousands of circuits.

Basically the technique is as follows. It is assumed that both designs which are being compared to each other have been defined in a high-level notation. It is assumed that these high-level algorithms are transformed in regular fashion into a regular logic design, possibly one of them at least being performed by the program R-TRANSFORMER . These two designs might differ algorithmically, or they might differ in their manner of implementation, or it might be that they differ in all except one module or block, a comparatively small portion of the total design.

In any event, a block-by-block correspondence between the two R-algorithms is assumed. The designs can be called A and B. Assume that the blocks are of such size that it is possible by VERIFY, to determine that these corresponding blocks are functionally equivalent. Let it be assumed further that the interconnections between the blocks in the two designs are in one-to-one correspondence. It follows, if this is the structural fact, that the overall designs A and B are equivalent if and only if all their corresponding blocks are likewise equivalent.

It can be seen that this technique of splitting, of having a subdivision of the design into smaller pieces which can be handled by VERIFY, allows the building of verification assignations from a "byte-sized block" to larger ones.

It is clear that this process can...