Automatic Generation and Verification of Sufficient Correctness Properties of Synchornous Array Processors

Stan Y. LIAO; Srinivas DEVADAS

Automatic Generation and Verification of Sufficient Correctness Properties of Synchornous Array Processors

Stan Y. LIAO, Srinivas DEVADAS

Full Text Views

0

Cite this

Summary :

We introduce automatic procedures for generating and verifying sufficient correctness properties of synchronous processors. The targeted circuits are synchronous array processors designed from localized, highly regular data dependency graphs (DDGs). The specification, in the form of a DDG, is viewed as a maximally parallel circuit. The implementation, on the other hand, is a (partially) serialized circuit. Since these circuits are not equivalent from an automata-theoretic viewpoint, we define the correctness of the implementation against the specification to mean that a certain relation (called the β-relation) holds between the two. We use a compositional approach to decouple the verification of the control circuitry from that of the data path, thereby gaining efficiency. An array processor in isolation may not have a definite flow of control, because control may reside in the data stream. Therefore, for the purpose of verification, we construct an auxiliary machine, which keeps a timing reference and generates control signals abstracted from a typical data stream. Sufficient correctness conditions are expressed as past-tense computation tree logic (CTL) formulae and verified by CTL model-checking procedures. Experimental results of the verification of a matrix multiplication array and a Gaussian elimination array are presented.

Publication: IEICE TRANSACTIONS on Information Vol.E76-D No.9 pp.1030-1038

Publication Date: 1993/09/25

Publicized

Online ISSN

DOI

Type of Manuscript: Special Section INVITED PAPER (Special Issue on Synthesis and Verification of Hardware Design)

Category: Design Verification

Cite this

Copy

Stan Y. LIAO, Srinivas DEVADAS, "Automatic Generation and Verification of Sufficient Correctness Properties of Synchornous Array Processors" in IEICE TRANSACTIONS on Information, vol. E76-D, no. 9, pp. 1030-1038, September 1993, doi: .
Abstract: We introduce automatic procedures for generating and verifying sufficient correctness properties of synchronous processors. The targeted circuits are synchronous array processors designed from localized, highly regular data dependency graphs (DDGs). The specification, in the form of a DDG, is viewed as a maximally parallel circuit. The implementation, on the other hand, is a (partially) serialized circuit. Since these circuits are not equivalent from an automata-theoretic viewpoint, we define the correctness of the implementation against the specification to mean that a certain relation (called the β-relation) holds between the two. We use a compositional approach to decouple the verification of the control circuitry from that of the data path, thereby gaining efficiency. An array processor in isolation may not have a definite flow of control, because control may reside in the data stream. Therefore, for the purpose of verification, we construct an auxiliary machine, which keeps a timing reference and generates control signals abstracted from a typical data stream. Sufficient correctness conditions are expressed as past-tense computation tree logic (CTL) formulae and verified by CTL model-checking procedures. Experimental results of the verification of a matrix multiplication array and a Gaussian elimination array are presented.
URL: https://global.ieice.org/en_transactions/information/10.1587/e76-d_9_1030/_p

Copy

@ARTICLE{e76-d_9_1030,
author={Stan Y. LIAO, Srinivas DEVADAS, },
journal={IEICE TRANSACTIONS on Information},
title={Automatic Generation and Verification of Sufficient Correctness Properties of Synchornous Array Processors},
year={1993},
volume={E76-D},
number={9},
pages={1030-1038},
abstract={We introduce automatic procedures for generating and verifying sufficient correctness properties of synchronous processors. The targeted circuits are synchronous array processors designed from localized, highly regular data dependency graphs (DDGs). The specification, in the form of a DDG, is viewed as a maximally parallel circuit. The implementation, on the other hand, is a (partially) serialized circuit. Since these circuits are not equivalent from an automata-theoretic viewpoint, we define the correctness of the implementation against the specification to mean that a certain relation (called the β-relation) holds between the two. We use a compositional approach to decouple the verification of the control circuitry from that of the data path, thereby gaining efficiency. An array processor in isolation may not have a definite flow of control, because control may reside in the data stream. Therefore, for the purpose of verification, we construct an auxiliary machine, which keeps a timing reference and generates control signals abstracted from a typical data stream. Sufficient correctness conditions are expressed as past-tense computation tree logic (CTL) formulae and verified by CTL model-checking procedures. Experimental results of the verification of a matrix multiplication array and a Gaussian elimination array are presented.},
keywords={},
doi={},
ISSN={},
month={September},}

Copy

TY - JOUR
TI - Automatic Generation and Verification of Sufficient Correctness Properties of Synchornous Array Processors
T2 - IEICE TRANSACTIONS on Information
SP - 1030
EP - 1038
AU - Stan Y. LIAO
AU - Srinivas DEVADAS
PY - 1993
DO -
JO - IEICE TRANSACTIONS on Information
SN -
VL - E76-D
IS - 9
JA - IEICE TRANSACTIONS on Information
Y1 - September 1993
AB - We introduce automatic procedures for generating and verifying sufficient correctness properties of synchronous processors. The targeted circuits are synchronous array processors designed from localized, highly regular data dependency graphs (DDGs). The specification, in the form of a DDG, is viewed as a maximally parallel circuit. The implementation, on the other hand, is a (partially) serialized circuit. Since these circuits are not equivalent from an automata-theoretic viewpoint, we define the correctness of the implementation against the specification to mean that a certain relation (called the β-relation) holds between the two. We use a compositional approach to decouple the verification of the control circuitry from that of the data path, thereby gaining efficiency. An array processor in isolation may not have a definite flow of control, because control may reside in the data stream. Therefore, for the purpose of verification, we construct an auxiliary machine, which keeps a timing reference and generates control signals abstracted from a typical data stream. Sufficient correctness conditions are expressed as past-tense computation tree logic (CTL) formulae and verified by CTL model-checking procedures. Experimental results of the verification of a matrix multiplication array and a Gaussian elimination array are presented.
ER -