Verification-Aware Microarchitecture

Duke University Department of Electrical and Computer Engineering

Directed by Prof. Daniel J. Sorin

 

 Objective 

 

Our goal is to design microarchitectures such that they can be more easily verified with existing formal verification methodologies.  Verification currently consumes the majority of resources in the development of a new processor, and yet current processors are still shipped to customers with dozens of subsequently discovered and documented design bugs.  Rather than design a processor for performance, power-efficiency, reliability, etc., and then, once the design is complete, "throw it over the wall" to the verification team, our goal is to treat verification effort as a first-class design constraint.  Specifically, we are exploring how to design processors such that they are more amenable to formal verification, particularly with model checking.

 

 Publications

 

Daniel J. Sorin, Opeoluwa Matthews, and Meng Zhang.  "Architecting Dynamic Power Management to be Formally Verifiable."  Design Automation Conference (DAC), June 2014.

Meng Zhang, Jesse D. Bingham, John Erickson, and Daniel J. Sorin.  "PVCoherence: Designing Flat Coherence Protocols for Scalable Verification.20th International Symposium on High Performance Computer Architecture (HPCA), February 2014.  Best Paper Award

Opeoluwa Matthews, Meng Zhang, and Daniel J. Sorin. "Scalably Verifiable Dynamic Power Management.20th International Symposium on High Performance Computer Architecture (HPCA), February 2014.

Meng Zhang, Alvin R. Lebeck, and Daniel J. Sorin. "Fractal Consistency: Architecting the Memory System to Facilitate Verification." Computer Architecture Letters, volume 9, number 2, July-December 2010.

Meng Zhang, Alvin R. Lebeck, and Daniel J. Sorin. "Fractal Coherence: Scalably Verifiable Cache Coherence. To appear in 43rd International Symposium on Microarchitecture (MICRO), December 2010.

Meng Zhang, Anita Lungu, and Daniel J. Sorin. "Analyzing Formal Verification and Testing Efforts of Different Fault Tolerance Mechanisms." 24th IEEE International Symposium on Defect and Fault Tolerance in VLSI Systems, October 2009.

Anita Lungu, Pradip Bose, Alper Buyuktosunoglu and Daniel J. Sorin. "Dynamic Power Gating with Quality Guarantees." International Symposium on Low Power Electronics and Design (ISLPED), August 2009.

Anita Lungu, Pradip Bose, Daniel J. Sorin, Steven German and Geert Janssen. "Multicore Power Management: Ensuring Robustness via Early-Stage Formal Verification." Seventh ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), July 2009.

Anita Lungu, Pradip Bose, Daniel J. Sorin, Steven German, and Geert Janssen. "Multicore Power Management: Ensuring Robustness via Early-Stage Formal Verification." 3rd Workshop on Dependable Architectures (WDA-3), November 2008.

Anita Lungu and Daniel J. Sorin. "Verification-Aware Microprocessor Design." Sixteenth International Conference on Parallel Architectures and Compilation Techniques (PACT), September 2007.

 

 Group

 

Prof. Daniel J. Sorin, Associate Professor of Electrical and Computer Engineering and Computer Science

Anita Lungu

Opeoluwa (Luwa) Matthews

Meng Zhang

 

Funding and Support

 

National Science Foundation grant CCF-0811290