Mark Greenstreet

Professor

Relevant Degree Programs

 

Graduate Student Supervision

Doctoral Student Supervision (Jan 2008 - May 2019)
Leveraging distributed explicit-state model checking for practical verification of liveness in hardware protocols (2015)

Protocol verification is a key component to hardware and software design.The proliferation of concurrency in modern designs stresses the need for accurate protocol models and scalable verification tools. Model checking is an approach for automatically verifying propertiesof designs, the main limitation of which is state-space explosion.As such, automatic verification of these designs can quickly exhaustthe memory of a single computer.This thesis presents PReach, a distributed explicit-state model checker, designed to robustly harness the aggregate computing power of large clusters.The initial version verified safety properties, which hold if no error states can be reached.PReach has been demonstrated to run on hundreds of machines and explore statespace sizes up to 90 billion, the largest published to date. Liveness is an important class of properties for hardware system correctnesswhich, unlike safety, expresses more elaborate temporal reasoning.However, model checking of liveness is more computationally complex,and exacerbates scalability issues as compared with safety.The main thesis contribution is the extension of PReach to verify two key liveness-like properties of practical interest:deadlock-freedom and response. Our methods leverage the scalability and robustness of PReach and strike a balance between tractable verification for large modelsand catching liveness violations.Deadlock-freedom holds if from all reachable system states, there existsa sequence of actions that will complete all pending transactions.We find that checking this propertyis only a small overhead as compared to safety checking.We also provide a technique for establishing that deadlock-freedom holds of a parameterized system -- a system with a variable number of entities.Response is a stronger property than deadlock-freedom and is the most common liveness property of interest.In practical cases, fairness must be imposed on system modelswhen model checking responseto exclude those execution traces deemed inconsistent with the expectedunderlying hardware.We implemented a novel twist on established model checking algorithms, to target response properties with action-based fairness.This implementation vastly out-performs competing tools.This thesis shows that tractable verification of interesting liveness propertiesin large protocol models is possible.

View record

Projectagon-based reachability analysis for circuit-level formal verification (2011)

This dissertation presents a novel verification technique for analog and mixed signal circuits. Analog circuits are widely used in many applications include consumer electronics, telecommunications, medical electronics. Furthermore, in deep sub-micron design, physical effects might undermine common digital abstractions of circuit behavior. Therefore, it is necessary to develop systematic methodologies to formally verify hardware design using circuit-level models. We present a formal method for circuit-level verification. Our approach is based on translating verification problems to reachability analysis problems. It applies nonlinear ODEs to model circuit dynamics using modified nodal analysis. Forward reachable regions are computed from given initial states to explore all possible circuit behaviors. Analog properties are checked on all circuit states to ensure full correctness or find a design flaw. Our specification language extends LTL logic with continuous time and values and applies Brockett’s annuli to specify analog signals. We also introduced probability into the specification to support practical analog properties such as metastability behavior.We developed and implemented a reachability analysis tool COHO for a simple class of moderate-dimensional hybrid systems with nonlinear ODE dynamics. COHO employs projectagons to represent and manipulate moderate-dimensional, non-convex reachable regions. COHO solves nonlinear ODEs by conservatively approximating ODEs as linear differential inclusions. COHO is robust and efficient. It uses arbitrary precision rational numbers to implement exact computation and trims projectagons to remove infeasible regions. To improve performance and reduce error, several techniques are developed, including a guess-verify strategy, hybrid computation, approximate algorithms, and so on.The correctness and efficiency of our methods have been demonstrated by the success of verifying several circuits, including a toggle circuit, a flip-flop circuit, an arbiter circuit, and a ring-oscillator circuit proposed by researchers from Rambus Inc. Several important properties of these circuits have been verified and a design flaw was spotted during the toggle verification. During the reachability computation, we recognized new problems (e.g., stiffness) and proposed our solutions to these problems. We also developed new methods to analyze complex properties such as metastable behaviors. The combination of these methods and reachability analysis is capable of verifying practical circuits.

View record

On-chip surfing interconnect (2010)

