# An Approach to the State Explosion Problem: SOPC Case Study
## 1 Introduction  
The system on a programmable chip (SOPC) architecture is superior to traditional devices. Compared with traditional microprocessors or field-programmable gate array (FPGA) devices, the SOPC model integrates the advantages of both. The microprocessor is realized using an embedded microcontroller unit (MCU), digital signal processor (DSP), and arm hardcore or softcore processor intellectual property (IP). In addition, with the rich IP resources and programmable logic resources in FPGA, it provides a good platform for software and hardware collaborative development technology. The SOPC system can comprehensively consider various situations of the whole system, reduce the connection delay between discrete devices under the same process and technical conditions, and significantly improve the reliability and performance of the system. For example, in Xilinx devices, the zynq-7045 is embedded with the advanced reduced instruction set computer machines (ARM) cortex-a9 hardcore microprocessor [1] and the xq7k325t chip integrated with a MicroBlaze softcore [2]. The m2s090 ts-1 fgg484m is embedded with an arm Cortex-M3 hardcore microprocessor in Microsemi devices [3]. These chips are programmable logic chips with embedded processor structures. The software and hardware interfaces are highly coupled, and the connection modes are diversified. For example, they are directly connected through a standardized bus protocol interface, or in a user-defined way, and may also contain some adhesive logic. At the same time, there are various ways to share data, including interrupt mode, memory mapping I/O mode, and special function register mode. According to different applications, the design scale and the complexity are alsodifferent. In addition, because the programmable logic and embedded software in SOPC model design are usually described in different languages, and there are even a large number of black box IPs, the significant semantic gap between software and hardware makes verification more challenging. Traditional testing methods face serious challenges in SOPC model testing quality and efficiency. The SOPC model combines the characteristics of software and logic, so it also integrates the verification methods of software and logic. The existing SOPC model dynamic test types include function test, performance test, interface test, boundary test, margin test, safety test, strength test, and other test types [4; 5; 6], which can cover the function requirements, performance requirements, safety requirements, and other requirements in the requirements specification from multiple dimensions, and can give specific data, such as data processing time, system response time, etc. With the powerful function and wide application of SOPC architecture, the design scale of the system is becoming larger and more complex, and its security and reliability requirements are becoming more and more prominent. It is necessary to fully verify the SOPC model. Compared with ground software, once this SOPC software runs in orbit (the SOPC software runs on payload chips in space that will run in space for more than five years), it is difficult to locate the fault. Even if the fault can be located, a lot of costs would be required to upload and reconstruct it. Compared with traditional application-specific integrated circuit (ASIC) chips or FPGA chips, SOPC software usually includes one or more embedded processors, which can embed and run software programs and even operating systems on the chip. The verification of the SOPC model consists of the evaluation of whether it meets the requirements from multiple dimensions such as functionality, performance, and security based on requirements. At present, the traditional SOPC model verification technology includes a simulation test, a static analysis, and a physical test. Static and simulation tests verify the software and logic, respectively, and cannot cover the area of software and hardware interaction.