
For FullText PDF, please login, if you are a member of IEICE,
or go to Pay Per View on menu list, if you are a nonmember of IEICE.

Automatic Generation and Verification of Sufficient Correctness Properties of Synchornous Array Processors
Stan Y. LIAO Srinivas DEVADAS
Publication
IEICE TRANSACTIONS on Information and Systems
Vol.E76D
No.9
pp.10301038 Publication Date: 1993/09/25 Online ISSN:
DOI: Print ISSN: 09168532 Type of Manuscript: INVITED PAPER (Special Issue on Synthesis and Verification of Hardware Design) Category: Design Verification Keyword: formal verification, automata, language, and theory of computing, hardware and disign,
Full Text: PDF>>
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 automatatheoretic 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 pasttense computation tree logic (CTL) formulae and verified by CTL modelchecking procedures. Experimental results of the verification of a matrix multiplication array and a Gaussian elimination array are presented.

