2026-06-05T23:21:38Z https://ipsj.ixsq.nii.ac.jp/oai

oai:ipsj.ixsq.nii.ac.jp:00014061 2025-01-23T00:58:45Z 581:768:769

ハードウェア設計 Design Verification Based on Theorem - Proving Technique for Sequential Control Circuits with Timing Coordination Design Verification Based on Theorem - Proving Technique for Sequential Control Circuits with Timing Coordination Naoyuki, Yamada Yoshikatsu, Ueda Junko, Ito Tomoharu, Nakamura Junichi, Yoshizawa Satoshi, Matsuda Naoyuki, Yamada Yoshikatsu, Ueda Junko, Ito Tomoharu, Nakamura Junichi, Yoshizawa Satoshi, Matsuda 論文 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. journal article 1994-12-15 application/pdf 情報処理学会論文誌 12 35 2774 2784 1882-7764 AN00116647 https://ipsj.ixsq.nii.ac.jp/record/14061/files/IPSJ-JNL3512025.pdf eng