Title :
Resolution-based correctness proofs of synchronous circuits
Author :
Camurati, Paolo ; Margaria, Tiziana ; Prinetto, Paolo
Author_Institution :
Dipartimento di Automatica e Inf., Politecnico di Torino, Italy
Abstract :
First-order theorem provers like OTTER satisfy the vital need for versatility and efficiency in formal verification of correctness. This paper deals with experiences in applying OTTER to synchronous circuits. Synchronous circuits are first modeled, then proved correct by means of demodulation- and hyperresolution-based methodologies. Experimental examples are discussed, results are reported and a first comparison is drawn with other proof styles
Keywords :
formal logic; logic circuits; theorem proving; OTTER; correctness; formal verification; hyperresolution-based methodologies; proof styles; synchronous circuits; Combinational circuits; Contracts; Demodulation; Formal verification; Logic;
Conference_Titel :
Design Automation. EDAC., Proceedings of the European Conference on
Conference_Location :
Amsterdam
DOI :
10.1109/EDAC.1991.206349
