|
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, Anita Lungu, and Daniel J. Sorin. "Analyzing Formal Verification and Testing Efforts of Different Fault Tolerance Mechanisms." To appear in 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 |
|
Meng Zhang |
| Funding and Support |
| National Science Foundation grant CCF-0811290 |
| Links |
| Duke Architecture |
| WWW Computer Architecture Page |
| Duke's Pratt School of Engineering |