TEMPORAL LOGIC IN VERIFICATION OF DIGITAL CIRCUITS

Daniela Kotmanová

   Verification of hardware circuits is a fundamental part of the hardware design. The paper presents temporal logic as a very powerful verification tool. Temporal logic is a classical logic perceived as a function of time. Now, the truth values of logical propositions change as the time flows on. We fetch up in a space of logical assertions in which, we emphasize, the time is flowing, that is, it is a variable, not a constant. Temporal logics, in principle, are linear or branching where linear means linear-time temporal logic (LTL) and branching branching-time temporal logic (CTL). Both can be used in SMV (Symbolic Model Verifier), a model checking-based verification system for digital devices. In this paper, we describe the results we obtained in our verification of a design of the binary comparator.

Keywords: temporal logic, automatic verification, model checking, digital design, Symbolic Model Verifier (SMV)

[full-paper]