My research is broadly in the areas of formal verification and VLSI design. In both, I'm particularly interested in problems involving real numbers including analog circuit verification; reachability problems for circuits and cyber-physical systems; performance analysis; and theorem proving and decision procedures with polynomials, and differential equations. These have applications in many areas, which has led, for example to my teaching our parallel computation course and using parallel computing in formal verification.
We can now design and manufacture integrated circuits with over one billion transistors. These provide the functionality for desktop and laptop computers, cellphones, tablets, internet servers, along with chips that are embedded in other devices such as engine controllers, cameras, drones, and medical devices. While most of the circuits on these chips are digital, putting complete systems on a chip also requires analog functionality. Analog functions include sensors (e.g. audio and video input and output, accelerometers for motion detection, vibration cancellation, and determining screen orientation, etc.), wireless interfaces, clock generation, power management, high-speed interconnect within and between chips, and so on. While analog circuits comprise a small fraction of the chip, they consume a large amount of design effort. They are often critical for performance, and a failure of a circuit can completely block further testing of a chip, for example, if the clock generator or a critical I/O interface fail to work.
I apply formal methods to the problem of verifying analog, and mixed analog/digital, often called “analog mixed-signal” (AMS) designs. As advanced by [Kim09], we take the view that AMS circuits usually have linear behaviour when they are in their intended operating region. Thus, we are interested in showing that an AMS circuit will always converge as intended. For example, researchers at Rambus posed a question from an actual design failure of “When can an oscillator be guaranteed to start correctly?” [Jones08]. We were the first to answer this challenge problem with [Greenstreet08]. More recently, we have shown that we can apply such methods to a state-of-the-art phase-locked loop [Crossley10] -- see [Wei13], [Peng15].
We are now looking at extending these methods to larger subsystems such as power distribution networks and high-speed serial links. We are also looking at extending our work downward into automatic generation of simulation test cases to check transistor-level designs against their higher-level models, and relieve AMS designers of manually performing hundreds of simulations to validate their designs. We use develop and use methods for reachability analysis, SAT solvers and other decision procedures, theorem-proving, numerical optimization, and circuit modeling and analysis.
In my Ph.D.\ research I developed the STARI (self-timed at receiver's input) protocol for mesochronous communication [Greenstreet90, Greenstreet93]. (Note: David Messerschmidt made a similar proposal concurrently and independently [Messerschmitt90]). I proved the correctness of the approach including its freedom from synchronization failures, and implemented a proof-of-concept chip [Greenstreet95]. Mesochronous designs are now widely used, for example, in high-bandwidth DDR memory interfaces.
I have continued to have an interest in efficient synchronization circuits including [Chakraborty03] and [Yang11] -- both papers won the Best Paper Award in their respective years at the ASYNC Symposium.