Description and verification of input constraints and input‐output specifications of logic circuits

The input constraints and the input‐output specifications of the logic circuit are assertions to be satisfied in the operation of the logic circuit. Most of the timing constraints such as the set‐up time of the clocked flip‐flop can be regarded as the input constraint or the input‐output specification. In this paper, the time is considered as discrete with sufficiently small steps, and the input and output of the logic circuit are treated as sequences. The method to describe the set of sequences satisfying the input constraints or the input‐output specifications and the method to verify these assertions are proposed anew; # expression and the first # form are proposed as the description methods. The # expression is obtained by adding the newly proposed # concatenation and # closure to the regular expression. The first # form is a restricted # expression, where the number of states of the deterministic finite automaton accepting the set of sequences represented by the expression does not exceed twice the length of the description. In this paper, the logic circuit is regarded as a converter for the set of sequences and the verification of the input constraint or the input‐output specification is reduced to the examination of the inclusive relation among the sets of sequences. Consequently, when the set of sequences satisfying the input constraint or the input‐output specification is described in the first # form, the verification can be performed efficiently. The proposed method is applied to several actual problems, and is shown to be useful.