For Full-Text 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
IEICE TRANSACTIONS on Information and Systems
Publication Date: 1993/09/25
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>>
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.