Assignment coverage, a complementary coverage metric in formal verification

Model checking is a formal verification method which proves whether a system satisfies a set of properties. After ensuring from correctness of properties, it is important to answer this question that which percent of the design was verified by the given set of properties? Coverage metrics in formal verification try to overcome this question. In this paper we will propose a new coverage metric in formal verification of hardware systems. We will define a mutation model to compute assignment coverage and the injection method of the proposed mutation model. This metric has the ability to make useful information to complete the set of properties. Also we will propose a method to extract minimal set of given properties for a verification process. This set reveals the effective properties to increase assignment coverage metric. The experiments show the effectiveness of this coverage metric.