@article{oai:ipsj.ixsq.nii.ac.jp:00014061,
 author = {Naoyuki, Yamada and Yoshikatsu, Ueda and Junko, Ito and Tomoharu, Nakamura and Junichi, Yoshizawa and Satoshi, Matsuda and Naoyuki, Yamada and Yoshikatsu, Ueda and Junko, Ito and Tomoharu, Nakamura and Junichi, Yoshizawa and Satoshi, Matsuda},
 issue = {12},
 journal = {情報処理学会論文誌},
 month = {Dec},
 note = {A design verification method for sequential control circuits with timing coordination has been developed. Unlike prevailing numeric simulations  this method is based on a theorem-proving technique. Sequential control circuits realize their target functions by coordinating the asyn-chronously inputted signals. In order to verify timing coordination efnciently  the control strategy which combines hyperresolution and a connection graph method with attached procedures for handling time variables symbolically has been developed. This method facilitates not only the verification of timing coordination but also the extraction of intended behavlours from proposed designs. The developed method was applied to verificatlon of an auto-reclosing circuit in an electric power substatlon which contains about 40 components. The verification for each specification was executed correctly In about I minute on a mainframe computer. The developed verification method was judged to be useful and efficient for practical use., A design verification method for sequential control circuits with timing coordination has been developed. Unlike prevailing numeric simulations, this method is based on a theorem-proving technique. Sequential control circuits realize their target functions by coordinating the asyn-chronously inputted signals. In order to verify timing coordination efnciently, the control strategy which combines hyperresolution and a connection graph method with attached procedures for handling time variables symbolically has been developed. This method facilitates not only the verification of timing coordination but also the extraction of intended behavlours from proposed designs. The developed method was applied to verificatlon of an auto-reclosing circuit in an electric power substatlon which contains about 40 components. The verification for each specification was executed correctly In about I minute on a mainframe computer. The developed verification method was judged to be useful and efficient for practical use.},
 pages = {2774--2784},
 title = {Design Verification Based on Theorem - Proving Technique for Sequential Control Circuits with Timing Coordination},
 volume = {35},
 year = {1994}
}