Timing verification of asynchronous sequential circuits with specifications - A method of reducing state transitions to be verified in detail

Atsuchi Ohnishi, Yuji Sugiyama, Takuji Okamoto

Research output: Contribution to journalArticle

Abstract

One of the important issues in the asynchronous sequential circuit is to verify that the state transitions as stated in the specification occur even if there is a delay variation in the element. When the exiting timing verification method is applied to this problem, however, the transient and other states must be examined, which requires an exponentially long time in the verification. This paper presents a formal procedure based on the circuit structure and the relation between the specification and the circuit, where the state transition to induce the transition in the specification is determined and the state transition to be verified in detail is restricted without generating the transient and other states. First, the time-invariant input values and state variable values are considered, and a sufficient condition is given for the above restriction. The sufficient condition ensures that the state transition occurs as is stated in the specification, independently of the element delay. A decision procedure for the sufficient condition is presented, and the time complexity is examined. It is shown that the proposed method is useful in reducing the verification time compared to the existing verification method. The sufficient condition is applied to sample circuits, and it is shown that the detailed verification can be omitted by the factor of 16/17 for the ring arbiter, and 20/24 for the D flip-flop. Thus, it is expected that the time for the verification can be reduced greatly by the proposed method.

Original languageEnglish
Pages (from-to)53-63
Number of pages11
JournalSystems and Computers in Japan
Volume27
Issue number11
Publication statusPublished - Nov 1996

Fingerprint

Sequential circuits
State Transition
Timing
Specification
Specifications
Sufficient Conditions
Networks (circuits)
Flip flop circuits
Decision Procedures
Flip
Time Complexity
Verify
Restriction
Ring
Invariant

Keywords

  • Asynchronous circuit
  • Design process
  • Specification
  • State transition
  • Timing verification

ASJC Scopus subject areas

  • Computational Theory and Mathematics
  • Hardware and Architecture
  • Information Systems
  • Theoretical Computer Science

Cite this

Timing verification of asynchronous sequential circuits with specifications - A method of reducing state transitions to be verified in detail. / Ohnishi, Atsuchi; Sugiyama, Yuji; Okamoto, Takuji.

In: Systems and Computers in Japan, Vol. 27, No. 11, 11.1996, p. 53-63.

Research output: Contribution to journalArticle

@article{500701f511b4465a88380fa33182ba0a,
title = "Timing verification of asynchronous sequential circuits with specifications - A method of reducing state transitions to be verified in detail",
abstract = "One of the important issues in the asynchronous sequential circuit is to verify that the state transitions as stated in the specification occur even if there is a delay variation in the element. When the exiting timing verification method is applied to this problem, however, the transient and other states must be examined, which requires an exponentially long time in the verification. This paper presents a formal procedure based on the circuit structure and the relation between the specification and the circuit, where the state transition to induce the transition in the specification is determined and the state transition to be verified in detail is restricted without generating the transient and other states. First, the time-invariant input values and state variable values are considered, and a sufficient condition is given for the above restriction. The sufficient condition ensures that the state transition occurs as is stated in the specification, independently of the element delay. A decision procedure for the sufficient condition is presented, and the time complexity is examined. It is shown that the proposed method is useful in reducing the verification time compared to the existing verification method. The sufficient condition is applied to sample circuits, and it is shown that the detailed verification can be omitted by the factor of 16/17 for the ring arbiter, and 20/24 for the D flip-flop. Thus, it is expected that the time for the verification can be reduced greatly by the proposed method.",
keywords = "Asynchronous circuit, Design process, Specification, State transition, Timing verification",
author = "Atsuchi Ohnishi and Yuji Sugiyama and Takuji Okamoto",
year = "1996",
month = "11",
language = "English",
volume = "27",
pages = "53--63",
journal = "Systems and Computers in Japan",
issn = "0882-1666",
publisher = "John Wiley and Sons Inc.",
number = "11",

}

TY - JOUR

T1 - Timing verification of asynchronous sequential circuits with specifications - A method of reducing state transitions to be verified in detail

AU - Ohnishi, Atsuchi

AU - Sugiyama, Yuji

AU - Okamoto, Takuji

PY - 1996/11

Y1 - 1996/11

N2 - One of the important issues in the asynchronous sequential circuit is to verify that the state transitions as stated in the specification occur even if there is a delay variation in the element. When the exiting timing verification method is applied to this problem, however, the transient and other states must be examined, which requires an exponentially long time in the verification. This paper presents a formal procedure based on the circuit structure and the relation between the specification and the circuit, where the state transition to induce the transition in the specification is determined and the state transition to be verified in detail is restricted without generating the transient and other states. First, the time-invariant input values and state variable values are considered, and a sufficient condition is given for the above restriction. The sufficient condition ensures that the state transition occurs as is stated in the specification, independently of the element delay. A decision procedure for the sufficient condition is presented, and the time complexity is examined. It is shown that the proposed method is useful in reducing the verification time compared to the existing verification method. The sufficient condition is applied to sample circuits, and it is shown that the detailed verification can be omitted by the factor of 16/17 for the ring arbiter, and 20/24 for the D flip-flop. Thus, it is expected that the time for the verification can be reduced greatly by the proposed method.

AB - One of the important issues in the asynchronous sequential circuit is to verify that the state transitions as stated in the specification occur even if there is a delay variation in the element. When the exiting timing verification method is applied to this problem, however, the transient and other states must be examined, which requires an exponentially long time in the verification. This paper presents a formal procedure based on the circuit structure and the relation between the specification and the circuit, where the state transition to induce the transition in the specification is determined and the state transition to be verified in detail is restricted without generating the transient and other states. First, the time-invariant input values and state variable values are considered, and a sufficient condition is given for the above restriction. The sufficient condition ensures that the state transition occurs as is stated in the specification, independently of the element delay. A decision procedure for the sufficient condition is presented, and the time complexity is examined. It is shown that the proposed method is useful in reducing the verification time compared to the existing verification method. The sufficient condition is applied to sample circuits, and it is shown that the detailed verification can be omitted by the factor of 16/17 for the ring arbiter, and 20/24 for the D flip-flop. Thus, it is expected that the time for the verification can be reduced greatly by the proposed method.

KW - Asynchronous circuit

KW - Design process

KW - Specification

KW - State transition

KW - Timing verification

UR - http://www.scopus.com/inward/record.url?scp=0030289604&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0030289604&partnerID=8YFLogxK

M3 - Article

VL - 27

SP - 53

EP - 63

JO - Systems and Computers in Japan

JF - Systems and Computers in Japan

SN - 0882-1666

IS - 11

ER -