Browse Prior Art Database

Regular Algorithm Verifier

IP.com Disclosure Number: IPCOM000082066D
Original Publication Date: 1974-Sep-01
Included in the Prior Art Database: 2005-Feb-28
Document File: 1 page(s) / 12K

Publishing Venue

IBM

Related People

Roth, JP: AUTHOR

Abstract

In the area of computer generated logic design, there exists the problem of ascertaining whether or not two programs are equivalent. The problem precisely stated is: Given two algorithms, A and B, to determine whether or not they will differ up to a given number of executions of the algorithm until the computer itself breaks down.

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

Page 1 of 1

Regular Algorithm Verifier

In the area of computer generated logic design, there exists the problem of ascertaining whether or not two programs are equivalent. The problem precisely stated is: Given two algorithms, A and B, to determine whether or not they will differ up to a given number of executions of the algorithm until the computer itself breaks down.

In this latter connection, an algorithm is described in the publication "Verify: An Algorithm to Verify a Computer Design", J.P. Roth, IBM Technical Disclosure Bulletin, Vol. 15, No. 8, January 1973, pp. 2646-2648, which can be employed to determine whether or not two "regular" logical designs are equivalent. This is a comparison of two hardware embodiments of algorithms. The term "regular" is defined in the above-mentioned Technical Disclosure Bulletin.

In the technique described herein, the algorithm described in the aforementioned IBM Technical Disclosure Bulletin publication is employed to ascertain whether or not two algorithms are equivalent. In this technique, algorithms to be tested for equivalency are described in a language PL/R, which is a variant of PL/I and syntactically equivalent to the R-notation. The use of R- notation and its usage in computer design is described in RC 4658, J. P. Roth and L. S. Levy, December 20, 1973, published by the IBM Corporation.

After the algorithms have been so described, they are transformed by an appropriate program called RTRAN also utilizing R-notation into regul...