Modelling Peripheral Designs using FSM-like Notation for Complete Property Set Generation

As the complexity of System-on-Chips (SoCs) continues to increase, there is a growing need for new and effective design, modeling, and verification methods to produce high-quality designs. To address this challenge, this paper proposes a trace-based approach for generating a complete set of formal properties that can be used to formally verify designs. The proposed approach employs FSM-like notations to model the sequential behavior of designs, including timing information between state transitions. This enables the generation of formal properties that capture all necessary design details. The approach has been applied to several industry-level designs, demonstrating its practicality and effectiveness. Experimental results show that the proposed approach significantly reduces the manual effort required for design verification, while simultaneously identifying several complex bugs that would have otherwise been difficult to detect. Overall, the trace-based approach presented in this paper represents a promising step towards addressing the design and verification challenges posed by increasingly complex SoCs.