Regular Temporal Logic Expressively Equivalent to Finite Automata and Its Application to Logic Design Verification
Access this Article
Search this Article
Author(s)
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 modelchecking method of the RTL is also given. Although the complexity of the modelchecking problem of the RTL is nonelementary the proposed modelchecking 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 mediumsize 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 modelchecking method of the RTL is also given. Although the complexity of the modelchecking problem of the RTL is nonelementary, the proposed modelchecking 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 mediumsize 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 modelchecking method of the RTL is also given. Although the complexity of the modelchecking problem of the RTL is nonelementary, the proposed modelchecking 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 mediumsize sequential machines allow them to satisfy their specifications in a reasonable time and space.
Journal

 Journal of Information Processing

Journal of Information Processing 15(1), 129138, 19920331
Information Processing Society of Japan (IPSJ)