El sistema en una arquitectura de chip programable (SOPC) es mejor que la arquitectura tradicional de unidad central de procesamiento (CPU) + matriz de puertas programable en campo (FPGA). Forma un acoplamiento eficiente entre el software del procesador y la lógica programable a través de un bus de alta velocidad en el chip. La arquitectura SOPC es rica en recursos y altamente personalizable. Al mismo tiempo, combina un bajo consumo de energía y un alto rendimiento, lo que lo hace popular en el campo de alta confiabilidad y otros nuevos campos industriales. El sistema de arquitectura SOPC es complejo e integra múltiples formas de propiedad intelectual (PI). Debido a esto, la prueba dinámica tradicional y la prueba estática no pueden cumplir con los requisitos de profundidad de prueba. Para resolver el problema de la profundidad de verificación, debemos introducir la verificación formal. Pero hay algunos tipos de formas de PI que las herramientas formales no pueden reconocer. Estos incluyen PI de caja negra, PI encriptada y PI de lista de conexiones en el modelo SOPC. Además, la explosión del espacio de estados causada por la enorme escala del modelo SOPC no se puede verificar formalmente. En este documento, proponemos un método de modelado utilizando la arquitectura SOPC. El modelo resuelve el problema de las herramientas formales que no reconocen IPs de múltiples formas. Para comprimir el espacio de estados, proponemos reducir variables SOPC y relaciones de rama basadas en propiedades de verificación. Luego, realizamos un experimento de verificación de propiedades en el modelo SOPC reducido. El resultado del experimento muestra que el modelo puede reducir significativamente el tiempo de verificación.