Abstract
Design optimization exploration is a key element in finding an optimal resource utilization. The exploration process applies optimizations iteratively; after applying each optimization, the result has to be validated. The research challenge for formal verification is to develop an efficient design validation flow and increase the quality of the validation. In this paper, we propose an automated validation flow to check the functional equivalence of the source design and its optimized version. This approach is based on a symbolic simulation technique to obtain the design properties and automatically check them using an equivalence checker. The novelty of this approach includes the use of model simplification techniques, such as if-conversion and loop-conversion, and state encoding to ease validation analysis.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Borrione, D., Georgelin, P., Rodrigues, V.: Using Macros to Mimic VHDL. In: Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Publishers, Dordrecht (2000)
Canon, http://www.canon.co.uk
Cupak, M., Catthoor, F.: Verification of Loop Tranformations for Complex Data Dominated Applications. In: High Level Design Validation and Test, La Jolla, California, November 1998, pp. 72–79 (1998)
Dave, M.A.: Compiler verification: a bibliography. ACM SIGSOFT Software Engineering Notes 28(6) (November 2003)
Dutertre, B., Moura, L.: System Description: Yices 1.0, SRI International (2006)
hArtes, http://www.hartes.org
Hoare, C.A.R., He, J., Sampaio, A.: Normal form approach to compiler design. ACTA informatica 30(8), 701–739 (1993)
Krishnamurthy, N., Abadir, M.S., Martin, A.K., Abraham, J.A.: Design and Development Paradigm for Industrial Formal Verification CAD Tools. IEEE Design and Test of Computers 18(4), 26–35 (2001)
Kurshan, R.P.: Formal Verification in a Commercial Setting. In: Proc. Design Automation Conference, Anaheim, pp. 258–262 (1997)
Lerner, S., Millstein, T., Chambers, C.: Automatically Proving the Correctness of Compiler Optimisations. In: Proc. Programming Language Design and Implementation, SanDiego, California (June 2003)
Tristan, J.B., Leroy, X.: Formal verification of translation validators: A case study on instruction scheduling optimizations. In: Proc. 35th symposium Principles of Programming Languages, January 2008, pp. 17–27 (2008)
Moore, J.S.: Symbolic Simulation: An ACL2 Approach. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol. 1522, pp. 334–350. Springer, Heidelberg (1998)
Necula, G.C.: Translation Validation for an Optimizing Compiler. In: Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation, Vancouver, British Columbia (June 2000)
Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs. In: Horspool, R.N. (ed.) CC 2002. LNCS, vol. 2304, p. 213. Springer, Heidelberg (2002)
Oliveira, M., Woodcock, J.: Automatic generation of verified concurrent hardware. In: Butler, M., Hinchey, M.G., Larrondo-Petrie, M.M. (eds.) ICFEM 2007. LNCS, vol. 4789, pp. 286–306. Springer, Heidelberg (2007)
Perna, J.I., Woodcock, J.: A Denotational Semantics for Handel-C Hardware Compilation. In: Butler, M., Hinchey, M.G., Larrondo-Petrie, M.M. (eds.) ICFEM 2007. LNCS, vol. 4789, pp. 266–285. Springer, Heidelberg (2007)
Saito, H., Ogawa, T., Sakunkonchack, T., Fujita, M., Nanya, T.: An Equivalence Checking Methodology for Hardware Oriented C-based Specifications. In: Proc. High-Level Design Validation and Test Workshop, October 2002, pp. 139–144 (2002)
Singh, S., Lillieroth, C.J.: Formal Verification of Reconfigurable Cores. In: Proc. Field-Programmable Custom Computing Machines, Napa Valley, California, pp. 25–32 (1999)
Siegel, S.F., Mironova, A., Avrunin, G.S., Clarke, L.A.: Using Model Checking with Symbolic Execution to Verify Parallel Numerical Programs. In: Proc. International Symposium on Software Testing and Analysis, Portland (2006)
Susanto, K.W., Melham, T.: Formally Analysed Dynamic Synthesis of Hardware. Journal of Supercomputing 19(1), 7–22 (2001)
Susanto, K.W., Luk, W., Coutinho, J.G., Todman, T.: Validating Design Optimisation. In: Proc. Tools and Techniques for Verification of System Infrastructure, London, March 2008, p. 36 (2008)
Stalmarck, G.: A System for Determining Propositional Logic Theorems by Applying Values and Rules to Triplets that are Generated from a Formula, Swedish Patent No. 467 076 (1992), U.S. Patent No 5 276 897 (1994), European Patent No 0403 454 (1995)
Todman, T., Coutinho, J.G., Luk, W.: Customisable Hardware Compilation. Journal of SuperComputing 32 (2005)
Todman, T., Luk, W.: Memory Optimisations for High Resolution Imaging, in Proc. In: Proc. International Conference on Field-Programmable Technology, Brisbane, Australia (December 2004)
Zuck, L., Pnueli, A., Fang, Y., Goldberg, B., Hu, Y.: Translation and Run-Time Validation of Optimized Code. Electronic Notes in Theoretical Computer Science 70(4) (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Susanto, K.W., Todman, T., Coutinho, J.G., Luk, W. (2009). Design Validation by Symbolic Simulation and Equivalence Checking: A Case Study in Memory Optimization for Image Manipulation. In: Nielsen, M., Kučera, A., Miltersen, P.B., Palamidessi, C., Tůma, P., Valencia, F. (eds) SOFSEM 2009: Theory and Practice of Computer Science. SOFSEM 2009. Lecture Notes in Computer Science, vol 5404. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-95891-8_46
Download citation
DOI: https://doi.org/10.1007/978-3-540-95891-8_46
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-95890-1
Online ISBN: 978-3-540-95891-8
eBook Packages: Computer ScienceComputer Science (R0)