Research Interests

Formal methods for the design and verification of digital-hardware systems at the register-transfer level and above.

Research Summary

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 datapath 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 supercomputers.

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 microprocessr 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)

Biographical Summary

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.