TY - JOUR

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

AU - Kimura, Shinji

AU - Yajima, Shuzo

PY - 1987

Y1 - 1987

N2 - 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.

AB - 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.

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

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

U2 - 10.1002/scj.4690180204

DO - 10.1002/scj.4690180204

M3 - Article

AN - SCOPUS:0023294917

VL - 18

SP - 29

EP - 42

JO - Systems and Computers in Japan

JF - Systems and Computers in Japan

SN - 0882-1666

IS - 2

ER -