A Generalized Theory for Formal Assertion Coverage

Coverage of formal property specifications has important ramifications in design verification. Mutation coverage, a well studied approach towards specification coverage, checks whether the specification fails in the presence of a fault. Existing mutation coverage methods are broadly divided into those which inject the fault into a given implementation and those which inject the fault directly into the specification. This paper presents a theory which unifies these contrasting approaches and extends the mutation coverage approach to partial implementations where some components are given, and for the others, we only have component specifications.