Coverage metrics for temporal logic model checking*

R. Armoni, L. Fix, A. Flaisher, O. Grumberg, N. Piterman, A. Tiemeyer, and M.Y. Vardi, “Enhanced vacuity detection in linear temporal logic,” in Proceedings of 15th International Conference in Computer Aided Verification (CAV), vol. 2725 of Lecture Notes in Computer Science, Springer, 2003. pp. 368–380.

D. Beaty and R. Bryant, “Formally verifying a microprocessor using a simulation methodology,” in Proc. 31st Design Automation Conference, IEEE Computer Society, 1994, pp. 596–602.

I. Beer, S. Ben-David, C. Eisner, and Y. Rodeh, “Efficient detection of vacuity in ACTL formulas,” Form. Meth. in Sys. Des., Vol. 18, No. 2, pp. 141–163, 2001.

J.P. Bergmann and M.A. Horowitz, “Improving coverage analysis and test generation for large designs,” In IEEE International Conference for Computer-Aided Design, Nov. 1999, pp. 580–584.

D. Bustan, A. Flaisher, O. Grumberg, O. Kupferman, and M.Y. Vardi, “Regular vacuity,” in 13th Advanced Research Working Conference on Correct Hardware Design and Verification Methods, volume 3725 of Lecture Notes in Computer Science, Springer-Verlag, 2005, pp. 191–206.

K.-T. Cheng and A. Krishnakumar, “Automatic functional test generation using the extended finite state machine model,” in Proceedings of 30th Design Automation Conference, June 1993, pp. 86–91.

H. Chockler, O. Kupferman, and M.Y. Vardi, “Coverage metrics for formal verification. charme 2003: 111–125,” in Proceedings of 12th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME), number 2860 in Lecture Notes in Computer Science, Springer-Verlag, 2003, pp. 111–125.

E.M. Clarke and E.A. Emerson, “Design and synthesis of synchronization skeletons using branching time temporal logic,” in Proc. Workshop on Logic of Programs, vol. 131 of Lecture Notes in Computer Science, Springer-Verlag, 1981, pp. 52–71.

E.M. Clarke, O. Grumberg, and D.E. Long, “Model checking and abstraction,” in Proc. 19th ACM Symp. on Principles of Programming Languages, Albuquerque, New Mexico, Jan. 1992, pp. 343–354.

E.M. Clarke, O. Grumberg, K.L. McMillan, and X. Zhao, “Efficient generation of counterexamples and witnesses in symbolic model checking,” in Proc. 32nd Design Automation Conference, IEEE Computer Society, 1995, pp. 427–432.

E.M. Clarke, O. Grumberg, and D. Peled, Model Checking. MIT Press, 1999.

S. Devadas, A. Ghosh, and K. Keutzer, “An observability-based code coverage metric for functional simulation,” in Proceedings of the International Conference on Computer-Aided Design, Nov. 1996, pp. 418–425.

E.A. Emerson, “Temporal and modal logic,” Handbook of Theoretical Computer Science, 1990, pp. 997–1072.

F. Fallah, P. Ashar, and S. Devadas, “Simulation vector generation from hdl descriptions for observability enhanced-statement coverage,” in Proceedings of the 36th Design Automation Conference, June 1999, pp. 666–671.

F. Fallah, S. Devadas, and K. Keutzer, “OCCOM: Efficient computation of observability-based code coverage metrics for functional simulation,“ in Proceedings of the 35th Design Automation Conference, June 1998, pp. 152–157.

G.D. Hachtel and F. Somenzi, Logic Synthesis and Verification Algorithms. Kluwer Academic Publishers, Norwell, Massachusetts, 1996.

D. Harel and A. Pnueli, “On the development of reactive systems,” in K. Apt (Ed.) Logics and Models of Concurrent Systems, vol. F-13 of NATO Advanced Summer Institutes, Springer-Verlag, 1985, pp. 477–498.

R.C. Ho and M.A. Horowitz, “Validation coverage analysis for complex digital designs,” in International Conference on Computer Aided Design, Nov. 1996, pp. 146–151.

R. Ho, C. Yang, M. Horowitz, and D. Dill, “Architecture validation for processors,” in Proceedings of the 22nd Annual Symp. on Computer Architecture, June 1995, pp. 404–413.

C.A.R. Hoare, Communicating Sequential Processes. Prentice-Hall, 1985.

Y. Hoskote, T. Kam, P.-H Ho, and X. Zhao, “Coverage estimation for symbolic model checking,” in Proc. 36th Design automation conference, 1999, pp. 300–305.

Y. Hoskote, D. Moundanos, and J. Abraham, “Automatic extraction of the control flow machine and application to evaluating coverage of verification vectors,” in Proceedings of ICDD, Oct. 1995, pp. 532–537.

N. Jayakumar, M. Purandare, and F. Somenzi, “Dos and don'ts of ctl state coverage estimation,” in Proc. 40th Design Automation Conference (DAC), IEEE Computer Society, 2003.

M. Kantrowitz and L. Noack, “I'm done simulating: Now what? verification coverage analysis and correctness checking of the dec chip 21164 alpha microprocessor,” in Proceedings of Design Automation Conference, June 1996, pp. 325–330.

S. Katz, D. Geist, and O. Grumberg, “Have I written enough properties ?” A method of comparison between specification and implementation,” in 10th Advanced Research Working Conference on Correct Hardware Design and Verification Methods, Lecture Notes in Computer Science. Springer-Verlag, 1999.

O. Kupferman and M.Y. Vardi, “Vacuity detection in temporal model checking,” International Journal on Software Tools for Technology Transfer (STTT), Vol. 4, No. 2, pp. 224–233, 2003.

O. Kupferman, M.Y. Vardi, and P. Wolper, “An automata-theoretic approach to branching-time model checking,” J. ACM, Vol. 47, No. 2, pp. 312–360, March 2000.

R.P. Kurshan, FormalCheck User's Manual. Cadence Design, Inc., 1998.

O. Lichtenstein and A. Pnueli, “Checking that finite state concurrent programs satisfy their linear specification,” in Proc. 12th ACM Symp. on Principles of Programming Languages, New Orleans, Jan. 1985, pp. 97–107.

Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, Berlin, Jan. 1992.

D. Moumdanos, J.A. Abraham, and Y.V. Hoskote, “Abstraction techniques for validation coverage analysis and test generation,” IEEE Trans. Comp., Jan. 1998.

R.G. Nigmatulin, The Complexity of Boolean Functions. Nauka, Main Editorial Board for Physical and Mathematical Literature, Moscow, 1990.

M. Purandare and F. Somenzi, “Vacuum cleaning ctl formulae,” in Proceedings of 14th International Conference in Computer Aided Verification (CAV), Lecture Notes in Computer Science, Springer, 2002. pp. 485–499.

J.P. Queille and J. Sifakis, “Specification and verification of concurrent systems in Cesar,” in Proc. 5th International Symp. on Programming, vol. 137 of Lecture Notes in Computer Science, Springer-Verlag, 1981. pp. 337–351.

I. Wegener, The Complexity of Boolean Functions. John Wiley & Sons, Chichester, 1987.