Functional Verification of System Level Model Refinements

by Samar Abdi

With continuous improvement in process technology, designers have more resources than ever available for implementing their systems. As applications become larger, the modeling abstraction has to rise to keep the complexity manageable. This has given rise to modeling at abstractions above the register transfer and cycle accurate levels. Verification becomes an even greater challenge as designers try to develop more models to evaluate their implementation choices. In this dissertation we present our verification strategy to alleviate the problems resulting from the move to system level. We argue our case for a system level modeling and verification methodology where detailed models are refined from abstract models. The models are represented formally using Model Algebra and the refinements are proved to be functionality preserving, using the rules of Model Algebra. We define the objects and composition rules of Model Algebra and show how system level models are represented as expressions in this formalism. The formal execution semantics of such models are discussed and a notion for functional equivalence of models is also presented. We then define transformation rules that syntactically modify a model algebraic expression, while keeping its functionality intact. Then we present key refinements that are commonly encountered in system level design and prove the correctness of those refinements using the transformation rules of Model Algebra. As a proof of concept, we implemented a tool that automatically checks if the refinements were performed correctly on SpecC models. As a result, the designer needs to perform the costly and time consuming property verification on the first model only. All step wise refinements from the original model are proven to produce functionally equivalent models.