Sat 17 Jun 2023 14:50 - 15:00 at Magnolia 4 - PLARCH: Session 3 Chair(s): Caroline Trippel

As we go from thousand-transistor designs to trillion-transistor designs, many breakthroughs were made in architecture, physical design and physical process. However, verification methodology remains stagnant, much the same as twenty years ago. To this end, we must shift our focus from agile hardware design to agile hardware verification. In this paper, we present NFC, a framework for formal verification tailored for high performance cache designs. With NFC, users could quickly build a formal verification infrastructure that finds bugs in corner case scenarios with a short turn-around time and builds confidence in cache designs. We show that our framework was able to find 8 bugs in a multi-banked non-blocking out of order data-cache within a single hour.

Sat 17 Jun

Displayed time zone: Eastern Time (US & Canada) change

14:00 - 15:30
PLARCH: Session 3PLARCH at Magnolia 4
Chair(s): Caroline Trippel Stanford University

#plarch-sat-magnolia4 Discord icon small YouTube icon small

14:00
15m
Talk
They're the same picture: a software-verification flow adapted for hardware verification
PLARCH
Andreas Lööw Imperial College London, Magnus O. Myreen Chalmers University of Technology
Pre-print
14:15
15m
Talk
Design for Hardware Memory Model Verification
PLARCH
Yao Hsiao Stanford University, Yasas Seneviratne University of Virginia, Tommy Tracy II University of Virginia, Kevin Skadron University of Virginia, Caroline Trippel Stanford University
File Attached
14:40
10m
Talk
Nerv: Probabilistic Dynamic Partial Order Reduction for Hardware
PLARCH
Tianrui Wei University of California, Berkeley, Shangyin Tan University of California at Berkeley, Koushik Sen University of California at Berkeley, Krste Asanovic University of California Berkeley
14:50
10m
Talk
NFC:Next-generation Formal verification for high performance Caches
PLARCH
Tianrui Wei University of California, Berkeley, Jerry Zhao UC Berkeley, Krste Asanovic University of California Berkeley
15:00
10m
Talk
Sandia's Formal Hardware Design and Verification, Present and Future
PLARCH
Noah Evans Sandia National Laboratories
15:10
10m
Talk
Silver Oak: Hardware Software Co-Design and Co-Verification in Coq
PLARCH
Ben Blaxill Groq, Samuel Grütter Massachusetts Institute of Technology, Jade Philipoom Google, Germany, Satnam Singh Groq