# An Approach to the State Explosion Problem: SOPC Case Study
## 6 Our Approach to State Space Reduction
### SOPC Reduced State Space Algorithm  
This paper proposes a state space reduction algorithm for the SOPC software. The problem of state space explosion of the SOPC software can be solved through the construction of a system-level model in the SOPC system, the analysis of state and state transition, variable reduction, and transition relationship reduction. Relevant algorithms are shown in Algorithm 1. The algorithm is divided into the following three steps. ```
INPUT: Design of an SOPC, A OUTPUT: SOPC reduced model, D_fomal / Step 1: SOPC design model construction*/  M = Identify_need_model(A)  FOR m \(\in\) M do  If m \(\in\) CPU then  m_formal = m = (s\({}_{0}\), s, I, O, f, g);  end  else if m \(\in\) netlist then  m_formal = m = (C, I, O, f\({}_{c}\), g);  end  else if m \(\in\) black_box then  m_formal = m = (I, O, g);  end  m_formal = m_formal \(\cup\) M_no_need_model; /Step 2: reduced variable*/  Rver = abstract_variables(property)  reduced_ctrl_variable = Pc(reg_ctt, reg_state) = \(\phi\)  reduced_assign_variable = Pa(reg_assign, reg_state) = \(\phi\)  reduce_variable = reduced_ctrl_variable \(\cup\) reduced_assgin_variable /Step 3: reduce transfer relation*/  FOR i = 1, i + n, i++) begin  Net_ver_i_ctrl = DFS(ver_i)  Net_ver_i_assign = DFS(Ver_i) + BFS(Ver_i)  Net_ver_i = Net_ver_i_ctrl \(\cup\) Net_ver_i_assgin End  D_fomal = convert_formal(Net_ver_1 \(\cup\) Net_ver_2 \(\cup\)... \(\cup\) Net_ver_i)
```  
**Algorithm 1**The formal verification framework for the SOPC software  
The first step is the modeling of the SOPC system. When building the model, if there is an original RTL code, we use the RTL code as a formal design model, which includes VHDL and Verilog. If there is no RTL code, we can convert models from other languages, such as MATLAB and C, into VHDL or Verilog using conversion tools. If there are no models in other languages, we build behavior-level models based on requirements and design documents, which can be used in VHDL, Verilog, or SVA. When building a design model manually, such as a CPU model, we do not need to describe the behavior of all CPUs. We only need to build the model for the behavior required, and we verify the consistency of the model by comparing the output under the same excitation after the construction is completed. The purpose of modeling the SOPC system is to establish the minimum design model for formal verification. First, select all IPs of the SOPC system according to the verification properties, and discard the IPs irrelevant to the verification properties. Secondly, establish a model for the reserved IP. If it is an IP that cannot be recognized by the formal tool, the model of various IPs is given through the polymorphic IP abstract modeling technology. For example, for the softcore or hardcore of the CPU, it is necessary to establish the working mode and interaction behavior between the CPU and other IPs, especially the reading and writing of the public storage area, the reading and writing of the public register, and the interrupt processing. For netlist IP, this paper mainly establishes a model from the information flow between sub-modules and sub-modules. A sub-module is regarded as a node, and the interaction between nodes connects two modules. For black-box IP, this paper mainly establishes a behavior layer model from the input-output relationship, establishes a complete input set, and obtains the matching output by combining multiple conditions of the input set. For the IP that can be recognized by the formal tool, it is believed that the completed IP code can be retained through analysis. After the completion of the model of the multi-form IP, this paper can form a complete SOPC system-level model by building the model of the on-chip bus and the model of the standardized interface between the IP and the on-chip bus. The second step is variable reduction.