# An Approach to the State Explosion Problem: SOPC Case Study
## 1 Introduction
As shown in Figure 1, the logic is the yellow box, and the software (processing system) is the green box. If the software and hardware are tested together, physical testing needs to be used. Physical testing inputs excitation from the input end of the chip and observes the output from the output of the chip. The software and hardware coupling area cannot be observed and cannot achieve 100% coverage because it is inside the chip. Figure 1: SOPC architecture. The verification of the area of software and hardware interaction in physical tests is based on limited test scenarios, which can only prove the existence of errors and defects in some cases. However, for the test scenarios not involved in the test cases, the correctness of the system design cannot be guaranteed, so there may be some hidden defects that cannot be found. Therefore, dynamic verification is generally suitable for finding a large number of obvious design errors in the early stage of verification, but it is difficult to mine the hidden and subtle errors in complex design, such as system architecture errors, software, and hardware coordination errors, etc. The differences between traditional testing and formal testing are shown in Table 1. So when we focus on SOPC model verification, we use model-checking methods on the basis of traditional testing methods. This helps us find hidden defects in the code, like defects in software and hardware coupling. The application practice of formal methods began in the 1970s and plays an extremely important role in the key field of safety. The most important feature of formal verification is that it is based on mathematical logic reasoning and proves whether the system design meets the system specification according to mathematical theory. For the existing test types and test methods of SOPC architecture, formal verification, as a powerful supplementary verification method, can make up for the shortcomings of the existing verification methods. By summarizing the key properties to be verified, it provides a good supplement to the existing dynamic test and static test, and effectively improves the quality of the software test and software reliability. The research on model detection [7; 8] began in the early 1980s when [PERSON], [PERSON], and others proposed CTL logic to describe the properties of concurrent systems, designed algorithms to detect whether a finite state system satisfies a given formula, and implemented a prototype system. The basic idea of model checking [9] is to express the temporal properties of a program or circuit using temporal logic formulas and to use finite state machines to represent the abstract structure of state transitions in a program or circuit [10; 11]. The correctness of the temporal logic formulas is verified by traversing finite state machines. Model checking is an exhaustive search based on the system state space. The number of states often increases exponentially with the increase in concurrent components. Therefore, when a system has many concurrent components, it is not feasible to search its state space directly, which is the so-called state space explosion problem. The scale and complexity of aerospace SOPC software have doubled in the last ten years. At present, the scale of single-chip software has reached about 150,000 lines and involves the implementation of various complex protocols. For such a concurrent system as the SOPC model, the number of states often increases exponentially with the increase in concurrent components, so it is actually impossible to search its state space. Aiming at the state space explosion of the SOPC model, our main contributions in this paper are listed as follows: