Temporal logic in verification of digital circuits

被引：0

作者：

Kotmanova, Daniela ^{[1
]}

机构：

[1] Slovak Tech Univ Bratislava, Fac Informat, Inst Comp Syst & Networks, Bratislava 81219, Slovakia

来源：

JOURNAL OF ELECTRICAL ENGINEERING-ELEKTROTECHNICKY CASOPIS | 2008年 / 59卷 / 01期

关键词：

temporal logic; automatic verification; model checking; digital design; Symbolic Model Verifier (SMV);

D O I：

暂无

中图分类号：

TM [电工技术]; TN [电子技术、通信技术];

学科分类号：

0808 ; 0809 ;

摘要：

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.

引用

页码：14 / 22

页数：9