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. Categories and Subject Descriptors B.6.3 [LOGIC DESIGN]: Design Aids--Verification General Terms Design, ...

• Type: Conference
• Year: 2008
• Where: DAC
• Authors: Malay Haldar, Gagandeep Singh, Saurabh Prabhakar, Basant Dwivedi, Antara Ghosh
• Keywords: C++ Based Verification, DAC 2008, Design Automation, Equivalence Checking, Sequential Equivalence Checking