Formal system-on-chip verification: An operation-based methodology and its perspectives in low power design

This paper surveys the state-of-the-art in operation-based property checking and describes how this technique can be used to conceptualize on a design at the Register-Transfer-Level (RTL). The paper argues that this technique can contribute to closing the semantic gap between system level design descriptions and the RTL and, thus, opens new possibilities for solving the power closure problem. The semantics of the high-level model are defined in terms of properties to be proven on the concrete RTL. The paper surveys a methodology to create sound abstractions and elaborates their possible role in a power-aware design flow. Specifically, it is demonstrated that the availability of a formal specification at an abstract level can be exploited for energy estimations at the system level as well as for deriving power optimizations at the RTL. First experimental results will be shown that demonstrate this optimization potential and confirm the correlation between energy consumption and operations which are the basic building blocks of the proposed abstract models.