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)
Please see Professor Aagaard's own web page for more information.