2013/07/30 by Salim Ismail Al-Akhras, Sofiène Tahar, Gabriela Nicolescu +3 · 2 citations
Computer Science · Engineering · Mathematics · #Abstraction #Cellular Automata and Applications #Computer science #Correctness #Embedded Systems Design Techniques #Equivalence (formal languages) #Formal equivalence checking #Formal verification #Functional verification #Mathematics #Model checking #Programming language #Symbolic trajectory evaluation #Theoretical computer science #Transformation (genetics) #VLSI and FPGA Design Techniques #cs.LO
paper · pdf · doi:10.4204/eptcs.122.3
published in Electronic Proceedings in Theoretical Computer Science 122, 23-37 (Open Publishing Association) · In Proceedings SCSS 2012, arXiv:1307.8029
openalex publication_date 2013/07/30 · arxiv created 2013/07/31 · arxiv updated 2013/08/02 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/05
In top-down multi-level design methodologies, design descriptions at higher levels of abstraction are incrementally refined to the final realizations. Simulation based techniques have traditionally been used to verify that such model refinements do not change the design functionality. Unfortunately, with computer simulations it is not possible to completely check that a design transformation is correct in a reasonable amount of time, as the number of test patterns required to do so increase exponentially with the number of system state variables. In this paper, we propose a methodology for the verification of conformance of models generated at higher levels of abstraction in the design process to the design specifications. We model the system behavior using sequence of recurrence equations. We then use symbolic simulation together with equivalence checking and property checking techniques for design verification. Using our proposed method, we have verified the equivalence of three WiMax system models at different levels of design abstraction, and the correctness of various system properties on those models. Our symbolic modeling and verification experiments show that the proposed verification methodology provides performance advantage over its numerical counterpart.