Mark Greenstreet
Relevant Thesis-Based Degree Programs
Affiliations to Research Centres, Institutes & Clusters
Graduate Student Supervision
Doctoral Student Supervision
Dissertations completed in 2010 or later are listed below. Please note that there is a 6-12 month delay to add the latest dissertations.
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
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
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
Theses completed in 2010 or later are listed below. Please note that there is a 6-12 month delay to add the latest theses.
Reactive programs are programs that process external events, such as signals andmessages. Device drivers and cloud microservices are examples of reactiveprograms. Systems built from reactive programs are concurrent and exhibit a highdegree of nondeterminism, making non-exhaustive testing inadequate. Ahigher-level language can be used to write a specification: a formal definitionof a program’s desired behaviour. Such specifications may be easier to reasonabout, but proofs of the specification say nothing of a low-levelimplementation.Program synthesis is one way to bridge this gap. A synthesizer searches a spaceof candidate programs for an implementation that satisfies the specification. Ingeneral, the number of candidate programs is infinite, making synthesisundecidable. Even a bounded search, e.g., on program length, soon becomesintractable as that search space grows exponentially.This work introduces COMET, a system for synthesizing reactive programs fromunbounded nondeterministic iterative transformations (UNITY) specifications.Recent work in symbolic execution and solver-aided synthesis has advanced thestate of the art, but symbolic techniques also lead to exponential blowup.COMET seeks to avoid exponential blowup by constraining the search space andsynthesizing in small steps. COMET synthesizes non-trivial programs forsequential and concurrent languages by applying three techniques: symbolicexecution of the specification into guarded traces, intermediate target tracesynthesis, and recursive synthesis of target expressions. To evaluate thisapproach, I synthesize Arduino and Verilog programs from UNITY specifications ofthe Paxos consensus proposer and acceptor roles.
View record
In 2007, Yang and Greenstreet presented an algorithm that enables the computationof synchronizer failure probabilities, even when these probabilities are extremelysmall. Their approach gives a single probability number for the synchronizer butdoes not explain how the circuit details within the synchronizer contributes to thefinal result. We present an extension of their algorithm that connects the time-to-voltage gain of a synchronizer to the propagation of metastability through synchronizer circuits. This allows the designer to see what circuit features are helpful ornot for synchronizer performance. There exists abundant folklore about what helpsor hinders multistage synchronizer performance. We use our analysis to examineand explain such synchronizer folklore and draw novel conclusions. A brief erroranalysis is presented to provide evidence that the machinery used to compute ournew measure of synchronizer effectiveness is accurate. The tools are exercised toobjectively evaluate a handful of industry used synchronizer designs in order tocompare their effectiveness against one another.
View record
We present a formal first-order theory of arbitrary dimensional real vector spaces in ACL2(r). This includes methods for reasoning about real vectors, metric spaces, continuity, and multivariate convex functions, which, by necessity, involves the formalisation of a selection of classically significant and useful mathematical theorems. Notable formalisations include the first mechanical proof of the Cauchy-Schwarz inequality in a first-order logic and a theorem attributed to Yurii Nesterov for characterising convex functions with Lipschitz continuous gradients.One motivation for this work is to further contribute to the automated deduction of theorems involving such mathematical objects. Another motivation is the potential applications in the verification of analog circuits, cyberphysical systems, and machine learning algorithms. Indeed, common techniques in these areas involve reasoning about the algebraic properties of higher dimensional structures over the reals or the extremal values, monotonicity, and convexity properties of functions over these structures. These applications, along with Nesterov's theorem, demonstrate that our formalisation serves as a useful foundation in the space of reasoning and verification research.
View record
Finding operating points of circuits is a crucial first step for simulation and verification.Traditional operating point analyses such as homotopy analysis do find anoperating point. However, a circuit may have many DC equilibria, and failing toconsider an unintended initial condition can lead to failures escaping to the physicalsilicon. This work presents a method for finding all DC equilibrium points;this approach is based on interval-arithmetic-based verification algorithms; and ouropen-source implementation supports state-of-the-art short-channel device models.This work also presents what we believe to be the first, completely automatic verificationof the Rambus ring-oscillator start-up problem. Our method offers largeperformance and scalability advantages when compared with the dReal and Z3SMT solvers.
View record
Ubiquitous computer technology is driving increasing integration of digital computing with continuous, physical systems. Examples range from the wireless technology, cameras, motion sensors, and audio IO of mobile devices to sensors and actuators for robots to the analog circuits that regulate the clocks, power supplies, and temperature of CPU chips. While combining analog and digital brings ever increasing functionality, it also creates a design verification challenge: the modeling frameworks for analog and digital design are often quite different, and comprehensive simulations are often impractical. This motivates the use of formal verification: constructing mathematically rigorous proofs that the design has critical properties. To support such verification, I integrated the Z3 “satisfiability modulo theories” (SMT) solver into the ACL2 theorem prover. The capabilities of these two tools are largely complementary – Z3 provides fully automatedreasoning about boolean formulas, linear and non-linear systems of equalities, and simple data structures such as arrays. ACL2 provides a very flexible framework for induction along with proof structuring facilities tocombine simpler results into larger theorems. While both ACL2 and Z3 have been successfully used for large projects, my work is the first to bring them together. I demonstrate this approach by verifying properties of a clock-generation circuit (called a Phase-Locked Loop or PLL) that is commonly used in CPUs and wireless communication.
View record
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
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
If this is your researcher profile you can log in to the Faculty & Staff portal to update your details and provide recruitment preferences.