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
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;
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
DOI :
10.1109/CMPEUR.1991.257404
