DocumentCode
1684882
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
fYear
1992
Firstpage
183
Lastpage
187
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;
fLanguage
English
Publisher
ieee
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
Type
conf
DOI
10.1109/ICCAD.1992.279377
Filename
279377
Link To Document