Design Validation by Symbolic Simulation and Equivalence Checking: A Case Study

Abstract. Design optimization exploration is a key element in finding an optimal resource utilization. The exploration process applies opti-mizations 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 valida-tion. 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 simpli-fication techniques, such as if-conversion and loop-conversion, and state encoding to ease validation analysis.