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.

Rights

URN

URN:NBN:SI:DOC-6NVC8Q5S

COBISSID

5935638

Added

18.12.2015

Metadata

Citation

APA:

Časar, Aleš, Brezočnik, Zmago, Kapus, Tatjana (2000). Formal verification of digital circuits using symbolic model checking. Informacije MIDEM, volume 30, issue 3, str. 153-160. URN:NBN:SI:DOC-6NVC8Q5S from http://www.dlib.si

MLA:

Časar, Aleš, Brezočnik, Zmago, Kapus, Tatjana. "Formal verification of digital circuits using symbolic model checking." Informacije MIDEM volume 30. issue 3 (2000) str. 153-160.
<http://www.dlib.si/?URN=URN:NBN:SI:DOC-6NVC8Q5S>

Informacije MIDEM
1986-
(Assembly record)

Formal verification of digital circuits using symbolic model checkingFormalna verifikacija digitalnih vezij s simboličnim preverjanjem modelov

Formal verification of digital circuits using symbolic model checking
Formalna verifikacija digitalnih vezij s simboličnim preverjanjem modelov