# An Approach to the State Explosion Problem: SOPC Case Study
## 5 Modeling and Verification of the SOPC System  
### Modeling of SOPC System  
This section will give the method of establishing a formal design model from the perspective of the SOPC system level as shown in Figure 5. An SOPC model may contain more than ten or more IPs according to the specific application design. Each IP core has specific functions. These IP cores are interconnected through the on-chip bus to achieve efficient data and information exchange. Suppose that a SOPC model design is expressed in \(M\), and each independent IP in the SOPC model includes its own functions, interfaces, and interaction with other IPs, expressed as \(m_{1}\), \(m_{2}\), \(\ldots\), \(m_{k}\in M\). The on-chip bus interconnection module belonging to  
Figure 4: The problem of state space explosion. Figure 5: Block diagram of the SOPC system. behavior of implementing the automaton does not comply with the behavior defined by the property automaton. In the formal verification based on automaton theory, assuming that \(\mathrm{L(A)}\) and \(\mathrm{L(P)}\) represent the language accepted by the implementation of automaton A and property automaton P, respectively, testing \(\mathrm{L(A)}\subseteq\mathrm{L(P)}\) is equivalent to testing whether \(\mathrm{L(A)}\cap\sim\mathrm{L(P)}\) is empty. In this way, as shown in the following Equations (10)-(12), the combined automaton AP includes all the traces of implementation that do not meet the property. If the AP is a directed graph, detecting whether the AP has a trace that does not meet the specification is equivalent to detecting whether the AP contains at least one path from the initial state S0 to the accepted state as shown in Equation (13). \[\mathrm{A}=(Q_{A},\sum_{A},\delta_{A},q_{0_{A}},F_{A}) \tag{10}\]  
\[\mathrm{P}=(Q_{P},\sum_{P},\delta_{P},q_{0_{P}},F_{P}) \tag{11}\]  
\[A\mid\mathrm{I}\,P=C,C=(Q,\sum,\delta,q_{0},F) \tag{12}\]  
\[\mathrm{While}\,Q=Q_{A}\times Q_{P},\ \sum=\sum_{A}\cup\sum_{P},\ q_{0}=q_{0_{A}} \times q_{0_{P}},\ \mathrm{F}=F_{A}\times F_{P} \tag{13}\]  
\[\mathrm{path}=q_{0}\ \overset{\sigma\mathrm{1}}{\rightarrow}\ s_{\sigma 1}\ \overset{\sigma \mathrm{2}}{\rightarrow}\ s_{\sigma 2}......\overset{\sigma\mathrm{f}}{ \rightarrow}\ s_{\sigma f},s_{\sigma f}\in\mathrm{F}\]  
As shown in Figures 6-8, we construct a finite directed graph AP whose nodes are an ordered pair. The first component of the ordered pair is a state of the implementing automaton A, and the second component is a subset of the states of the property automaton P. Because A is deterministic, it has only one initial state, and whenever a character is read, the implementing automaton A can only reach one next state. The automaton P is nondeterministic, which may transfer to multiple states after reading the character a. Additionally, s0 is the initial state of implement automaton A and S0 is a set of initial states. In concurrent systems, there may be multiple initial states. T0 is the initial state of the property automaton. If the automaton A can enter a state sj after accepting the input a, the automaton P can also accept the character a to enter one or more sub-state sets, tj. If tj and sj are both members of the state set, the \"pass\" is used to identify the state (sj, tj), otherwise the \"fail\" is used. If the automaton AP contains a path from the initial node to the failed node, it indicates that the language of automaton acceptance is outside the language of property automaton acceptance. SVA is the abbreviation of SystemVerilog Assertions. From a linguistic perspective, it is a new temporal logic language derived from LTL and RE semantics. Its concise syntax can describe complex temporal behaviors, which traditional temporal logic languages do not have. Therefore, it is more suitable for describing the behavior of SOPC systems that are sensitive to timing. In any property model, a sequence is represented by a combination of multiple logical events, which can be a simple Boolean expression evaluated at the same clock edge or an event evaluated over several clock cycles.