B.S., California Institute of Technology (1981); M.Sc., Princeton University (1988); Ph.D., Princeton University (1993); Senior Engineer, ESL Inc. (1982-1985); Visiting Lecturer, Aarhus University (1985-1987); Assistant Professor, University of British Columbia (1992-1997); Associate Professor, University of British Columbia (1997-).
VLSI Design and Verification
I am developing models and tools for verifying that circuits as modeled by non-linear, ordinary differential equations correctly implement digital behaviours. Part of this is developing a 'topology of discrete behaviour'. A complementary part is developing symbolic and numerical tools for verifying that real designs actually behave as intended. This work contributes to making designs reliable and provides insight that leads to higher performance design.
I strongly believe that verification must be complemented by implementation. In recent years, implementations have taken the form of a proof-of-concept chip for STARI, a high-performance communication protocol, design of a controller for a computer controlled model train, and design of a high performance arbitration circuit. I'm currently working on designs for high-speed pipelines and clock distribution networks.
I have been developing techniques for verifying that a circuit in a continuous model correctly implements a discrete specification. This involves finding invariant sets of systems of non-linear differential equations corresponding to CMOS circuits. In the next four years, I will to apply these techniques to a wider range of designs including high-speed CMOS circuits and system-level interconnect. I will also explore applications of these methods to other engineering domains such as embedded controllers for internal combustion engines and rules for free-flight air traffic control.
Lightweight Theorem Proving
With my students, I have developed a lightweight theorem prover that allows the combination of deductive theorem proving with heuristic decision procedures in an intuitive framework. Our initial success with this approach motivates further exploration. In particular, I am interested in incorporating decision procedures for timed automata and our reachabilty procedures for systems modeled by differential equations.
Greenstreet, M., "Reachability Analysis Using Polygonal Projections", with Ian Mitchell. Proceedings of the 2nd International Workshop on Hybrid Systems: Computation and Control, pages 103-116, March 1999.
Greenstreet, M. "A Light-Weight Framework for Hardware Verification", with Christoph Kern and Tarik Ono-Tesfaye. Proceedings of TACAS'99, pages 330-344, March 1999.
Greenstreet, M., "Self-Timed Meshes are Faster Than Synchronous", with Peggy B.K. Pang. Proceedings of Async97, pages 30-39, April 1997.
Greenstreet, M., "Implementing a STARI Chip". Proceedings of ICCD'95.