Resumen:
This report presents a tool for functional equivalence verification of transaction level models (TLMs). The tool is based of the theory of Model Algebra which provides the objects and composition rules needed to abstract TLMs into symbolic expressions. Synthesis and verification of TLMs is made possible by the manipulation of these symbolic expressions using the transformation rules of Model Algebra. We define the verification problem in the context of platform based design. Functional TLMs that are refined as a result of design optimization are verified against original TLMs for consistency. We describe the Application Program Interface for the Model Algebrabased verification tool. The tool is composed of two main parts: the model creation component and the verifier component. The first API allows the user to abstract TLMs into model algebraic expressions, while the second API allows …
