Mark Greenstreet

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.

Hybrid Systems
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.