Mark Aagaard

Biography

"I'm an Associate Professor in the Electrical and Computer Engineering Dept at the University of Waterloo. I arrived here by a rather circuitous route: I was born and raised in Southern California, where I spent many weekends and summer vacations hiking and backpacking through the San Gorgonia Mountains, Mt Baldy, Mt San Jacinto, and Sierra Nevadas. I earned a Bachelors in Engineering from Harvey Mudd College, very unbiasedly regarded as one of the best undergraduate schools in North America. For graduate school, I went to the Electrical and Computer Engineering Dept at Cornell University where I earned my Masters and Doctorate working with Miriam Leeser. While at Cornell, I spent a great deal of time in the Computer Science Dept, working with the Nuprl proof system and Bob Constable's research group. For my Masters, I used Nuprl to verify a logic synthesis program that was based on the Boolean Division algorithm used in the Berkeley CAD tool MIS. In my PhD I developed a framework for specifying, designing and verifying pipelined circuits that have structural hazards. Structural hazards are common; especially in high-performance, superscalar microprocessors. They greatly complicate pipeline design and verification and can lead to problems with execution ordering, loss of instructions, generation of bogus instructions, and termination. After finishing up at Cornell, I spent a year and a half as a PostDoc working for Carl Seger in the Computer Science Dept at the University of British Columbia. With Carl Seger, I worked on combining the symbolic trajectory evaluation model checking algorithm with theorem proving. We implemented and verified an IEEE compliant, double precision, pipelined floating-point multiplier. Carl is currently leading the Forte formal verification group at Intel, in Hillsboro, Oregon. I joined Intel in 1996, and spent almost five years there, first as part of Carl's group working on Forte, and then using Forte to verify control circuits in the back end of the Willamette (Pentium(R) 4) processor. I joined the Electrical and Computer Engineering Dept at the University of Waterloo in January of 2001, where I am currently a faculty member and am continuing to do research on hardware verification and design."

Research Interest

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.