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.
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