# An Approach to the State Explosion Problem: SOPC Case Study
## 6 Our Approach to State Space Reduction
### Variable Reduction Based on RTL Code  
In this section, we propose a variables reduction method based on RTL code, which can indirectly reduce the design state space. Variables in RTL code include the register, the wire, the input, and the output. RTL codes are as follows (Table 2), where rec_nstate is a register, and wr_en_in, rstn, and wr_cmd_data_in are input. The state (register) transition diagram based on RTL code is shown in Figure 9.  
From the state transition in Figure 9, we can see that each assignment of the register is a separate state, and the transition between states is determined by conditional branching. When we verify the properties of the SOPC system, we usually conduct a model check for each property. Since a single property does not involve all registers and variables of the design, if we only retain registers and variables related to the verification property, the state space of the design is reduced. This section proposes a method to reduce registers and variables from the perspective of the RTL code. In state transition, if there is no path from the control variable to the state register, then this control path is empty. It is shown as P\({}_{\text{c}}\)(var_ctrl, reg_state) = \(\phi\). As shown in Figure 9, P\({}_{\text{c}}\)(wr_cmd_data_in, rec_nstate) \(\
eq\phi\). In state transition, if there is no path from the assignment variable to the state register, then this assignment path is empty. It is shown as P\({}_{\text{a}}\)(var_assign, reg_state) = \(\phi\). As shown in Figure 9, P\({}_{\text{a}}\)(state_enum, rec_nstate) \(\
eq\phi\). \begin{table}
\begin{tabular}{l} \hline \hline \multicolumn{2}{c}{**RTL Codes**} \\ \hline Reg[4:0] rec\_nstate; \\ typedefenum logic [4:0] [SELFCHECK\_TASK, RESET\_TASK, DIR\_TASK, SYN\_TASK, \\ TIME\_TASK, REC\_TASK] state\_enum; \\ always @(posedge clk or negedge strn) \\ if(trstn) \\ rec\_nstate = SELFCHECK\_TASK; \\ else if(wr\_en\_in \&\&\&\) (wr\_cmd\_data\_in[31:24] == 8\({}^{\text{N}}\)h01)) \\ rec\_nstate = SELFCHECK\_TASK; \\ else if(wr\_en\_in \&\&\) (wr\_cmd\_data\_in[31:24] == 8\({}^{\text{N}}\)h02)) \\ rec\_nstate = RESET\_TASK; \\ else if(wr\_en\_in \&\) (wr\_cmd\_data\_in[31:24] == 8\({}^{\text{N}}\)h04)) \\ rec\_nstate = DIR\_TASK; \\ else if(wr\_en\_in \&\) (wr\_cmd\_data\_in[31:24] == 8\({}^{\text{N}}\)h08)) \\ rec\_nstate = SYN\_TASK; \\ else if(wr\_en\_in \&\) (wr\_cmd\_data\_in[31:24] == 8\({}^{\text{N}}\)h10)) \\ rec\_nstate = TIME\_TASK; \\ else \\ rec\_nstate = rec\_nstate; \\ \hline \hline \end{tabular}
\end{table} 
Table 2: RTL codes. After analyzing the control path and assigning the path, we will discuss the reduction in design variables and registers by analyzing the variables of properties. An SVA property based on the RTL code in Figure 9 is shown below:  
Suppose Rver is a verified register in a specification, then the verification variables for the above property include {rstn, rec_nstate, state_enmum}, where the rstn is the conditional variable, the state_enum is the assigning variable, and the rec_nstate is the state registers. Figure 9: State transition diagram. In this property, the variable rstn and state_enum in the design model can be retained, and other variables can be reduced; for example, the variable wr_en_in and the variable wr_cmd_data_in. In a real large-scale SOPC design, the complexity of the property and design would be much greater than in the example in Figure 9. The methods and steps of reduction are given below. **Definition 7**. : _Design variable minimum set: If \(R_{d}\) is the variable set of the design model, a minimum variable set \(R_{r}\)\(\in\)\(R_{d}\) is found during the property verification, so that the states of the design model can be minimized, and the reduced design model should be equally equivalent to the design model before the reduction._  
The steps for variable reduction are shown in Figure 10:  
\(R_{ver}\) is a set of verification variables that refer to the property. \(R_{d}\) is a set of model variables, \(r_{d}\)\(\in\)\(R_{d}\).