With growing chip sizes and operating frequencies, on-chipglobal interconnect has become a critical bottleneck for CMOS technology.With processes scaling into deep submicron scales,the gap between gate delay and global-interconnect delay increases witheach technology generation.Bandwidth is also important for on-chip interconnect and is limited by skew and jitter.Due to temperature variation, crosstalk noise, power supply variation and parameter variation, timing variation increases with the length of global interconnect lines.Jitter and skew in the transmitter and receiver's clocks add timing variation to on-chip interconnect communication. Repeaters in a buffering technique amplify clock jitter and drop pulses due to intersymbol interference.Latches can be inserted in place of some of the buffers to control the timing variation.However, these latches increase latency and power consumption. In 2002, a novel circuit technique called ``surfing'' was proposed to boundthe timing uncertainty in wave pipelines~\cite{Winters02}.This thesis extends the application of surfing to on-chipinterconnects and introduces surfing RC interconnect and surfing LCinterconnect techniques.For RC interconnects, we present a jitter attenuating buffer.This buffer uses inverters with variable output strength to implementa simple, low-gain DLL. Chains of these surfing buffersattenuate jitter making them well suited for source-synchronous interconnect.Furthermore, our chains can be used to reliably transmit handshakingsignals and support sliding-window protocols to improve the throughputof asynchronous communication.We use distributed varactors to dynamically vary the latency of LCinterconnects and thus effect surfing.Different from RC signaling, signals on LC interconnect propagate at nearly the speed-of-light.The varactors not only modulate the line latency, but also sharpen the edges of signals.We present both a full-swing and a low-swing LC interconnect designs.In both interconnects, the jitter and skew are attenuated along the line due to the surfing effect.In the low swing interconnect, the surfing effect also helps to reshape the pulses to increase the eye height.To demonstrate these techniques in real silicon, we designed, fabricatedand tested a chip.The testing results show that surfing LC interconnects are promisingfor deep submicron technology.

View record

Master's Student Supervision (2010 - 2018)
Fault tolerance for distributed explicit-state model checking (2014)

PReach, developed at the University of British Columbia and Intel, is a state of the art parallel model checker. However, like many model checkers, it faces reliability problems. A single crash causes the loss of all progress in checking a model. For computations that can take days, restarting from the beginning is a problem. To solve this, we have developed PReachDB, a modified version of PReach. PReachDB maintains the state of the model checking computation even across program crashes by storing key data structures in a database. PReachDB uses the Mnesia distributed database management system for Erlang. PReachDB replicates data to allow the continuation of the computation after a node failure. This project provides a proof-of-concept implementation with performance measurements.

View record

Formal verification of a digital PLL (2014)

Common AMS circuit are composed from blocks that can be modeled accurately using linear differential inclusions to enable verification of important properties using reachability analysis. This dissertation presents a formal verification of Digital Phase Locked Loop (PLL) using reachability techniques. PLLs are ubiquitous in analog mixed signal (AMS) designs and are widely used in modern communication equipment, clock generation for CPUs in computers, clock-acquisition in high-speed links etc. The most important property of a PLL is convergence, which means starting from any possible initial conditions, the PLL will eventually lock to the desired equilibrium. We model the digital PLL as a set of Ordinary Differential equation (ODEs), and discretize the weakly non-linear ODEs to linear differential inclusions. The transformation not only provides us an over approximation of the verification problem but also provides the basis for a sound proof. We present the verification of a digital PLL using real tools, SpaceEx and Coho. In particular, we show how each component of the digital PLL can be modelled as a hybrid automaton. Due to the large number of transitions caused by the model, the whole proof is established by several lemmas. Interesting problems such as a timing glitch in the Phase Frequency Detector (PFD) are discussed and triggering conditions are formally proved in the dissertation. Global convergence is demonstrated by both tools. Based on the digital PLL circuit and the challenges that arose during our verification, the error bounds, limitations, implementation differences and usability of the two leading tools are carefully evaluated. SpaceEx provides a graphical user interface that makes it easy to get started with simple examples but requires extensive user interaction for larger problems. The interface to Coho is a MATLAB API. While this lacks the packaged-tool feel of SpaceEx, it provides a flexible way to break a large verification problem into smaller lemmas and allows the proof to be ''re-executed'' simply by re-executing the MATLAB script.

View record

 

Membership Status

Member of G+PS
View explanation of statuses

Program Affiliations

 

If this is your researcher profile you can log in to the Faculty & Staff portal to update your details and provide recruitment preferences.