Abstract
Arithmetic operations on integers are very expensive to represent in formalisms that most automatic formal verification tools use. To deal with this problem, a verification methodology is proposed where systems that include such operations are simplified before they are verified. The simplifications are classified either as abstractions (ensuring that the original system satisfies all the properties satisfied by the simplified system, but not vice versa), reductions (the simplified system preserves exactly all the properties of the original one), and restrictions (the simplified system has the same properties as the original, provided certain constraints on the state variables are satisfied). In the proposed methodology, systems are simplified automatically, as instructed by the designer. The simplifications preserve the structure of the system, and can be performed in time and space that depends only on the size of the simplified system.
Chapter PDF
Similar content being viewed by others
References
Felice Balarin and Alberto L. Sangiovanni-Vincentelli. An iterative approach to languagecontainment. In Costas Courcoubetis, editor, Proceedings of Computer Aided Verification: 5th International Conference, CAV’93, Elounda, Greece, June/July 1993, pages 29–40. Springer-Verlag, 1993. LNCS vol. 697.
Felice Balarin, Harry Hsieh, Attila Jurecska, Luciano Lavagno, and Alberto SangiovanniVincentelli. Formal verification of embedded systems based on CFSM networks. In Proceedings of the 33th ACM/IEEE Design Automation Conference, June 1996.
R.K. Brayton, A. Sangiovanni-Vincentelli, G.D. Hachtel, F. Somenzi, A. Aziz, S.-T. Cheng, S. Edwards, S. Khatri, Y. Kukimoto, S. Qadeer, R.K. Ranjan, T.R. Shiple, G. Swamy, T. Villa, A. Pardo, and S. Sarwary. VIS: A system for verification and synthesis. In Rajeev Alur and Thomas A. Henzinger, editorsProceedings of Computer Aided Verification: 8th International Conference CAV’96 Rutgers NJ July 1996. Springer-Verlag, 1996. LNCS vol. 1102.
Massimiliano Chiodo, Paolo Giusto, Harry Hsieh, Attila Jurecska, Luciano Lavagno, and Alberto Sangiovanni-Vincentelli. A formal specification model for hardware/software codesign. In Proceedings of the International Workshop on Hardware-Software Codesign, 1993.
Massimiliano Chiodo, Paolo Giusto, Harry Hsieh, Attila Jurecska, Luciano Lavagno, and Alberto Sangiovanni-Vincentelli. A formal methodology for hardware/software codesign of embedded systems. IEEE Micro, August 1994.
M. Chiodo, P. Giusto, H. Hsieh, A. Jurecska, L. Lavagno, K. Suzuki, S. Yee, and A. Sangiovanni-Vincentelli. A case study in computer-aided codesign of embedded controllers. Design Automation for Embedded Systems, 1 (1–2): 51–67, January 1996.
Edmund M. Clarke, Orna Grumberg, and David E. Long. Model checking and abstraction. In Proc. Principles of Programming Languages, January 1992.
C. Consel and O. Danvy. Tutorial notes on partial evaluation. In Proc. 20th Ann. ACM Symp. on Principles of Prog. Lang.,pages 493–501. 1993.
P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction of approximation of fixpoints. In Proc. nth Ann. ACM Symp. on Principles of Prog. Lang. 1977.
S. Graf and C. Loiseaux. A tool for symbolic program verification and abstraction. InCostas Courcoubetis, editorComputer Aided Verification: 5th International Conference, CAV’93, Elounda, Greece, June/July 1993 Proceedingspages 71–84. Springer-Verlag, 1993. LNCS vol. 697.
J.E. Hoperoft and J.D. Ullman. Introduction to Automata Theory, Languages and Computation. Addison Wesley, 1979.
Robert P. Kurshan. Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, 1994.
Kenneth L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.
Thomas R. Shiple, Massimiliano Chiodo, Alberto L. Sangiovanni-Vincentelli, and Robert K. Brayton. Automatic reduction in CTL compositional model checking. In Proc. Fourth Workshop on Computer-Aided Verification,pages 225–238, Montreal, June 1992. Also appeared in Lecture Notes in Computer Science, vol. 663.
P. Wolper. Expressing interesting properties of programs in propositional temporal logic. In Proc. 13th Ann. ACM Symp. on Principles of Prog. Lang. January 1986.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1997 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Balarin, F., Sajid, K. (1997). Simplifying Data Operations for Formal Verification. In: Kloos, C.D., Cerny, E. (eds) Hardware Description Languages and their Applications. IFIP — The International Federation for Information Processing. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35064-6_3
Download citation
DOI: https://doi.org/10.1007/978-0-387-35064-6_3
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-5387-5
Online ISBN: 978-0-387-35064-6
eBook Packages: Springer Book Archive