# An Approach to the State Explosion Problem: SOPC Case Study
## 7 Experiment
### Model Checking Result Analysis  
This original design was implemented using Xilinx Kintex-7 series FPGA chips, the language was Verilog, and the number of lines of code was about 70,000 lines. After the front-end code was synthesized, placed, and routed, a synchronous sequential software composed of logic resources, wiring resources, clock resources, storage resources, IP resources, etc., was obtained. The resources occupied by this design are shown in Figure 21.  
\begin{table}
\begin{tabular}{c c c} \hline \hline
**Type** & **Property** & **Property** \\ \hline Read\_Write & Does not read and write the same address &! (Read\&write\&(Read\_addr==Write\_addr)) \\ conflict & of dual-port RAM at the same time. &! (master1\_wr\&\(master2\_wr\&(master1\_wr\&(master1\_wr\&(master2\_wr\&\  
The resource list in the figure above includes flip flop (FF), lookup table (LUT), input-output (IO), and other components. From the synthesis result, we can see that the FPGA software has 221,340 flip flops and 182,304 \(\times\) 6 logic lookup tables. Based on the third chapter theory analysis of the number of states, if this SOPC software does not perform state reduction, \(2^{221,340}\) states and \(2^{221,340}\)\(\times\)\(2^{71}\) transition relationships need to be traversed in formal verification. After the model of the CPU was established, we integrated the CPU model and the SOPC logic code to form a complete formal SOPC design model. In the comparative experiment, based on the original SOPC formal design model and the formal design model after variables reduction and transfer relations reduction, we conducted model checking on the five properties in the previous section, and the test results are shown in Tables 7 and 8. In the experiment process, we first performed the variable reduction method on the original model. After the reduction, we performed transfer relations reduction. We compared the states of the original design with the states of the reduced design and compared the run time with the memory of different properties. In Table 7, the first two columns, \"property\" and \"pass\", show verified properties and the result of property verification. The third to sixth columns, respectively, show the total running time needed to verify each property and the peak memory. In Table 7, the results of the original formal design model test are shown; property 1 and property 2 have no results. In the experiment we chose 2 h as the time limit; beyond 2 h, the property cannot be verified. From the memory usage and runtime of property verification, we can see that the runtime is significantly reduced. Moreover, in experiments with property 1 and property 2, we set their timeout as two hours. While the properties cannot be verified in the original design, they can be verified after state reduction. For different properties, if the design state space involved in property A is larger than the design state space involved in property B, then the time to detect property A is longer \begin{table}
\begin{tabular}{c c c c c c} \hline \hline \multirow{2}{*}{**Property**} & \multirow{2}{*}{**Pass \({}^{*}\)**} & \multicolumn{2}{c}{**Original Formal Design Model**} & \multicolumn{2}{c}{**Reduction Formal Design Model**} \\ \cline{3-6}  & & _Memory_ **(MB)** & _Running Time_ **(s)** & _Memory_ **(MB)** & _Running Time_ **(s)** \\ \hline P1 & \(\surd\) & NA & NA & 1056 & 2954 \\ P2 & \(\times\) & NA & NA & 1024 & 2410 \\ P3 & \(\surd\) & NA & NA & 1114 & 3202 \\ P4 & \(\surd\) & 274 & 810 & 124 & 44 \\ P5 & \(\surd\) & 214 & 702 & 122 & 40 \\ P6 & \(\times\) & 680 & 3450 & 685 & 211 \\ P7 & \(\surd\) & 1036 & 3228 & 780 & 130 \\ P8 & \(\times\) & NA & NA & 1024 & 3581 \\ P9 & \(\surd\) & 362 & 1012 & 178 & 68 \\ \hline \hline \end{tabular}  
* \({}^{*}\times^{o}\) means property verification failed; \({}^{o}\surd\) means property verification passed; and NA means no detection.  
\end{table} 
Table 7: Running Results of the experiment.