A formal equivalence checking methodology for Simulink and Register Transfer Level designs

Driven by the increase in complexity of design, time-to-market pressure and the need for a high level of collaboration between multiple discipline teams in a project, model based design has become the inevitable choice for IC Design projects. High-level models are being substantially used as the reference for implementation of the Register Transfer Level (RTL) counterpart of the designs. In that respect, Matlab/Simulink is one of the adopted high level modeling platforms in the IC design industry. However, checking the formal equivalence of the models with their RTL counterparts is still an area of interest to be investigated. In this study, a methodology addressing that matter is proposed. Simulink models of interest in this paper comprise built-in Simulink blocks, Stateflow blocks modeling the state machines, and user-defined blocks. Proposed methodology utilizes Simulink´s Hardware Design Language (HDL) Coder and Real Time Workshop (RTW) tools, Mentor Graphics´ Catapult, and Synopsys´ Formality in the flow. Building of the methodology is explained with a simple example. Then the methodology is applied to multiple designs, including Advanced Encryption Standard (AES) to verify its applicability.