Syntactic transformation of assume-guarantee assertions: from sub-modules to modules

Assume-guarantee style assertions are increasingly being adopted by the design community. This paper addresses the task of transforming the assume-guarantee RTL properties of a set of submodules to a set of assume-guarantee properties of the parent module. Though this task is of considerable importance in the validation of large designs, current assertion specification languages do not admit a clean separation between a behavioral property of a module (the "guarantee") and the input restriction (the "assume") under which it is expected to hold, thereby making this task very complex. In this paper, we propose a logic called interactive linear temporal logic which provides a platform for expressing module-level specifications separating the input assumptions from the guarantee properties. Using this logic, we further show how assume-guarantee properties for individual modules can be composed, thereby facilitating hierarchical FPV of large designs.