Architecture Model Refinement Verification in System Level Design
Douglas Michael Densmore and Alberto L. Sangiovanni-Vincentelli
The goal of this project is to identify a formal procedure in which to verify that one platform model (potentially an architecture modeled in Metropolis  or Metro II ) is a "refinement" of another model. As the level of abstraction used to specify systems increases, this process becomes critical. Unlike equivalence checking, we are not interested in whether or not the two models are functionally the same but rather if the refined model can be substituted for the more abstract model and ensure that the system will still function correctly.
A combination of interface synthesis , event trace reasoning, and model algebra  manipulation are exploited to perform refinement verification of these platforms at a variety of abstraction levels. This approach ensures that the verification effort is not duplicated and that as models become less abstract, their behaviors remain contained by their abstract counterparts
This investigation will answer the following questions: Firstly, what properties or conditions should refinement ensure at the system level? Secondly, how are these properties or conditions expressed and ultimately extracted from the model? And thirdly, once these two questions are answered, how can we efficiently and ideally automatically perform this verification? This project should culminate in an addition to the Metro II framework which supports this verification as well as a methodology which potential designers can use in order to preserve refinement in subsequent models.
- F. Balarin, Y. Watanabe, H. Hsieh, L. Lavagno, C. Passerone, and A. L. Sangiovanni-Vincentelli, "Metropolis: An Integrated Electronic System Design Environment," IEEE Computer, April 2003, pp. 45-52.
- A. Davare, D. Densmore, T. Meyerowitz, A. Pinto, A. Sangiovanni-Vincentelli, G. Yang, H. Zeng, and Q. Zhu, "A Next-Generation Design Framework for Platform-Based Design," Conference on Using Hardware Design and Verification Languages (DVCon), February 2007.
- D. Densmore, S. Rekhi, and A. L. Sangiovanni-Vincentelli, "Microarchitecture Development via Metropolis Successive Platform Refinement," Design Automation and Test Europe, Paris, France, February 2004.
- S. Abdi and D. Gajski, "Verification of System Level Model Transformations," International Journal of Parallel Programming, February 2006 (to appear).