Coverage Metrics for Formal Verification
Related
Persistent Notes
In-text annotations
“1 Introduction” Page 1
“One direction is to detect vacuous satisfaction of the specification [BBER01,KV03,PS02], where cases like antecedent failure [BB94] make parts of the specification irrelevant to its satisfaction. For example, the specification “every request is eventually granted” is vacuously satisfied in a design in which no requests are sent." Page 2
Cover=0 assertions are vacuous Page 2
“Indeed, specifications are written manually, and their completeness depends entirely on the competence of the person who writes them” Page 2
“code-based coverage metrics, the design is given as a program in some hardware description language (HDL), and one measures the number of code lines executed during the simulation." Page 2
“Early work on coverage metrics in formal verification [HKHZ99,KGG99] suggested two directions. Both directions reason about a finite-state machine (FSM) that models the design. The metric in [HKHZ99], later followed by [CKV01,CKKV01,CK02], is based on mutations applied to the FSM. Essentially, a state in the FSM is covered by the specification if modifying the value of a variable in the state renders the specification untrue. The metric in [KGG99] is based on a comparison between the FSM and a reduced tableau for the specification. See [CKV01] for a discussion of pros and cons of this metric." Page 2
The FSM mutation metric or something similar to it is often used in miners that don’t have access to the RTL code. Page 2
“exhaustiveness of the verification effort, but no single measure can be absolute." Page 3
“Prior research of coverage in formal verification [HKHZ99,KGG99,CKV01,CKKV01,CK02] has focused solely on state-based coverage." Page 3
“Our goal in this paper is to adapt the work done on coverage in simulation-based verification to the formalverification setting in order to obtain new coverage metrics." Page 3
“The way we suggest to do so is to check whether the specification is vacuously satisfied in a mutant design in which this behavior is disabled: a vacuous satisfaction of the specification in such a design (we assume that the specification is not vacuously satisfied in the original design) indicates that the specification does refer to this behavior; on the other hand, a non-vacuous satisfaction of the specification in the mutant design indicates that the specification does not refer to the missing behavior." Page 3
“2 Preliminaries” Page 4
“2.1 Simulation-Based Verification” Page 4
“2.2 Model checking, vacuity, and coverage” Page 5
“Coverage in model checking was introduced in [HKHZ99,KGG99]. The metric in [HKHZ99] is based on FSM mutations” Page 6
“3 Coverage Metrics in Simulation-based Verification” Page 8
“3.1 Syntactic coverage metrics” Page 8
“The most widely used circuit-coverage metrics are latch and toggle coverage [HH96,KN96]. Essentially, a latch is covered if it changes its value at least once during the execution of the input sequence. Similarly, an output variable is covered if its value has been toggled” Page 8
“3.2 Semantic coverage metrics” Page 9
“4 Coverage Metrics in Model Checking” Page 9
“4.1 Syntactic coverage” Page 10
“4.2 Semantic coverage” Page 10
“5 Coverage Computation” Page 11
%% Import Date: 2025-12-31T14:40:36.739-05:00 %%