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

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

Meng Zhang

Funding and Support
National Science Foundation grant CCF-0811290

 

 Links
Duke Architecture
WWW Computer Architecture Page
Duke's Pratt School of Engineering