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

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.