Formal verification of digital circuits using symbolic model checking - Časar, Aleš (Informacije MIDEM, 2000)
This paper presents efficient algorithms for digital circuit verification. The algorithms are based on symbolic CTL (Computation Tree Logic) model checking. We also present an extension of ordinary CTL with fairness constraints. They enable verification of circuits with symbolic model checkingregarding only fair paths in the computaion tree. The model checking algorithms were implemented as part of a fully hime-made program package for manipulating finite machine descriptions of digital circuits, represented with Boolean functions. The package is also based on a fully home-made program package for manipulating Boolean functions, represented with binary decision diagrams.
Keywords: algoritmi; digitalna vezja; odločitveni grafi; preverjanje; verifikacija