Cohesive Coverage Management: Simulation Meets Formal Methods

Hazra, Aritra ; Ghosh, Priyankar ; Dasgupta, Pallab ; Chakrabarti, Partha Pratim (2012) Cohesive Coverage Management: Simulation Meets Formal Methods Journal of Electronic Testing, 28 (4). pp. 449-468. ISSN 0923-8174

Full text not available from this repository.

Official URL: http://doi.org/10.1007/s10836-012-5308-1

Related URL: http://dx.doi.org/10.1007/s10836-012-5308-1

Abstract

It has been advocated by many experts in design verification that the key to successful verification convergence lies in developing the verification plan with adequate formal rigor. Traditionally, the verification plans for simulation and formal property verification (FPV) are developed in different ways, using different formalisms, and with different coverage goals. In this paper, we propose a framework where the difference between formal properties and simulation test points is diluted by using methods for translating one form of the specification to the other. This allows us to reuse simulation coverage to facilitate formal verification and to reuse proven formal properties to cover simulation test points. We also propose the use of inline assertions in procedural (possibly randomized) test benches, and show that it facilitates the use of hybrid verification techniques between simulation and bounded model checking. We propose the use of promising combinations of formal methods presented in our earlier papers to shape a hierarchical verification flow where simulation and formal methods aim to cover a common design intent specification. The proposed flow is demonstrated using a detailed case study of the ARM AMBA verification benchmark. We believe that the methods presented in this work will stimulate new thought processes and ultimately lead to wider adoption of cohesive coverage management techniques in the design intent validation flow.

Item Type:Article
Source:Copyright of this article belongs to Springer Nature Switzerland AG
Keywords:Simulation;Formal property verification;Test plan;Test points;Coverage;Assertion;Inline assertion;Semi-formal verification
ID Code:129751
Deposited On:21 Nov 2022 03:44
Last Modified:21 Nov 2022 03:44

Repository Staff Only: item control page