Design validation by symbolic simulation and equivalence checking: A case study in memory optimization for image manipulation

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. © Springer-Verlag Berlin Heidelberg 2009.