DocumentCode
3439697
Title
Formal verification of design correctness of sequential circuits based on theorem provers
Author
Camurati, Paolo ; Margaria, Tiziana ; Prinetto, Paolo
Author_Institution
Dipartimento di Autom. e Inf., Politecnico di Torino, Italy
fYear
1991
fDate
13-16 May 1991
Firstpage
322
Lastpage
326
Abstract
After a presentation of alternative time modeling techniques, the description techniques available in OTTER, a first-order logic proof environment at the different abstraction levels are presented. A discussion is presented of the methodology envisaged for the proof of correctness and its implementation in OTTER depending on the circuit characteristics and on the reasoning technique. Some experimental results are also reported
Keywords
integrated circuit testing; logic testing; sequential circuits; theorem proving; OTTER; abstraction levels; alternative time modeling techniques; design correctness; first-order logic proof environment; sequential circuits; theorem provers; Clocks; Contracts; Equations; Formal verification; Hardware; History; Logic devices; Sequential circuits;
fLanguage
English
Publisher
ieee
Conference_Titel
CompEuro '91. Advanced Computer Technology, Reliable Systems and Applications. 5th Annual European Computer Conference. Proceedings.
Conference_Location
Bologna
Print_ISBN
0-8186-2141-9
Type
conf
DOI
10.1109/CMPEUR.1991.257404
Filename
257404
Link To Document