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

Access this Article

Search this Article

Author(s)

    • Hiromi Hiraishi
    • Department of Information and Communication Sciences, Faculty of Engineering, Kyoto Sangyo University
    • Hiroshi Fujii
    • Information and Communication Processing Research Laboratory, NTT.
    • Shuzo Yajima
    • Department of Information Science, Facu1ty of Engineering, Kyoto University

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.

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

  • Journal of Information Processing

    Journal of Information Processing 15(1), 129-138, 1992-03-31

    Information Processing Society of Japan (IPSJ)

Codes

  • NII Article ID (NAID)
    110002673621
  • NII NACSIS-CAT ID (NCID)
    AA00700121
  • Text Lang
    ENG
  • Article Type
    Article
  • ISSN
    1882-6652
  • Data Source
    NII-ELS  IPSJ 
Page Top