In this talk, I will reveal what our research group has learned about formally verifying microprocessor designs. Where do current approaches fall short? What special characteristics of the designs can we exploit? What new methods might help? And, what are the prospects for this work producing a useful result?
About the speaker:
David L. Dill is Associate Professor of Computer Science and, by courtesy, Electrical Engineering at Stanford University. He has been on the faculty at Stanford since 1987. He has an S.B. in Electrical Engineering and Computer Science from the Massachusetts Institute of Technology (1979), and an M.S and Ph.D. from Carnegie-Mellon University (1982 and 1987).
His primary research interests relate to the theory and application of formal verification techniques to system designs, including hardware, protocols, and software.
Prof. Dill's Ph.D. thesis, "Trace Theory for Automatic Hierarchical Verification of Speed Independent Circuits" was named as a Distinguished Dissertation by ACM and published as such by M.I.T. Press in 1988. He was the recipient of an Presidential Young Investigator award from the National Science Foundation in 1988, and a Young Investigator award from the Office of Naval Research in 1991. He has received Best Paper awards at International Conference on Computer Design in 1991 and the Design Automation Conference in 1993. He was a visiting professor during the summer of 1996 at Intel in Hillsboro, Oregon (where he learned how many orders of magnitude short of being able to verify the Pentium Pro he was). From July 1996 to September 1997 he was Chief Scientist (and one of the founders) of 0-In Design Automation, a start-up that is developing verification tools that combine conventional simulation and formal verification technology.
Contact information:
David L. Dill
Gates Bldg 3A, Rm. 344
Stanford University
Stanford CA 94305-9030
(650) 725-3642
(650) 725-6949
dill@cs.stanford.edu