DocumentCode :
2367834
Title :
Formal methods for analyzing the completeness of an assertion suite against a high-level fault model
Author :
Das, Sayantan ; Banerjee, Ansuman ; Basu, Prasenjit ; Dasgupta, Pallab ; Chakrabarti, P.P. ; Mohan, Chunduri Rama ; Fix, Limor
Author_Institution :
Dept. of Comput. Sci. & Eng., Indian Inst. of Technol., Kharagpur, India
fYear :
2005
fDate :
3-7 Jan. 2005
Firstpage :
201
Lastpage :
206
Abstract :
One of the emerging challenges in formal property verification (FPV) technology is the problem of deciding whether sufficient properties have been written to cover the design intent. Existing literature on FPV coverage does not solve this problem adequately, since they primarily analyze the coverage of a specification against a given implementation. On the other hand, we consider the task of determining the coverage of a formal specification against a high-level fault model that is independent of any specific implementation. We show that such a coverage analysis discovers behavioral gaps in the specification and prompts the design architect to add more properties to close the behavioral gaps. Our results establish that the coverage analysis task at this level is computationally complex, but it is possible to obtain a conservative estimate of the coverage at low cost.
Keywords :
computational complexity; formal specification; program verification; assertion suite completeness; behavioral gaps; coverage analysis; fault model; formal methods; formal property verification; formal specification; Computational modeling; Computer science; Costs; Formal specifications; Logic design; Protocols; Standards development; Strategic planning; Testing; Writing;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
VLSI Design, 2005. 18th International Conference on
ISSN :
1063-9667
Print_ISBN :
0-7695-2264-5
Type :
conf
DOI :
10.1109/ICVD.2005.101
Filename :
1383277
Link To Document :
بازگشت