Phone: 519-888-4567 x33138
Location: EIT 4138
- BSc, Harvey Mudd
- MSc, Cornell University
- PhD, Cornell University
My area of research is formal methods for the design and verification of digital-hardware systems at the register-transfer level and above. Specifically, I have developed a formal theory for pipelined circuits that is based on the conventional notions of structural hazards, control hazards, data hazards, and data path functionality. My current research activities use different aspects of my formalization of pipeline hazards to explore new design and verification techniques for different classes of hazards.
Formal methods use mathematics and logic to model the structure and behaviour of systems. Conventional verification techniques require generating and simulating individual test cases. Formal methods evaluate all test cases simultaneously, thereby greatly increasing the confidence that a system works correctly. Pipelining is an optimization technique for digital-hardware systems that increases performance by overlapping the execution of multiple instructions, analogous to the way that automobiles flow through an assembly line. Pipelining is used on almost all digital-hardware systems, ranging from simple signal-processing filters up to high-performance super computers.
Some recent research projects include:
- Verified data-hazard correctness for a high-level model of Dual-RAT register renaming, a pipeline performance optimization based on the Intel Pentium 4 processor. (With Hazem Shehata)
- Invented a technique that exploits the power and usability of an off-the-shelf combinational equivalence checker to solve the obligations arising from the completion-functions verification strategy. (With Vlad Ciubotariu, Jason Higgins, and Farzad Khalvati)
- Developed a prototype design and verification tool that includes a cell library of control components for pipeline stages, a graphical interface for constructing pipelines, and an automated connection to verify structural-hazard properties on commercial equivalence checkers and model checkers. (With Jason Higgins)
- Created the Microbox framework for microprocessor correctness statements, where we analyzed over 30 published verification results and proved conditions under which different correctness statements are equivalent. (With Nancy Day and Robert Jones)
- Mark D. Aagaard, Nancy A. Day, and Meng Lou, "Relating Multi-step and Single-step Microprocessor Correctness Statements," in Formal Methods in Computer-Aided Design (FMCAD). LNCS, Volume 2517, Springer Verlag; New York, November, 2002, pp. 123-141.
- Mark D. Aagaard, Byron Cook, Nancy A. Day, and Robert B. Jones "A Framework for Microprocessor Correctness Statements," CHARME 2001, LNCS, Volume 2144, Livingston, Scotland, Sept 4-7, 2001.
- Nancy A. Day, Mark D. Aagaard, and Byron Cook. "Combining stream-based and state-based verification techniques for microarchitectures." In Warren Hunt and Steve Johnson, editors, Formal Methods in Computer-Aided Design (FMCAD). LNCS, Volume 1954, Springer Verlag; New York, November 2000.
- Mark D. Aagaard, Robert B. Jones, John W. O'Leary, Carl-Johan H. Seger, and Thomas F Melham. "A methodology for large-scale hardware verification." In Warren Hunt and Steve Johnson, editors,Formal Methods in Computer-Aided Design (FMCAD). LNCS, Volume 1954, Springer Verlag; New York, November 2000.
- Robert H. Beers, Rajnish Ghughal, and Mark D. Aagaard. "Applications of hierarchical verification in model checking." In Warren Hunt and Steve Johnson, editors, Formal Methods in Computer-Aided Design (FMCAD). Springer Verlag; New York, November 2000 (appears in CHARME 2001 proceedings).
Please see Professor Aagaard's own web page for more information.