Collaborative Research: FMitF: Track I: AVA: Architectural Insights For Formal Verification Of Computer Architectures

Formal verification has made a significant impact on hardware verification. Even though hardware formal verification tools available through EDA (Electronic Design Automation) companies and open source are widely used in industrial and research practice, these tools face significant scalability and usability challenges. Specifically, there is no framework that makes these techniques available to architects and hardware designers for direct use and subsequent integration with existing hardware verification flows. The project's novelties are to address these challenges by leveraging architectural insights in a systematic way to make formal verification scalable and usable by computer architects. The project's impacts are the advancement of both functional and security verification for contemporary architectures, and formal verification techniques for synthesis of invariants and information leakage verification via abstraction-refinement. The overarching theme of the project is the use of architectural insights in lifting important formal verification techniques to be directly usable by computer architectures. Specifically, the project involves four tasks: 1) developing architecture-driven abstractions, component interfaces, and invariants for functional verification of complex processors using modular-refinement-based techniques; 2) leveraging architectural insights to derive shadow logic (monitors) and abstraction/refinement schemes for taint analysis, for security verification of software-hardware contracts; 3) developing new formal verification methods for synthesis of architecture-driven invariants and information-leakage verification via abstraction-refinement; 4) developing an open-source prototype framework with the above techniques built-in to be integrated with existing hardware verification flows and tools. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.