Verification of System Level Model Transformations

This paper presents Model Algebra (MA), a formalism for representing SoC designs at system level. We define the objects and composition rules of MA and show how system level models can be represented as expressions in this formalism. The formalism is applied to a system level design methodology, where design decisions are used to gradually transform the functional specification model of the system to a transaction level model with components and communication structure. Each transformation is represented as a manipulation of a model algebraic expression, and proven for correctness using the laws of model algebra. These laws are based on the well defined execution semantics and notion of functional equivalence for MA models. Our approach promises significant savings in the verification of system level models because only the first model needs to be verified using conventional techniques. All transformations of this model, derived using MA laws, are proven to be functionally equivalent.