Construction of concrete verification models from C

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.