Discovering the input assumptions in specification refinement coverage

Basu, Prasenjit ; Das, Sayantan ; Dasgupta, Pallab ; Chakrabarti, P. P. (2006) Discovering the input assumptions in specification refinement coverage Asia and South Pacific Design Automation Conference . pp. 13-18.

PDF - Publisher Version

Official URL:

Related URL:


The design of a large chip is typically hierarchical - large modules are recursively expanded into a collection of sub-modules. Each expansion refines the design due to the addition of level specific details. We believe that a similar approach is necessary to scale the capacity of formal property verification technology - as the design gets refined from one level to another, the formal specification must also be refined to reflect the level specific design decisions. At the heart of this approach we propose a checker that identifies the input assumptions under which the refined specification "covers" the original specification. This enables the validation engineer to focus the verification effort on the remaining input scenarios thereby reducing the number of target coverage points for simulation.

Item Type:Article
Source:Copyright of this article belongs to Institute of Electrical and Electronic Engineers.
ID Code:6009
Deposited On:19 Oct 2010 09:52
Last Modified:16 May 2016 16:26

Repository Staff Only: item control page