Reference:

Robert B. Jones, Carl-Johan H. Seger, and David L. Dill. Self consistency checking. In Mandayam Srivas and Albert Camilleri, editors, Formal Methods in Computer-Aided Design (FMCAD), volume 1166 of Lecture Notes in Computer Science, pages 159-171. Springer-Verlag, November 1996.

Abstract:

We introduce the notion of self-consistency checking, a new methodology for applying formal methods in the debugging process. Intuitively, self-consistency checks functional consistency of a circuit in two different modes or environments. Self-consistency can (1) simplify property verification and (2) enable the use of symbolic simulation in the absence of a concrete specification. We present a correctness model for property verification with self-consistency checking and the formal framework for the technique. Finally, we provide illustrative examples and partial verification results using self-consistency checking on circuits with many thousands of latches.

Download (please read copyright notice):

PostScript (gzipped)
PDF (auto-translated from PS, may have problems)

BibTeX entry:

@InProceedings{JonesSegerDill96FMCAD,
  author    = {Robert B. Jones and 
               Carl-Johan H. Seger and 
               David L. Dill},
  title     = {Self Consistency Checking},
  pages     = {159--171},
  booktitle = {Formal Methods in Computer-Aided Design (FMCAD)},
  editor    = {Mandayam Srivas and Albert Camilleri},
  volume    = 1166,
  series    = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  month     = {November},
  year      = 1996,
}