Modular Verification of RTL Processors Against ISA Contracts (MIT, Google, UW)

Researchers from MIT, Google, and University of Washington published a technical paper titled “Granite: A Modular Methodology for Foundational Verification of Hardware-Software Leakage Contracts.” Abstract Excerpt: “Granite is a methodology for modular verification of both functional correctness and nonleakage of RTL processors against ISA contracts. We prove that the cycle-by-cycle timing of a pipelined RISC design–with speculation, precise interrupts, and I/O–is determined solely by observable