Abstract

The system-On-Chip design process is continuously increasing in terms of cost and complexity. This imposes new modeling and verification challenges. A particular example is heavy computational applications and functionality, such as digital signal processing and telecommunication applications, which are increasingly integrated in embedded systems nowadays. To meet these challenges, designers use a multilevel model based approach, which is a top-down design methodology where the behavior of the system is first modeled at a higher level of abstraction. Then, design decisions are made to refine those models in a number of transformations until the final product is realized. In this thesis we verify an implementation of a WiMax modem physical layer that has been designed according to the multilevel design approach. This implementation is provided by STMicroelectronics. We propose the utilization of two verification methodologies to verify designs at higher levels of abstraction. The first one is an equivalence checking methodology that is based on symbolic simulation, which provides high speed and computational capabilities. The main purpose of this methodology is to verify the functional equivalence of refined system models in the design process. The second methodology is a property checking approach, which is also based on symbolic simulation. It verifies the conformance of models at different levels of abstraction with the system specification. We verified the equivalence of three models of the WiMax system at different levels of abstraction, and we verified the correctness of various system properties on those models.