IEICE TRANSACTIONS on Fundamentals
Formal Design Verification of Sequential Machines Based on Symbolic Model Checking for Branching Time Regular Temporal Logic
Summary :
Recently, Burch et al. proposed symbolic model checking method to verify sequential machines formally. The method, which is based on logic function manipulation using binary decision diagram, can handle large sequential machines that cannot be handled by the conventional techniques. The expressive power of Computational Tree Logic (CTL), which was used by Burch et al., is not very powerful, for example, CTL cannot describe repetition of events. This papers shows an extension of the symbolic model checking algorithm to Branching time regular temporal logic (BRTL), which has been proposed by the authors as an improvement of CTL in terms of expressive power. The implemented verifier based on the proposed algorithm could verify behaviors of a microprocessor composed of approximately 1,600 gates and 68 flipflops.
- Publication
- IEICE TRANSACTIONS on Fundamentals Vol.E75-A No.10 pp.1220-1229
- Publication Date
- 1992/10/25
- Publicized
- Online ISSN
- DOI
- Type of Manuscript
- Special Section PAPER (Special Section on VLSI Design and CAD Algorithms)
- Category
Authors
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Kiyoharu HAMAGUCHI, Hiromi HIRAISHI, Shuzo YAJIMA, "Formal Design Verification of Sequential Machines Based on Symbolic Model Checking for Branching Time Regular Temporal Logic" in IEICE TRANSACTIONS on Fundamentals,
vol. E75-A, no. 10, pp. 1220-1229, October 1992, doi: .
Abstract: Recently, Burch et al. proposed symbolic model checking method to verify sequential machines formally. The method, which is based on logic function manipulation using binary decision diagram, can handle large sequential machines that cannot be handled by the conventional techniques. The expressive power of Computational Tree Logic (CTL), which was used by Burch et al., is not very powerful, for example, CTL cannot describe repetition of events. This papers shows an extension of the symbolic model checking algorithm to Branching time regular temporal logic (BRTL), which has been proposed by the authors as an improvement of CTL in terms of expressive power. The implemented verifier based on the proposed algorithm could verify behaviors of a microprocessor composed of approximately 1,600 gates and 68 flipflops.
URL: https://global.ieice.org/en_transactions/fundamentals/10.1587/e75-a_10_1220/_p
Copy
@ARTICLE{e75-a_10_1220,
author={Kiyoharu HAMAGUCHI, Hiromi HIRAISHI, Shuzo YAJIMA, },
journal={IEICE TRANSACTIONS on Fundamentals},
title={Formal Design Verification of Sequential Machines Based on Symbolic Model Checking for Branching Time Regular Temporal Logic},
year={1992},
volume={E75-A},
number={10},
pages={1220-1229},
abstract={Recently, Burch et al. proposed symbolic model checking method to verify sequential machines formally. The method, which is based on logic function manipulation using binary decision diagram, can handle large sequential machines that cannot be handled by the conventional techniques. The expressive power of Computational Tree Logic (CTL), which was used by Burch et al., is not very powerful, for example, CTL cannot describe repetition of events. This papers shows an extension of the symbolic model checking algorithm to Branching time regular temporal logic (BRTL), which has been proposed by the authors as an improvement of CTL in terms of expressive power. The implemented verifier based on the proposed algorithm could verify behaviors of a microprocessor composed of approximately 1,600 gates and 68 flipflops.},
keywords={},
doi={},
ISSN={},
month={October},}
Copy
TY - JOUR
TI - Formal Design Verification of Sequential Machines Based on Symbolic Model Checking for Branching Time Regular Temporal Logic
T2 - IEICE TRANSACTIONS on Fundamentals
SP - 1220
EP - 1229
AU - Kiyoharu HAMAGUCHI
AU - Hiromi HIRAISHI
AU - Shuzo YAJIMA
PY - 1992
DO -
JO - IEICE TRANSACTIONS on Fundamentals
SN -
VL - E75-A
IS - 10
JA - IEICE TRANSACTIONS on Fundamentals
Y1 - October 1992
AB - Recently, Burch et al. proposed symbolic model checking method to verify sequential machines formally. The method, which is based on logic function manipulation using binary decision diagram, can handle large sequential machines that cannot be handled by the conventional techniques. The expressive power of Computational Tree Logic (CTL), which was used by Burch et al., is not very powerful, for example, CTL cannot describe repetition of events. This papers shows an extension of the symbolic model checking algorithm to Branching time regular temporal logic (BRTL), which has been proposed by the authors as an improvement of CTL in terms of expressive power. The implemented verifier based on the proposed algorithm could verify behaviors of a microprocessor composed of approximately 1,600 gates and 68 flipflops.
ER -
English
