• DocumentCode
    3105189
  • 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
  • fYear
    1991
  • fDate
    25-28 Feb 1991
  • Firstpage
    11
  • Lastpage
    15
  • 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;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Design Automation. EDAC., Proceedings of the European Conference on
  • Conference_Location
    Amsterdam
  • Type

    conf

  • DOI
    10.1109/EDAC.1991.206349
  • Filename
    206349
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=3105189