چکیده (انگلیسی):

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 MDGHDL
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.