TEMPORAL LOGIC IN VERIFICATION OF DIGITAL CIRCUITS
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)