Regular Temporal Logic Expressively Equivalent to Finite Automata and Its Application to Logic Design Verification

IPSJ

Search this article

Abstract

Due to the progress of VLSI technologies logic circuits have become more complex. As a result the possibilities of design errors have increased. Logic design verification therefore has become more important as a means of guaranteeing the correctness of logic design. Logic design verification requires mathematical logic with enough expressive power to describe the behavior of logic circuits. While propositional logic is known to be equivalent to combinatorial logic circuits a class of mathematical logic that corresponds to sequential machines and/or finite automata has not yet been clarified. This paper introduces various types of Regular Temporal Logic (RTL) which is expressively equivalent to finite automata and can express the notion of time explicitly. A design verification algorithm for sequential machines based on a model-checking method of the RTL is also given. Although the complexity of the model-checking problem of the RTL is non-elementary the proposed model-checking algorithm is efficient and still runs in a time proportional to the size of the structure models. An RTL model checker based on the proposed algorithm is implemented and it is shown that it can determine whether the designs for medium-size sequential machines allow them to satisfy their specifications in a reasonable time and space.

Due to the progress of VLSI technologies, logic circuits have become more complex. As a result, the possibilities of design errors have increased. Logic design verification, therefore, has become more important as a means of guaranteeing the correctness of logic design. Logic design verification requires mathematical logic with enough expressive power to describe the behavior of logic circuits. While propositional logic is known to be equivalent to combinatorial logic circuits, a class of mathematical logic that corresponds to sequential machines and/or finite automata has not yet been clarified. This paper introduces various types of Regular Temporal Logic (RTL), which is expressively equivalent to finite automata and can express the notion of time explicitly. A design verification algorithm for sequential machines based on a model-checking method of the RTL is also given. Although the complexity of the model-checking problem of the RTL is non-elementary, the proposed model-checking algorithm is efficient and still runs in a time proportional to the size of the structure models. An RTL model checker based on the proposed algorithm is implemented, and it is shown that it can determine whether the designs for medium-size sequential machines allow them to satisfy their specifications in a reasonable time and space.

Journal

Details 詳細情報について

Report a problem

Back to top