Copyright © 2026 Authors retain the copyright of this article. This article is an open access article distributed under the Creative Commons Attribution License which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.

@article{183283,
        author = {Aparna Mohan},
        title = {Reusable Formal IP for Digital Control Verification},
        journal = {International Journal of Innovative Research in Technology},
        year = {2025},
        volume = {12},
        number = {3},
        pages = {1553-1562},
        issn = {2349-6002},
        url = {https://ijirt.org/article?manuscript=183283},
        abstract = {Reusable formal IP for digital control verification is a growing research area at the intersection of embedded systems, formal methods, and control theory. As digital control mechanisms become more complex and safety-critical—particularly in domains like renewable energy, automotive systems, and robotics—the limitations of simulation-based verification have led to increased reliance on formal methods. This review examines the key methods, architectures, and tools proposed over the last decade to develop and integrate formally verified reusable IP blocks into digital controllers. Through a detailed analysis of theoretical frameworks, block diagrams, experimental validations, and academic contributions, we identify major trends and emerging techniques such as contract-based design, SMT solvers, and AI-assisted verification. We also discuss future directions involving runtime verification, hybrid AI-control integration, and standardized repositories. The review concludes that reusable formal IPs offer a scalable and certifiable path for verifying digital controllers in modern embedded systems.},
        keywords = {Reusable IP, Formal Verification, Digital Control Systems, Embedded Systems, SMT Solvers, Runtime Verification, PID Controller, Cyber-Physical Systems, Property Specification Language, AI-Assisted Verification},
        month = {August},
        }