SAT-based Calculation of Source Code Coverage for BMC.
Görschwin Fey, Rolf Drechsler · 2006
Property checking is the method of choice to guarantee functional correctness of a design under any input assignment and in any state. But so far only few methods to evaluate the coverage achieved by a set of properties have been presented. These methods either suffer from complexity problems known from CTL model checking or are incomplete themselves due to simulation-based engines. In this work we present an approach to calculate coverage information in the context of Bounded Model Checking (BMC). The components of a design that are covered by a given set of properties are calculated. The result is presented at the source code level. The approach is explained in detail and empirically evaluated. 1