Static slicing-based pre-reduction technique for MDG model-checker

The hardware designs that are described at the register transfer level (RTL) have become more complex and difficult to debug. Therefore, using Multiway Decision Graphs (MDG), the same designs can be defined into a more abstract environment. However, to avoid the state explosion problem, the MDG-based designs still need to be reduced. Moreover, all the backward reduction algorithms cannot be used in MDG, due to the presence of abstract state variables. In this paper, we study this problem and propose a new reduction technique, called static slicing pre-reduction technique (SSPr-MDG), in order to deal with the MDG-based designs. The main feature of our SSPr-MDG is to construct a reduced transition relation (Tr) using circuit dependency graph (CCDG). Our results, along with the case study, indicate the practical merits of the SSPr-MDG in terms of processing time, graph size, and memory capacity.