Leveraging AI-Driven Methods for Optimized Formal Verification of Generated Properties in SoC Components
Lamia Eljadiri, Ismail Assayad, Tarik Nahhal · 2025
Over the last decade, formal verification* has become a crucial method in the design and analysis of embedded systems* and critical architectures. It enables the early detection of errors and the validation of complex properties-particularly those expressed through LTL temporal formulas*-for both software and hardware components. This paper presents the SysVerPml framework*, which introduces an innovative methodology for verifying embedded system properties through the integration of Artificial Intelligence Models*. The framework incorporates Supervised Machine Learning* techniques-such as LightGBM, CatBoost, and Decision Trees-to classify IP components based on temporal/functional properties and to optimize the design space after formal verification. SysVerPml supports the construction of abstract models and employs reduction strategies while preserving process semantics. It enables the verification of predefined generic safety properties of subarchitectures during the design phase, allowing these results to be applied across future architectural prototypes and significantly reducing verification overhead. Our multi-phase methodology offers a promising path for improving verification efficiency and adaptability across reused sub-architectures. We validate the effectiveness of our approach through comparative analysis with tools such as SMV and UPPAAL, demonstrating notable improvements in speed and accuracy. Additionally, we review prior research related to the co-design and verification of intelligent embedded systems using AI techniques. Looking ahead, our objective is to identify Intelligent Components* within preverified SoC* modules and define their corresponding Artificial Intelligence Models, paving the way for more adaptive and automated verification workflows.