Abstract
State-space explosion remains to be a significant challenge for Finite State Machine (FSM) exploration techniques in model checking and sequential verification. In this work, we study the use of sequential ATPG (Automatic Test- Pattern Generation) as a solution to overcome the problem for a useful class of temporal logic properties. We also develop techniques to exploit the existence of synchronizing sequences to reduce some temporal logic properties to simpler properties that can be efficiently checked using an ATPG algorithm. We show that the method has the potential to scale up to large, industrial-strength, hardware designs for which current model checking techniques fail.
Chapter PDF
Similar content being viewed by others
References
M. Abramovici, M. A. Breuer, and A. D. Friedman. Digital System Testing and Testable Design. NewYork, NY: Computer Science Press, 1990.
R. Alur and T. A. Henzinger, editors. Computer-Aided Verification, CAV’ 96, volume 1102 of Lecture Notes in Computer Science, New Brunswick, NJ, July/August 1996. Springer-Verlag.
V. Boppana. State information-based solutions for sequential circuit diagnosis and testing. Technical Report CRHC-97-20, Ph.D. thesis, Center for Reliable and High-Performance Computing, University of Illinois at Urbana-Champaign, July 1997.
R.E. Bryant. Binary decision diagrams and beyond: Enabling technologies for formal verification. In Proceedings of the International Conference on Computer-Aided Design, pages 236–243, November 1995.
K. T. Cheng and V. Agrawal. State Assignment for Initialilzable Synthesis. In Proc. Intl. Conf. Computer-Aided Design, pages 212–215, November 1989.
K. T. Cheng and V. Agrawal. Initializability consideration in sequential machine synthesis. IEEE Trans. Computers, 41(3):374–379, March 1993.
E. Clarke, O. Grumberg, and D. Long. Verification tools for finite-state concurrent systems. In A Decade of concurrency-Reflections and Perspectives, volume 803 of Lecture Notes in Computer Science. Springer-Verlag, 1994.
K. T. Cheng and H. K. T. Ma. On the over-specification problem in sequentialATPG algorithms. In Proc. Design Automation Conf., pages 16–21, June 1992.
K. T. Cheng and H. K. T. Ma. On the over-specification problem in sequentialATPG algorithms. IEEE Trans. Computer-Aided Design, 12(10):1599–1604, October 1993.
M. Fujita, H. Tanaka, and T. Moto-oka. Verification with prolog and temporal logic. In Proc. of IFIP WG10.2 International Conference on Hardware Description Languages and their Applications, May 1983.
M. Fujita, H. Tanaka, and T. Moto-oka. Logic design assistance with temporal logic. In Proc. of IFIP WG10.2 International Conference on Hardware Description Languages and their Applications, Aug. 1985.
P. Goel. An implicit enumeration algorithm to generate tests for combinational logic circuits. IEEE Trans. Computers, C-30(3):215–222, March 1990.
The VIS Group. VIS:A system for verification and synthesis. In Alur and Henzinger [AH96], pages 428–432.
F. C. Hennie. Finite-State Models for Logical Machines. NewYork, NY: JohnWiley & Sons, Inc., 1968.
M. S. Hsiao, E. M. Rudnick, and J. H. Patel. Sequential circuit test generation using dynamic state traversal. In Proc. European Design and Test Conf., pages 22–28, March 1997.
H. Iwashita and T. Nakata. Forward model checking techniques oriented to buggy designs. In Proc. Intl. Conf. Computer-Aided Design, pages 400–404, November 1997.
H. Iwashita, T. Nakata, and F. Hirose. Ctl model checking based on forward state traversal. In Proc. Intl. Conf. Computer-Aided Design, pages 82–87, November 1996.
Z. Kohavi. Switching and Finite Automata Theory. New York, NY: McGraw-Hill, 1978.
R. P. Kurshan. Computer-Aided Verification of Coordinating Processes-The Automata-Theoretic Approach. Princeton University Press, Princeton, NJ, 1994.
O. Kupferman and MosheY. Vardi. Model checking of safety properties. In CAV99, 1999.
Kenneth L. McMillan. Symbolic Model Checking. Kluwer Academic Pub., Boston, MA, 1993.
H. Nakamura, M. Fujita, S. Kono, and H. Tanaka. Temporal logic based fast verification systems using cover expressions. In Proc. of IFIP WG10.5 International Conference on VLSI, Aug. 1987.
T. Niermann and J. H. Patel. HITEC:A test generation package for sequential circuits. In Proc. European Design Automation Conf., pages 214–218, February 1991.
[ORR+96]_ S. Owre, S. Rajan, J.M. Rushby, N. Shankar, and M.K. Srivas. PVS: Combining specification, proof checking, and model checking. In Alur and Henzinger [AH96], pages 411–414.
Doron Peled. Combining partial order reductions with on-the-fly model-checking. Formal Methods in System Design, 8(1):39–64, 1996.
I. Pomeranz and S. M. Reddy. The multiple observation time test strategy. IEEE Trans. Computer-Aided Design, 40(5):627–637, May 1992.
I. Pomeranz and S. M. Reddy. Classification of faults in synchronous sequential circuits. IEEE Trans. Computers, 42(9):1066–1077, September 1993.
K. Takayama, T. Satoh, T. Nakata, and F. Hirose. An approach to verify a large scale system-on-a-chip using symbolic model checking. In Proceedings of the International Conference on Computer Design, pages 308–313, October 1998.
P. Wolper. “synthesis of communicating processes from temporal logic specifications”. Technical Report STAN-CS-82-925, Dept. of Computer Science, Stanford University, 1982.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Boppana, V., Rajan, S.P., Takayama, K., Fujita, M. (1999). Model Checking Based on Sequential ATPG. In: Halbwachs, N., Peled, D. (eds) Computer Aided Verification. CAV 1999. Lecture Notes in Computer Science, vol 1633. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48683-6_36
Download citation
DOI: https://doi.org/10.1007/3-540-48683-6_36
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66202-0
Online ISBN: 978-3-540-48683-1
eBook Packages: Springer Book Archive