Digital-system designers rely upon a hierarchy of abstractions that allow them to treat complex collections of transistors as single modules. These abstractions range from switch-level models, to Boolean algebra, to the register-transfer level. An increasingly urgent challenge is to find an abstraction above the register-transfer level that is effective in improving design and validation techniques.
Today, digital-system design proceeds primarily by evolution and validation is done almost entirely by simulation. A deeper understanding of the structure and behavior at the microarchitectural level will make design and validation more systematic and productive. My focus is pipelining, a pervasive and complex microarchitectural optimization. A solid mathematical foundation for pipelined circuits will provide system designers and tool developers with a coherent set of rules that will both open up new regions of the design space for exploration and prevent straying into unsound regions.
Current research is supported by: Intel, SRC, CFI, OIT, NSERC.
I'm looking for students at all levels who are interested in challenging and exciting research projects and theses. Below, I've listed a variety of potential projects and theses at different levels, many other topics are also possible.
The plan is to design and build a pipelined microprocessor based on the ubiquitious DLX . Our goal is to explore high-level design techniques that will result in a concise and robust VHDL implementation that does not sacrifice the traditional metrics of performance, area, and power. This work will also serve as a vehicle for additional research on verification, digital system design, and computer architecture.
Each of projects listed below are is one of the more challenging components of a microprocessor. Designing such a componenent will provide insight into the architecture of modern microprocessors and the design cycle from conception to silicon.
Pipelining is a common microarchitectural optimization in digital systems. Pipelining can improve the performance of a machine, but it also complicates the design and introduces many sources of bugs. A goal of our research is to develop techniques that enable designers to achieve their goals of low power, high performance, and small area while reducing the effort it takes to debug their circuits.
Pipelines add three sources of potential bugs to a circuit: structural hazards, control hazards, and data hazards. The plan is to attack each of these hazards in turn, beginning with structural hazards and working our way up to data hazards, which are the most complex. For each type hazard, we will begin by exploring how real pipelined circuits handle their hazards and then branch out in two directions: CAD tools to design pipelines and techniques to verify pipelines.
Most designers don't want to be encumbered with the mathematics of formal verification. One way to make it easier for people to use the results of formal verification is to pre-verify results that can then be used over and over again. The goal of this project is to identify common mechanisms for dealing with structural hazards in pipelines, and then verify generic instances of the mechanisms. The following three topics tackle each of the three types of hazards in pipelines. Some initial work on structural hazards has already been done.
Another way to make it easier for designers to use the results of formal verification is to build formal methods into the CAD tools. The following two projects investigate CAD tools that prevent designers from making mistakes without sacrificing the traditional design goals of performance, area, and power.
A PhD thesis offers an opportunity to explore a topic in depth and do ground-breaking research in that area. A strong thesis will combine practical results with solid mathematical foundations --- both advancing the state of the art and providing ideas for industry to explore. PhD topics are necessarily open ended, which makes them both exciting and challenging. The topics listed here are very general, students student can tailor any of them to suit their own interests and talents.
In my own PhD, I focussed on structural hazards in pipelines, and so have listed control and data hazards as two possible topics here.
Another long-term interest of mine is combining different verification techniques. The Forte verification system, which I helped develop at Intel, combined symbolic trajectory evaluation and theorem proving and was used successfully on many large and complicated circuits. Having demonstrated this combination works well in practice, we now need to strengthen the connection between the two techniques. This involves both mathematical reasoning about the semantics of symbolic trajectory evaluation and tool building to demonstrate the practicality of the approach.
The continued advances in computer architecture provide a never-ending supply of verification challenges. Here are a few micro-architectural ideas that have been proposed in academia or used in industry that pose interesting verification questions.