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
DOIs
Publication statusPublished - Nov 1996

Keywords

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

ASJC Scopus subject areas

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

Fingerprint Dive into the research topics of 'Timing verification of asynchronous sequential circuits with specifications - A method of reducing state transitions to be verified in detail'. Together they form a unique fingerprint.

  • Cite this