Logic in Computer Science (LICS 1995)

Paper: Hardware Verification, Boolean Logic Programming, Boolean Functional Programming (at LICS 1995)

Authors: Enrico Tronci

Abstract

One of the main obstacles to automatic verification of Finite State Systems (FSSs) is state explosion. In this respect automatic verification of an FSS M using Model Checking and Binary Decision Diagrams (BDDs) has an intrinsic limitation: no automatic global optimization of the verification task is possible until a BDD representation for M is generated. This is because systems and specifications are defined using different languages. To perform global optimization before generating a BDD representation for M we propose to use the same language to define systems and specifications. We show that First Order Logic on a Boolean Domain yields an efficient functional programming language that can be used to represent, specify and automatically verify FSSs. E.g. on a SUN Sparc Station 2 we were able to automatically verify a 64 bit commercial multiplier.

BibTeX

  @InProceedings{Tronci-HardwareVerificatio,
    author = 	 {Enrico Tronci},
    title = 	 {Hardware Verification, Boolean Logic Programming, Boolean Functional Programming},
    booktitle =  {Proceedings of the Tenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1995},
    year =	 1995,
    editor =	 {Dexter Kozen},
    month =	 {June}, 
    pages =      {408-418},
    location =   {San Diego, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }