Title :
Automatic generation and verification of sufficient correctness properties for synchronous processors
Author :
Van Aelten, F. ; Liao, S.Y. ; Allen, J. ; Devadas, S.
Author_Institution :
Res. Lab. of Electron., MIT, Cambridge, MA, USA
Abstract :
A general strategy for automatically generating and verifying sufficient correctness properties for a broad class of synchronous processors is presented. Given a particular specification and implementation pair, it is shown how basic correctness properties can be algorithmically translated into a set of computation tree logic (CTL) formulae which are sufficient for equivalence between the behavioral and logic descriptions. Preliminary experimental results on the verification of microcoded and array processors are presented.<>
Keywords :
formal specification; formal verification; parallel processing; protocols; array processors; automatic verification; behavioural descriptions; computation tree logic; logic descriptions; specification; sufficient correctness properties; synchronous processors; Parallel processing; Protocols; Software requirements and specifications;
Conference_Titel :
Computer-Aided Design, 1992. ICCAD-92. Digest of Technical Papers., 1992 IEEE/ACM International Conference on
Conference_Location :
Santa Clara, CA, USA
Print_ISBN :
0-8186-3010-8
DOI :
10.1109/ICCAD.1992.279377
