Signal Coverage Computation in Formal Verification

Formal verification is an automatic technique to verify whether certain properties, expressed in a property language like computational temporal logic (CTL), hold in a model, typically expressed in an HDL language like VHDL. Assume that all specification formulae were successfully checked for the implementation. Are we sure that the implementation is correct? If the specification is incomplete, we may fail to find an error in the implementation. On the other hand, if the specification is complete, then the model checking process can be stopped without adding more specification formulae. So coverage computation is an important phase in model checking process. In this paper we propose a new coverage metric for formal verification of hardware systems. We define signal coverage in formal verification and we explain our method to implement signal coverage with help of OBDD. For various levels and forms of coverage we show examples and properties that cover or uncover design signals. Our experiments on some benchmark circuits show effectiveness of this algorithm and its capabilities