Conditioned Slicing for Efficient Multiway Decision Graphs Model-Checker

Abstract

Integrating formal verification techniques into the hardware design process provides the means to rigorously prove critical properties. However, most automatic verification techniques, such as model checking, are only effectively applicable to designs of limited sizes due to the state explosion problem. The Multiway Decision Graphs (MDG) method is an efficient method to define hardware designs into more abstract environments; however, the MDG model checker (MDG-MC) still suffers from the state explosion problem. Furthermore, all the backward reduction algorithms cannot be used in MDG, due to the presence of abstract state variables. In this study, an efficient extractor for MDG Hardware Descrpiton Languge (MDG-HDL) is introduced based on static (SS-MDG) and conditioned (CS-MDG) program slicing techniques. The techniques can obtain a chaining slice for given signals of interest. The main advantages of these techniques are: It has no MDG-HDL coding style limitation, it is accurate and it is competent in dealing with various MDG-HDL constructions. The main motivation for introducing this approach is to tackle the state explosion problem of MDG-MC that big MDG-HDL may cause. We apply our proposed techniques on different MDG-HDL designs and our analyses have shown that the proposed reduction techniques resulted in significantly improved performance of the MDG-MC. In this study, we present a general idea of program slicing, a discussion of how to slice MDG-HDL programs, implementation of the tool and a brief overview of some applications and experimental results. The underlying method and the tool based on it need to be empirically evaluated when applying to various applications.