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

Basu, P. ; Dasgupta, P. ; Chakrabarti, P. P. (2005) Syntactic transformation of assume-guarantee assertions: from sub-modules to modules In: 18th International Conference on VLSI Design held jointly with 4th International Conference on Embedded Systems Design, 3-7 January 2005.

Full text not available from this repository.

Official URL:

Related URL:


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.

Item Type:Conference or Workshop Item (Paper)
Source:Copyright of this article belongs to Institute of Electrical and Electronics Engineers.
ID Code:101694
Deposited On:09 Mar 2018 10:18
Last Modified:09 Mar 2018 10:18

Repository Staff Only: item control page