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

Stan Y. LIAO  Srinivas DEVADAS  

IEICE TRANSACTIONS on Information and Systems   Vol.E76-D   No.9   pp.1030-1038
Publication Date: 1993/09/25
Online ISSN: 
Print ISSN: 0916-8532
Type of Manuscript: INVITED PAPER (Special Issue on Synthesis and Verification of Hardware Design)
Category: Design Verification
formal verification,  automata,  language,  and theory of computing,  hardware and disign,  

Full Text: PDF>>
Buy this Article

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.