Name
Title | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1007/978-3-540-95891-8_46 | SOFSEM |
Keywords | Field | DocType |
design optimization exploration,case study,efficient design validation flow,equivalence checking,formal verification,design validation,memory optimization,functional equivalence,image manipulation,design property,source design,validation analysis,equivalence checker,automated validation flow,exploration process,resource utilization,design optimization | Formal equivalence checking,Symbolic simulation,Discrete mathematics,Validation rule,Computer science,Equivalence (measure theory),Symbolic execution,Novelty,Encoding (memory),Formal verification | Conference |
Volume | ISSN | Citations |
5404 | 0302-9743 | 5 |
PageRank | References | Authors |
0.52 | 16 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Kong Woei Susanto | 1 | 81 | 5.22 |
| Tim Todman | 2 | 65 | 12.10 |
| J. G. F. Coutinho | 3 | 125 | 17.26 |
| Wayne Luk | 4 | 3752 | 438.09 |