Title
Construction of concrete verification models from C++
Abstract
C++ based verification methodologies are now emerging as the preferred method for SOC design. However most of the verification involving the C++ models are simulation based. The challenge of using C++ for sequential equivalence checking comes from two aspects (1) Language constructs such as pointers, polymorphism, virtual methods, dynamic memory allocation, dynamic loop bounds, floating points pose difficulty in creating a model suitable for equivalence checking (2) The memory and runtime required for creating models suitable for equivalence checking from practical C++ designs is huge. In this paper we describe techniques for constructing verification models from C++ designs containing a very rich set of language constructs. The flow is built keeping in mind that formal methods are inherently capacity constrained but need to be applied to large C++ designs to have practical value.
Year
DOI
Venue
2008
10.1145/1391469.1391707
Anaheim, CA
Keywords
Field
DocType
dynamic memory allocation,language construct,dynamic loop bound,equivalence checking,sequential equivalence checking,practical value,verification methodology,concrete verification model,large c,verification model,practical c,system on chip,testing,floating points,pointers,construction industry,automata,floating point,computational modeling,polymorphism,formal verification,hardware,design methodology,logic design,indexes,dynamic scheduling,concrete,c,formal methods,resource management,computer architecture
Formal equivalence checking,Pointer (computer programming),Programming language,C dynamic memory allocation,Computer science,Floating point,Language construct,Automaton,Theoretical computer science,Formal methods,Formal verification
Conference
ISSN
ISBN
Citations 
0738-100X
978-1-60558-115-6
2
PageRank 
References 
Authors
0.47
5
5
Name
Order
Citations
PageRank
Malay Haldar19810.78
Gagandeep Singh292.48
Saurabh Prabhakar320.47
Basant Dwivedi420.47
Antara Ghosh5211.93