advanced
Journal Information
Journal Information
   Description
   Editorial Board
   Guide for Authors
   Ordering

Contents Services
Contents Services
   Regular Issues
   Special Issues
   Authors Index

Links
Links
   FEI STU Bratislava
   SAS Bratislava

   Feedback

[1, 2008] 

Journal of Electrical Engineering, Vol 59, 1 (2008) 14-22

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]


© 1997-2019  FEI STU Bratislava