# An Approach to the State Explosion Problem: SOPC Case Study
## 6 Our Approach to State Space Reduction
### Transform Relations Reduction Based on Property  
In this section, we propose a state transition relation reduction method based on verification properties. Through the reduction in the transition relation, the model state space can be further reduced. Through the analysis of the RTL code variables in the previous chapter, we reduced the variables of the model based on the analysis of verified property variables. After reduction, only the variables related to the verified property were left in the model. Based on the reduction in variables, we can further analyze the transform relations between variables. For the same number of variables, there can be many kinds of transform relations between variables. The idea of this section is to further reduce the state space of the model by reducing the transform relations irrelevant to the verification properties. The method is shown in Figure 16. Firstly, we select the root node according to the verification property and then search the control branch and the assigned branch through the root node to form the complete network state diagram of the model. Figure 16: Transfer relations diagram. Figure 15: Variable interaction diagram. Root node variable selection  
The root node is based on the variables involved in the verification property. For example, the property is shown in Table 3.  
The root variables include the rstn and the rec_nastate. Because SELFCHECK_TASK is an enumeration constant, it is not included in the root node. The variable rstn is the input signal, so it is also not in the root node. Next, we use the root node as the starting point to find the control branch path and assignment branch path, respectively. Control branch search  
If v is the root node, we search the control path that controls the variable transforms. It is shown as P\({}_{\text{c}}\)(var_ctrl, reg_state) \(\
eq\)\(\phi\). The var_ctrl includes the condition variables in the property. For example, if the condition variable of property reset_check is rstn, then we start from the root node and find the condition branch!rstn, and then other branches are discarded. When the branch variables involved in the property are complex, we start from the root node and use the Depth First Search (DFS) algorithm to search all the control paths related to the root node. When searching the first level variable, if the variable is an input signal or a constant, we stop searching the current node and return to other nodes at the same level. When the first level variable to be searched is a register, then we search the second level variable from the current node until the variable is an input or constant. As shown in Figure 17, we start from the root node and reverse search along one path to the end (root, variable 1). When we finish the first path, we search for the second path from the node register variable 2. For the two branches of variable 2, we start the search from the left branch until we find the input signal or constant node. After the search, we return to the node of variable 2 to start searching the right branch. We repeat this process until all control paths related to the root node are searched. The control path vector diagram of the root node is formed. Figure 17: Control branch network. \begin{table}
\begin{tabular}{c} \hline \hline \multicolumn{2}{c}{**An SVA Property Based on the RTL Code**} \\ \hline Property reset\_check \\ ($fell(rstn)!\) \(>\) rec\_nstate\(=\) SELFCHECK\_TASK \\ Endproperty \\ \hline \hline \end{tabular}
\end{table} 
Table 3: An SVA property based on the RTL code. Assignment branch search  
An assignment transformation graph is a network graph for finding assignment variables related to verification variables. If v is the root node, we search the assignment path assigned to register v. It is shown as Pa(var_assign, reg_state) \(\
eq\)\(\phi\). The reg_state includes the register variables in the property. For example, the register variable of property reset_check is rec_nstate.