# Mark Greenstreet's Research

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.

## Formal Verification

### Analog and Mixed-Signal Circuits

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.

### Model Checking

Working Brad Bingham (now at IBM) and collaborators at Intel, we developed PReach, a parallel, explicit-state model checker [Bingham10]. PReach can utilize the combined memory of hundreds of machines to check properties of modes with billions of states. In addition to checking safety properties, PReach supports efficient techniques for proving response properties [Bingham14] and deadlock freedom [Bingham11], [Bingham13]. You can get Brad's Ph.D. thesis here.

### Reachability for AMS and cyber-physical systems

Working with Ian Mitchell, we developed the first version of Coho, a reachability tool that pioneered the use of projection based methods for approximating reachable regions in high-dimensional spaces. We have extended this work with Chao Yan to demonstrate that such methods can verify properties of non-linear circuits including oscillators [Yan12], flip-flops [Yan07], arbiters [Yan10], and asynchronous C-elements [Yan11]. Coho is available from github here. you can get Chao's Ph.D. thesis here.

## VLSI Design

### Crossing Clock Domains

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.

### Synchronizer Analysis

Large chips are partioned into many clock domains, both internally and for I/O. It is well-known that it is impossible to communicated between two synchronous circuits with independent clocks with absolute guarantees of correctness [Marino81]. However, the failure probability can be made aribtrarily small. For high-reliability applications, the failure probability per synchronization may need to be 1025 or lower. With Suwen Yan, we developed a novel algorithm that makes it practical to determine these failure probabilities to ensure that synchronizers are adequate to meet design requirements [Yang07a, ]. This algorithm has become the standard for synchronizer analysis and is used, for example, tools from Blendics.

Power consumption is now one of the main constraints on chip design and performance. For mobile devices, power consumption determines battery life. For desktop computers and large servers, power dissipation limits performance. There is a direct connection between speed and energy consumption: if a processor is slower, it can be designed to use much less energy per operation. In particular, a parallel implementation of an algorithm may use many, slower processors to perform a task faster and with less energy than a single processor. With Brad Bingham, Vijay Korthikanti, and Gul Agha, we showed fundamental limits in a simple, theoretical model for energy-time trade-offs [Bingham12], and for higher-level models of shared-memory multiprocessors [Korthikanti11].