A Half-Day Hands-On Tutorial
About
Verification is a critical bottleneck in hardware design. According to a 2024 Siemens study, critical bugs escape to silicon in over 85% of IC/ASIC design projects despite verification consuming over 50% of design effort. The root cause is twofold: modern computer hardware is highly complex, and rigorous verification today relies on manual property writing by formal methods experts—an arduous process that limits scalability and accessibility.
The standard approach to formally verifying that a hardware implementation upholds its design specifications is top-down: engineers manually translate abstract design requirements into detailed formal properties over design signals, then use formal tools—especially model checkers—to verify them. Initial translations typically yield complex, hard-to-prove properties. Verification engineers spend significant time manually decomposing the design and properties to increase proof bounds. Yet bounded proofs, covering a finite execution depth in cycles, remain common in industrial practice.
This tutorial introduces a novel suite of approaches and tools for automatically and scalably verifying that hardware upholds important hardware-software contracts—including its memory consistency model, cache coherence protocol, and leakage contract for side-channel security (e.g., Arm DIT, Intel DOIT, RISC-V Zkt). These tools require no manual property writing; they take modest design metadata familiar to hardware designers without any formal expertise.
We implement a bottom-up verification approach: many simple formal properties are automatically generated from templates and static analysis of the design under verification, then checked against it to synthesize a formally verified specification. This strategy automatically decomposes complex top-down properties into many simple ones, most of which admit unbounded proofs.
These automated verification approaches have been successfully deployed on industry CPU modules and recognized with a Sloan Reserach Fellowship, an NSF CAREER Award, the Intel 2024 Rising Star Award, the Intel 2023 Outstanding Researcher Award, and a keynote at Cadence's major formal verification conference JUG'25. Multiple major hardware companies have expressed interest in deploying these tools on commercial designs and at least one has done so. By automating the labor-intensive property-writing process, these methods democratize access to rigorous verification, enabling broader adoption of formal methods in hardware design.
Schedule
This hands-on tutorial requires no prior formal verification experience. Attendees will use open-source tools integrated with commercial model checkers to verify adherence of open-source hardware designs to important hardware-software contracts. Each phase pairs conceptual foundations with hands-on exercises.
Open Source
Automatically synthesize formally-verified per-instruction microarchitectural execution paths from RTL for functional verification and to enable downstream verification tasks.
GitHub RepositoryAutomatically synthesize formally-verified memory consistency model specifications from RTL, enabling automated verification of RTL MCM implementations.
GitHub RepositoryAutomatically synthesize formally-verified leakage contracts from RTL, enabling automated verification of RTL implementations of Arm DIT, Intel DOIT, and RISC-V Zkt, and more.
GitHub RepositoryQuantify microarchitectural side-channel leakage with probabilistic guarantees, complementing formal leakage contract synthesis with quantitative analysis.
GitHub RepositoryAutomatically synthesize formally-verified cache coherence protocol specifications from Murphi implementations, enabling verification of coherence protocol correctness.
GitHub repository coming soonResearch
Helium: Quantifying Microarchitectural Side-Channel Leakage with Probabilistic Guarantees
In Proceedings of the 53rd International Symposium on Computer Architecture (ISCA), June 2026.
PDF link coming soonRTL2MµPATH: Multi-µPATH Synthesis with Applications to Hardware Security Verification
In Proceedings of the 57th IEEE/ACM International Symposium on Microarchitecture (MICRO), November 2024.
PDFAxiomatic Hardware-Software Contracts for Security
In Proceedings of the 49th International Symposium on Computer Architecture (ISCA), June 2022.
PDFConsistency-Directed Formal Verification of Cache Coherence Protocol Implementations
PDF link coming soonOrganizers
Ph.D. Student, Stanford University
Yao Hsiao is a Ph.D. student at Stanford University advised by Prof. Caroline Trippel. Her research focuses on the development of automated methodologies and tools for formally verifying processor implementations of cache coherence, memory consistency, and side-channel security features.
Ph.D. Student, Stanford University
Samantha Archer is a 3rd-year Ph.D. student at Stanford University advised by Prof. Caroline Trippel. Her research focuses on the formal verification of hardware, with an emphasis on microarchitectural side-channel verification. Her work aims to help programmers more precisely reason about the risk of security-critical software leaking information through hardware side channels.
Assistant Professor, Stanford University
Caroline Trippel is an Assistant Professor in the Computer Science and Electrical Engineering Departments at Stanford University. Her research fits broadly in the area of computer architecture and focuses on promoting high assurance—correctness, security, and reliability—as a first-order computer architecture design goal. A central theme is leveraging automated reasoning and formal methods to design and verify hardware systems. Her work has influenced the RISC-V ISA memory consistency model, prompted Intel to update their Software Security Guidance, and produced methodologies that synthesized new variants of Meltdown and Spectre attacks. Trippel's research has been recognized with IEEE Top Picks distinctions, an NSF CAREER Award, the inaugural Google ML and Systems Junior Faculty Award, the Intel Rising Star Faculty Award, an Intel Outstanding Researcher Award, the 2020 ACM SIGARCH/IEEE CS TCCA Outstanding Dissertation Award, and the 2020 CGS/ProQuest Distinguished Dissertation Award in Mathematics, Physical Sciences, & Engineering.
Acknowledgments