Proving Newtonian Arbiters Correct, Almost Surely by Ian M. Mitchell B.A.Sc, University of British Columbia, 1994 A THESIS SUBMITTED IN PARTIAL FULFILLMENT OF T H E REQUIREMENTS FOR T H E DEGREE OF Master of Science in T H E FACULTY OF GRADUATE STUDIES (Department of Computer Science) We accept this thesis as conforming to the required standard The University of British Columbia October 1996 © Ian M. Mitchell, 1996 In presenting this thesis in partial fulfilment of the requirements for an advanced degree at the University of British Columbia, I agree that the Library shall make it freely available for reference and study. I further agree that permission for extensive copying of this thesis for scholarly purposes may be granted by the head of my department or by his or her representatives. It is understood that copying or publication of this thesis for financial gain shall not be allowed without my written permission. Department of CcV^v^M j - P ^ ^ J ^ n r ^ The University of British Columbia Vancouver, Canada Date DE-6 (2/88) for putting up with me hogging the machine. To Brian Edmonds for writing such a slick little thesis style file. To the office staff, students, and profs of the CS department for a wonderful 26 months (of a 1 year masters degree). Very special thanks are due to David Kirkpatrick, Dinesh Pai, and Carl Seger for stepping in as second readers on a panicky last weekend. I don't know what to say about Kaaren. Grad school's important, friends are important, but you've been the most important for the last five years. And hopefully for many more, Thank you. Large parts of this thesis have been pulled from the paper "Proving Newto-nian Arbiters Correct, almost surely" written by me and Mark, which appears in the proceedings to Designing Correct Circuits '96, held in Bastad, Sweden, Sept. 1-3, 1996. The University of British Columbia October 1996 viii Abstract An arbiter is a circuit that grants its clients mutually exclusive access to a shared re-source. The ideal arbiter cannot be built—either requests must occur synchronously, mutual exclusion is not guaranteed, or the arbiter may become hung indefinitely and fail to make a decision. This thesis explores arbiters whose failure mode is the lat-ter; they are not live. Two specific arbiters are investigated: a "toy" arbiter, whose model was chosen for its .tractability; and Seitz's nMOS interlock, which was cho-sen as an example of a widely used and studied design. Both arbiters are modeled by nonlinear continuous dynamic systems, and both models are Newtonian: given an initial set of system states, the future image of that set has exactly the same dimension. The toy is shown to be almost surely live—with probability 1, the arbiter eventually, grants some pending request—while still satisfying all the other properties of an ideal arbiter. The analysis is more general than previously published results in that the inputs of the arbiter may vary while the arbiter is metastable, and conditions are given that ensure liveness even in the presence of such variations. The verification is accomplished by proof that the set of states forever trapped in the metastable region of the toy is lower dimensional than the state space of the toy as a whole. Parallels between the toy and the interlock can then be drawn. ii Contents c Abstract ii Contents iii List of Figures vi Acknowledgements vii Dedication ix 1 Introduction 1 1.1 What's so interesting? 1 « 1.2 Scope and Goals . 4 1.3 Outline 5 2 Background Material 7 2.1 Circuits and Metastability 7 2.1.1 Mutual Exclusion and Synchronizers 7 2.1.2 Metastability: Indecisiveness in Circuits 9 2.1.3 The Impossibility of the Ideal Arbiter 11 2.2 • Verification and-Dynamical Systems 13 iii 2.2.1 Dynamical Systems Theory 14 2.2.2 Relating the Continuous to the Discrete 15 2.2.3 Inputs that Change 17 2.2.4 Specifying the Inputs 18 2.2.5 Other ODE Approaches to Verification 19 3 Preliminaries 21 3.1 Continuous Models 21 3.2 Abstraction Functions 24 3.3 Temporal Formulas on Probability Spaces 26 3.4 A.Discrete Specification 27 4 The System 30 ".' 4.1 The Clients 30 4.1.1 Brockett Constraints for the Requests 30 4.1.2 No Feedback Controllers . ' 32 4.1.3 An Abstraction Mapping . . . . ." 34 4.2 The Toy Arbiter 36 4.2.1 The Differential'Equations 37 4.2.2 The Abstraction Mapping 39 4:2.3 . The Continuous.Model 41 5 Verification 43 5.1 Closure " 43 5.2 Mutual Exclusion 43 5.3 Reset . . . . . . . . . • • • 45 5.4 Handshake 47 iv 5.5 Liveness, almost surely 48 5.5.1 Liveness and metastability 49 6 The Seitz Interlock 57 7 Conclusions 63 7.1 What has been Accomplished 63 7.2 Suggestions for Further Research 65 Bibliography 68 Appendix A Details of Divergence Proof 71 List of Figures 2.1 Brockett's Ring 18 3.1 Continuous Model 22 3.2 Arbiter Specification 29 4.1 Ricochet Trajectory 32 4.2 a-insensitivity . . 34 4.3 . Phase space portraits for the Toy Arbiter 38 4.4 The Toy's Output Brockett Ring 39 5.1 Regions for Liveness Proof 49 6.1 Seitz Interlock .Circuit .. 58 6.2 ' Transistor Model . . . 59 6.3 Transistor Model Equation , . 59 6.4 Phase space portraits for Seitz's arbiter 60 * vi' Acknowledgements Hmmmm.. Ian Mitchell writes his thesis on indecision. Who ever would have thought? Actually, the only question left is what to do next. I wonder . . . Meantime, there are an awful lot of people who got me through this !@#$%*&* thing (and you try cartoon swearing in L^TgX). Mark Greenstreet is definitely at the head of the list. A fount of endless neat ideas, Mark took an indecisive second year masters student and found a perfectly matched topic. And since then has been providing the supervision and "Arrrgh! I'm stuck again!" answers necessary to finally finish one of these thesis thingees. Necessary but not sufficient. I never would have gotten here, stayed here, or finished here without Mom, Dad, Eric, and the cats (the dog, well, not so much). My thanks to Fraser for reminding me that computers are more than just an arbiter with some stuff around it—they are fascinatingly capable of playing Civ II for example. To Katrina for reminding me that life is more than just a computer with some stuff around it and for always providing a perfect foil to a habitual devil's advocate. To Kevin (and the rest of the former pit night flock) for keeping me from wasting my time at UBC studying—now I'll be knocking on your door with a Netrunner deck, Kevin. To Piers and the gaming gang (past and present) for Sunday nights happily divorced from reality. To my office mates (Cristina, Dan, Elisa, and Sonya) vii To Grandpa and Sputnik. Wish you both could be here. Chapter 1 Introduction 1.1 What's so interesting? An arbiter is a circuit that grants its clients mutually exclusive access to a shared resource. In its simplest form, an arbiter has a request input and a corresponding grant output for each of its clients. When a client wants access to the resource, it signals the arbiter on it's request line. The arbiter awaits request signals, and then produces a grant—only.one grant may be outstanding no matter how many clients are making requests. When a client receives a grant, it may safely access the resource without conflict. Eventually, the client will finish with the resource and release its request, at which point the arbiter is free to generate a grant to any other currently requesting client. Arbitration is such a common operation that few complex VLSI circuits are without some form of arbiter. Although construction of a failsafe arbiter in synchronous circuits (circuits with a common clock reference) is relatively easy, the push for faster and larger circuits has lead to increasing use of asynchronous (no 1 single clock) design techniques. And as soon as asynchronous arbiters were used, they started to fail. As early as the 1960's, it was recognized that arbiters—and a related circuit element, synchronizers—subject to asynchronous inputs were failing occasionally. Since that time, a series of proofs have been developed to show that • Arbiters fail when both clients request permission to the resource at nearly the same time. • The failure manifests itself as an inability to give digitally defined grant signals • back to the clients fast .enough after the requests. • The grant.signals may remain hung at an intermediate value for an unbounded interval of time. The arbiter is said to be metastable in this case. •. This time-unbounded response is a fundamental property of arbiters—any design which avoids-it. will fail to act like an arbiter in some other respect. Each proof required fewer and fewer assumptions about the arbiter and/or envi-ronment; consequently, it is now clear that no ideal asynchronous arbiter may be physically constructed. Starting with the early, research attempts, arbiters were studied through mathematical models. For the simplest case of arbiter, the two client arbiter, most models take the form of bistable dynamic systems—dynamic systems which, for at least some range of parameters, have two separated asymptotically stable attractors. Associating a different client with each attractor allows a mutually exclusive map-ping of the state space of the system: when the system state is near an attractor, that attractor's client gets permission to access the resource. 2 Looking at phase space plots of these bistable systems shows immediately the cause of metastability. Each attractor collects trajectories from its basin of attraction in state space. But because stable basins of attraction must be open sets in the state space, there must be some set of states which separates the two basins and belongs to neither. Trajectories starting at the edge of a basin may take arbitrarily long times to approach the attractor, thus causing metastability. And trajectories starting in neither basin will never reach an attractor at all. So not only is it impossible to guarantee arbitration within bounded time, but, because of the trajectories which lie in neither basin, it is impossible to guar-antee arbitration ever occurs. This thesis explores that possibility—the likelihood of an arbiter never completing its task. Intuitively, that probability is zero. A dynamic system which models a two client arbiter can be constructed in a two dimensional space. The basins of attraction will be two dimensional, but their separator need only be one dimensional; some curve through the state space. For any reasonable distribution of initial states, the probability of landing on that lower dimensional curve is then zero. The analysis is not that simple, however. The properties of an arbiter demand that the topology of the state space change depending on the inputs from the clients. For example, if only one client is requesting permission to use the resource, then there should only be one attractor in the state space (corresponding to granting that client's request). But if the other client then also makes a request, fairness demands that a second, corresponding attractor appears in the state space. If these large changes to the inputs can produce such large changes in the location (or existence) of attractors, continuity demands that small changes in the inputs must also change the location of attractors. Moving an attractor changes the shape of the basin of attraction, which in turn influences the shape of the curve of trapped metastable states—those states which lie on trajectories never leading to a completed arbitration. If the clients can change the shape of the set of trapped trajectories by varying their input signals, a question then arises: could a client waiting for permission to the resource whose request signal varied slightly over time, although it definitely always remained "raised", accidentally create a set of trapped states whose dimension was equal to the dimension of the system; a set whose probability of occurring would be non-zero? Note that a probability distribution over initial states is used in the analysis that follows, but given an initial state, the systems studied evolve deterministically. Noise is not considered in this thesis. Also, the dynamic systems used to model the arbiters are Newtonian in the* sense that the dimension of subsets of the state space is preserved over time. Therefore, if the initial state space is two dimensional, the reachable state space will likewise be two dimensional. 1.2 Scope and Goals This thesis presents a detailed' examination of a simple "toy" dynamic system which behaves as an arbiter. A set of discrete properties is described which exemplifies an ideal arbiter, and the toy can be shown to satisfy all properties except liveness—it may fail to finish arbitration-even after an infinite time. The major hew contribution of this thesis is to show that, for most clients, the set of trapped trajectories is guaranteed to be of lower dimension than the state space of the arbiter, and thus arbitration eventually occurs "almost surely" (i.e. with probability one). The group of clients excluded from this statement are feedback controllers carefully designed to trap the arbiter; clients which would serve no useful purpose and thus would be highly unlikely to occur by accident in actual designs. In addition to the concrete objective of proving the arbiter almost surely correct, the research described in this thesis has worked as a testbed for techniques whose goal is the formal verification of continuous dynamic systems models against discrete specifications. Tools such as • Workable abstraction mappings which map states or sets of states from the continuous model into the discrete domain of the specification and back again. • A discrete temporal logic defined over a continuous state space, so that adher-ence to the discrete specification can be verified. were refined during the work with the toy, and this thesis can be taken as an example of their use. The analysis of the toy, by itself, is a somewhat esoteric pursuit. The eventual goal of this research is the study of real VLSI arbiters, and lessons learned while examining the toy can hopefully be applied to such circuits. As an example, some parallels between the toy and a transistor level model of the Seitz interlock circuit (a real VLSI arbiter) are drawn in chapter 6. 1.3 Outline This thesis presents the formal verification that the continuous dynamic system model of an arbiter almost surely implements a discrete specification of the proper-ties of an ideal arbiter. • Chapter 2 reviews related work. First, previous analysis of asynchronous ar-biters is presented, with particular attention to the theorems proving the im-5 possibility of constructing an ideal arbiter. Focus is then shifted to the other important body of work—the issues surrounding verification of continuous dynamic system models against discrete specifications. • Chapter 3 provides the mathematical preliminaries necessary for the verifica-tion. Separate sections describe the types of dynamic systems studied, the formal temporal logic used for verification, the abstraction mappings between the continuous and discrete domains, and a discrete specification of an ideal arbiter. • Chapter 4 contains the dynamic system model. The continuous implemen-tation of the arbiter's clients in first described in very general terms, includ-ing specification of those clients excluded from consideration (the feedback controllers). The toy's differential equations are introduced, and a careful abstraction mapping is given which will allow its verification. • Chapter 5 is the actual verification of the arbiter. The toy is shown to satisfy all properties of the ideal arbiter but liveness, and satisfy liveness almost surely. • Chapter 6 presents the interlock circuit, a description of the methods used to turn it into a dynamic system, and an analysis of the similarities between the interlock's system and the toy's. A. chapter of conclusions and suggestions for further research completes the core of the thesis, with an appendix containing proof details following. 6 Chapter 2 Background Material 2.1 Circuits and Metastability 2.1.1 Mutual Exclusion and Synchronizers Mutual exclusion, or mutex, is a fundamental concept in computer science. Grant-ing solitary access to. a resource to just one among several competing clients is a requirement of almost all complex circuits. The concept is simple—whoever asks for the resource first is granted access, and retains sole right to access for as long as is necessary. This first in, first out behaviour only needs to be followed loosely. If several requests for access arrive nearly simultaneously and no right has been given, one of the requests must be honoured (it does not matter which). Only when the chosen client releases the right of access may another client be granted access. A circuit which can enforce mutual exclusion is called an arbiter. When clients share a common clock reference, such as in a synchronous cir-cuit, many solutions to the mutex problem exist. In every case, advantage is taken of the fact that in a purely synchronous world, time advances in discrete steps (the 7 clock edges). Signal levels are only allowed to change between time steps, and so signals at each step also lie in a discrete set of values—in digital circuits the set variously called {true, false}, {high, low} or {1, 0}. Without a common clock, in asynchronous systems, no such simple solution exists. Time must be considered a continuous variable in these systems, and so, in a theoretical sense, determining which client's request arrived first would require in-finite precision and thus a physically unrealizable circuit. Even arbitration between two separate synchronous systems will not work—the signals passing between the systems can no longer be assumed to lie in a discrete set. For example, consider a signal in one system changing value between two clock edges. Within that system, the signal will start at a discrete value on one clock edge, and finish with another discrete value at the next clock edge. But because the clocks of the two systems are unrelated, if the second system is given access to the changing signal, its clock edge may arrive at any time .during the change. To the second system, the signal can take on any of a full continuous range of values. The obvious solution is to assign, based on the continuous value of the incom-ing signal, some discrete value whenever the second system's clock advances. Such a "synchronizer" element ensures that input signals have discrete values and would allow separate asynchronous circuits to submit requests to a synchronous mutual exclusion device, thus solving the asynchronous mutual exclusion problem. Unfortu-nately, a synchronizer must operate by determining where a continuous input value lies relative to a threshold, and assigning its output appropriately. But such deter-mination would again require; infinite precision and is thus physically unrealizable. There is, however, a deep connection between the problems of synchroniza-tion and mutual exclusion. ^ 2.1.2 Metastability: Indecisiveness in Circuits As early as the 1960's it was recognized that synchronizers and arbiters were occa-sionally failing due to a phenomenon known as metastability. The outputs of these systems, although designed to be stable at one of the discrete digital logic levels at each time step, could become hung at intermediate levels. This inconclusive output wasn't stable—it would settle to a discrete level after an indeterminant period of time—and hence was called metastability. Failures occurred when the metastability lasted longer than a clock cycle, the intermediate output value escaped into the rest of the circuit, and was interpreted in contradictory ways by different parts of the circuit. The study of asynchronous arbitration and synchronization, even in its early days; proceeded with sporadic results,, and a great number of different researchers have contributed to the literature over the years. More than two decades ago, Chaney and Molnar [CM73] were able to stim-ulate some common synchronization circuits repeatably enough to obtain photo-graphic evidence of metastability on an osilliscope. At that time it was known that synchronizers and arbiters could not be guaranteed to produce an appropriate digital output signal at any fixed time after receiving an asynchronous input signal. Two years later, Hurtado [Hur75] tackled the case of bistable dynamical systems—systems of ordinary differential equations (ODEs) in which most trajec-tories are asymptotically attracted to one of two equilibrium locations in the phase space. After associating each of these "attractors" with a digital logic level, the system can be considered to output the appropriate logic level when its state is in the neighborhood of an attractor. Both synchronizers and arbiters can be modeled by bistable systems. Hurtado showed by continuity arguments on the ODEs that 9 there must exist a set of states which approaches neither attractor—the so-called region of indecisiveness. Furthermore, Hurtado showed that there must exist valid inputs which will take the system state from the neighbourhood of an attractor into this region. . . Due to the strength of assumptions that Hurtado made about his systems, however, models of real circuits could not be expected to fulfill them. It was not until Marino [Mar81] extended Hurtado's arguments that the theoretical metastability results could definitely be said to apply to real circuits. Unlike Hurtado, Marino does not require inputs to remain fixed. Also, Hurtado's region of indecisiveness is a lower dimensional set in the phase space of the bistable circuit (and thus an unlikely set for the system state to get into). Marino's important extension showed that there exist states near the region of indecisiveness which—even though they move toward an attractor over time—would fail to get close enough to either attractor to output a logically defined value in any fixed bounded time interval. The probability of metastability was thus nonzero for any bounded time. Marino argues convincingly that his assumptions are weak enough to include models of all real digital systems. Several years later, Chapiro [Cha84] took another step in analyzing metasta-bility. Although the. bulk-of his doctoral thesis was concerned with the design of high-performance asynchronous systems, Chapiro proved an important theorem related to the mutual exclusion- and synchronization problems. In circuit terms, Marino's result showed that sequential bistable machines could not avoid metasta-bility. Chapiro applied his result to show that no machine, combinational or se-quential, could give a discrete output based on the value of a continuous input in bounded time. -While the systems they studied were different—Hurtado's and Marino's bi-10 stable dynamical systems versus Chapiro's general asynchronous digital systems— the techniques used were very similar. First, an exacting statement of the properties of the particular system was made. Second, a continuity argument was described which showed the properties to be contradictory and thus impossible to fulfill. In all, a very successful paradigm. But, although all these results were applicable to the mutex problem, none had directly addressed it. By using this two-step method on an arbiter, even more powerful results were possible. 2.1.3 The Impossibility of the Ideal Arbiter The specific case of the arbiter, however, waited until Mendler and Stroup's rel-atively recent paper [MS93]. In it, they work with a fairly general example of a two client arbiter. The broader class of continuous automata instead of bistable dynamical systems is used asthe model of physical devices. The arbiter has an input and output for each of its clients—respectively called the request and grant lines. Communication follows a four-phase handshake • In the quiescent state, both request and grant are low. When a client wants to use the resource, it .raises its request (so this phase is called the request phase); however, it may not do so until its previous handshake sequence has been completed: a client may not raise its request until its grant is low. • . The arbiter is a passive element—it will not attempt any signaling on its outputs until one of - its - clients requests the resource. Once a request has arrived, the arbiter should issue a grant (arbitration phase): the arbiter may not raise a grant until the corresponding request is high. • Once the grant is received, the client may use the resource (transmission 11 phase). However, this protocol requires persistent clients: a client may not lower its request until it has been acknowledged by a raised grant. • Clients signal completion by lowering their request (release phase). However, mutual exclusion dictates that further grants may not be issued until the client has finished and signaled completion: the arbiter may not lower a grant until the corresponding request is low. Note that the client must enforce the first and third rules, while the arbiter must enforce the second and fourth. If the client follows its part of the protocol, then Mendler and Stroup identify five attributes of an ideal arbiter (stated in terms of a discrete abstraction of the continuous system): °. • The.arbiter must allow requests at any time—in particular, concurrent re-quests are allowed (called the closure property). • The arbiter must never allow both grants to be outstanding at one time (mu-tual exclusion). • When a client withdraws-its request, the arbiter must withdraw the grant within a fixed time interval (reset). • Once,a grant is given, it may not be withdrawn until the corresponding re-quest has been withdrawn. Likewise, the arbiter cannot give a grant until a corresponding request has ..occurred (handshake). • If at least one request is outstanding, eventually one request will be granted • (liveness)... ; •' 12 Of particular interest is the final property, liveness. Unlike previous proofs, the "eventually" statement places no time bound on the response of the arbiter. The authors formally define each of these properties, and then prove that no arbiter which fulfills closure, reset, handshake, and liveness can guarantee mutual exclusion. Once again, a continuity argument forms the foundation of the proof. The new contribution of the research is the proof (without any resort to dynamical systems theory) that even a time unbounded arbiter may fail to perform correctly. Mendler and Stroup also claim, without proof, that an arbiter could be con-structed which fulfills any four of the five ideal properties—a claim which is in most cases trivially obvious. It is important none-the-less; this thesis studies ar-biters which satisfy closure, reset, handshake and mutual exclusion, but which fail, however improbably, to satisfy even the weak liveness of Mendler and Stroup. 2.2 Verification and Dynamical Systems Modern circuit design suffers from the competing demands of producing faster cir-cuits in less time. In an attempt to avoid costly mistakes in production systems, hardware verification has become a hot topic. Verifying the operation of any system usually involves determining whether an instantiation of the system fulfills the properties of some high-level specification. In digital computer systems, such a specification is given in discrete logical terms. A discrete model of the actual "system is then created, and the model is checked against the specification. There are, however, circuit behaviours not covered by a discrete view of the world. Signal rise and fall times cannot be tracked in discrete models; conse-quently, those models are poorly suited for asynchronous design. And some circuit 13 behaviours—such as the inescapable metastabilities described above—have no dis-crete analogue. The first step in verifying such circuits is then determining an appropriate continuous modeling environment that supports all these additional be-haviours. And because designers will continue to give specifications of digital circuits in discrete terms, the second step of verification will have to determine whether a continuous model implements a discrete specification. 2.2.1 Dynamical Systems Theory Fortunately, nonlinear dynamical systems theory may be able to solve both prob-lems at once. A dynamic system, as used in this paper, is a system modeled by ordinary differential equations. Instead of attempting analytic or numeric solutions to the ODEs, dynamic systems theory studies the qualitative behaviour of groups of solutions. General types of behaviour—such as shrinking to a point, growing from a point, periodic orbits or chaos—can be identified. In particular, the long term evolution of the system can be determined. The ability of ODEs to model metastable circuit behaviour was the keystone of Hurtado's thesis [Hur75] as described above. The use of dynamic systems to verify circuits is much more recent, however. Black [Bla94] gives a good description of most of the dynamic systems theory used in the research presented here. The dynamic systems model of a circuit consists of a current system state and a set of ODEs describing the evolution of that state. Inputs to the circuit become parameters of the ODE set. The variables of the system create a phase space, in which the current system state is a point. As time is allowed to progress, the state will travel through a set of points, forming a curve in the phase space. This curve is called a trajectory of the system. Dynamic systems theory can describe the general 14 behaviour of trajectories based on topological features of the phase space. For the systems studied here, the only topological features of importance are fixed points—equilibrium positions in which the system state does not change. Based on the behaviour of nearby trajectories as time increases, fixed points can be classified into three groups: if the trajectories converge to the fixed point, it is an attractor; if trajectories diverge, it is a repellor; and if trajectories approach in some directions but recede in others, it is a saddle point. Trajectories may also loop back onto themselves, forming periodic orbits, or behave chaotically; however, neither of the systems studied here exhibit these types of behaviour. Although certainly hot the only way to study dynamic systems, both Hurtado and Black make use-of the extensive literature describing the behaviour of ODE systems for fixed values of their parameters. This so-called static approach, which will be adopted for most of the work here, looks at how trajectories will evolve if the parameters—the circuit .inputs—remain at constant values. Of particular interest are the values of parameters, called critical values, where the qualitative behaviour, of the system changes. For example, fixed points may move about as the parameters of the system are varied. But the number and relative locations of the fixed points remain constant unless the system passes through a critical value; here new fixed points may be created, old points may disappear, or more complicated structures may develop. This large change in the behaviour of a system at a critical value is called a bifurcation. 2.2.2 Relating the Continuous to the Discrete ODEs describing the behaviour of VLSI circuits to a fair degree of accuracy can be written, as SPICE [Nag75] demonstrates. Having established those terms and 15 techniques from dynamical systems theory that are needed to study these ODE models, the problem of linking the continuous system with a discrete behaviour remains unresolved.' Hurtado's answer, in keeping with his static analysis, was to associate dis-tinct fixed point attractors with digital logic levels. The set of trajectories which approach an attractor is called its basin of attraction. If every trajectory in a cir-cuit's dynamic system was in the basin of attraction of an attractor, then the system state always remains bounded—a good property for any model of a physical object. And if a neighbourhood of every attractor is mapped to a discrete logic level, then every trajectory will eventually have a logic level associated with it (note that neigh-bourhoods, must be used because no trajectory other than the fixed point itself will ever reach an attractor). As an example of this method, consider the systems from Hurtado's thesis. Their purpose was to model bistable circuits—circuits with two stable configurations for some constant set of inputs—such as arbiters and synchronizers. The obvious dynamic system to use was one with two separate attractors. Similar systems will be used in this paper to model arbiters. Hurtado was able to show the impossibility of a bistable system in which the entire phase space was in. one basin of attraction or the other. Some set of states must lie in neither basin, and thus approach neither attractor. Furthermore, states near this set will take extremely long times to approach their appropriate attractor. It is these states, which slowly or never approach an attractor, which are the cause of metastability. .. ; 16 2.2.3 Inputs that Change For a fixed set of inputs and a mapping of attractors to logic levels, static analysis can use the basins of attraction in a dynamic system to determine which initial states will end up outputting which logic levels. However, a designer of real systems may object to having a circuit's inputs forever fixed. Fortunately, the static analysis of dynamic systems is not as restrictive as might be expected from its name. Although attractors and their basins may move or change shape slightly, the overall behaviour of the system will remain qualitatively similar under varying inputs.as long as those inputs do not approach critical values. It is then, possible to choose the logically mapped neighbourhoods of attractors sufficiently large enough to include the wanderings of the attractor itself and small enough to avoid overlapping any other basins. So with inputs restricted to ranges that avoid criticaf values,"'the'discrete behaviour of the system will remain the same for most trajectories even with changing inputs. There is one remaining dilemma—system designers really do want the dis-crete behaviour of the system to depend on its inputs, at least when its inputs change significantly (for example, from one logic level to another). In order for the system to change its qualitative behaviour, the inputs will have to pass through critical values. But analysis of the system near these critical parameter values is difficult, because even the qualitative behaviour is no longer stable. It could be considered fortuitous, or inevitable, that system designers have found a solution to this problem when discrete binary logic could not. In real circuit design, the. logic levels are separated by an interval of voltage with an undefined logic value, and signals are expected to move through this range fairly quickly. Note that this separation is a design abstraction—real circuits will always produce outputs, but 17 these outputs are rarely expected to be coherent when the inputs are in the undefined range. So an obvious analogy for dynamic systems would place the critical values of parameters in the undefined input range. Consequently, for logically defined input values (which could be intervals) the system would be far from critical parameter values and thus easy to analyze. And yet the behaviour of the system would depend upon its inputs. 2.2.4 Specifying the Inputs Dynamic systems theory can be used to model and verify circuits, so long as inputs do not remain too near critical parameter values. In real circuits, the transition of signals through the undefined range is usually controlled by monotonicity or minimum and maximum-rise and fall time restrictions. Brockett [Bro89] proposed an elegant way to define such restrictions on input signals. It also serves as a method to map continuous inputs to discrete values. min mint The Annulus A "typical" trajectory Figure 2.1: Brockett's Ring For a signal v, Brockett's ring is actually an annulus in v X dv/dt space (see figure 2.1). For each value.of v, it gives ranges on acceptable rates of change in v. 18 When the signal lies in the region on the far left, denoted B\, its derivative may be positive or negative; so the signal may fluctuate up and down, and remain in B\ for as long as it likes. Signals leaving B\ may only exit into the upper region adjacent to #1 (denoted B2)—exiting into the lower adjacent region (#4) would require a positive derivative and signals in B\ may only have negative derivative. Once in B2, the signal must maintain a positive derivative and thus travel monotonically to the far right region (#3), where it may once again remain for as long as it likes. Leaving B3 may only be accomplished through B4 which, complementary to B2, requires a monotonic transition down to B\. Because the signal can remain for arbitrary periods in the left and right regions {B\ and B3), these; are^ obvious choices for mapping to logic levels. The upper and lower regions (B2 and B4) will then represent monotonic transitions between the discrete logic levels. The outer and inner rings of the annulus in B2 and B\ restrict the minimum and maximum times the signal may spend in transition. By : placing critical values of parameters in the intermediate range represented by B2 and #4, input signals will be forced to move through bifurcations with non-zero speed and remain away from the bifurcation when logically defined. Static analysis and verification of the dynamic system can then proceed with logically defined inputs. 2.2.5 Other ODE Approaches to Verification The study of ODE models of circuits using static dynamic systems theory is not the only technique to use continuous models to try and verify digital circuits. SPICE models have been used for decades in trial and error verification of circuits—try a ; signal'waveform, see if the circuit fails; repeat. That particular method, although popular, has obvious shortcomings: it cannot handle the infinite variability of signals 19 possible in a continuous environment. Kurshan and McMillan [KM91] divided the phase space of an arbiter model into boxes, and then used numerical integration to find a next state relation for each rectangle. The adherence of this relation to an arbiter specification was then checked using a traditional discrete model checker. Although the technique did take account of continuous behaviours of the ODEs that would not be exhibited in a dis-crete model, the analysis fell short in the case of an arbiter for two reasons: results depended heavily on the choice of rectangle size and time step used in the integra-tion phase, and no analysis of the arbiter's metastable behaviour was attempted. A significant contribution was that the verification did not depend on the inputs remaining fixed—only that they lay in some reasonable range. Greenstreet [Gre96] has verified a toggle element using dynamic system the-ory. The toggle's ODE system, unlike that of the arbiters studied below, does not have nicely separated attractors and, in fact, may contain attractive periodic orbits. It is therefore not amenable to the static analysis style described above, and other techniques, numerical' in nature, have had to be used. Thomas Henzinger and a group at Cornell have developed a tool, Hytech, for automatic analysis and verification of linear dynamic systems models in the field of hybrid control systems. Henzinger and Ho [HH95] have recently been working on ways of transforming nonlinear systems so that Hytech can be used in their verifica-tion. Those techniques are similar to the ones used below to verify that the arbiter models fulfill most of the properties of an ideal arbiter. Hytech would, however, be unable to prove that mutual exclusion is fulfilled almost surely. On the other hand, further work on Hytech should be carefully observed—its automatic verification abilities would surely be a boon should new arbiter models be investigated. 20 Chapter 3 Preliminaries Verifying that a continuous dynamic system implements a discrete specification re-quires four ingredients: the dynamic system, the discrete specification, an abstrac-tion mapping which takes states from the continuous domain to the discrete and back again, and a temporal logic defined over continuous dynamic systems which— with the abstraction mapping—allows proof of discrete assertions. This chapter mathematically defines each of these components. Dynamic systems are only dealt with in a general sense; the specific dynamic model of the arbiter will be given in the next chapter. The same- holds true of abstraction map-pings, since so much depends .on.the.model in question. Because only arbiters are dealt with in this thesis, the discrete specification will be given in full detail. Finally, a brief overview of the temporal, logic that is used in the verification will be given. 3.1 Continuous Models A continuous model is a tuple, (F, Q,P) where F is a derivative function on some d dimensional subspace of Rd (the system state space), and (£l,P) is a probability 21 space. F must be C 1 (i.e. dF(x)/dx is continuous). Furthermore, Q is assumed to be the Borel E-algebra over U (the initial state set) with U C Rd, and dim(£/) = d. A continuous model is a closed system (no inputs) modeling both the circuit of interest and its environment (see figure 3.1). arbiter f:R,+mr^Rn P1 environment J n -t— d - m+n+h F:I?i-+Rd Figure 3.1: Continuous Model—Arbiter & Environment with no inputs Autonomous (time independent), non-linear, ordinary differential equations are used to model circuits. A circuit with m inputs and n outputs is modeled by a function / : R T O + n W1 that gives the time derivative of each output as a function of the current values of the inputs and outputs. In this model, circuit behaviour will only depend on its current state and inputs; consequently, autonomous ODEs are sufficient for modeling. An environment for the circuit has n inputs corresponding to the outputs of the circuit, m outputs corresponding to the inputs of the circuit, and h internal variables. The behaviour of-the environment is given by a function (mapping K / l + m + " to M / l + O T ) that gives the time derivatives of each output and internal variable of the environment. Let d = h + m + n denote the total dimension of the circuit with its environment. A state of this system corresponds to a point in Kd. F denotes the 22 time derivative function for the system state, F : Kd r-» Kd. By modeling the circuit and environment together, a closed system is ob-tained. A trajectory <p(xo,t) is the curve (parameterized by initial point and time) through Rd representing the evolution of the entire system starting at state Xq at time t = 0: <p(xo, 0) = XQ. The path of a trajectory is defined by the ODE V r e K f . ^ f 5 ^ = FM a ! o,r)) Because F is autonomous and has no inputs, a trajectory is completely determined by its initial state. For some fixed time r, </>(•, r) :Kd^Rd is a function which maps states forward r units in time, and which may be inverted by </>(•, —T): The dual function-</>(x, •) denotes an entire trajectory (extending for-wards and backwards in time) which passes through state x at time 0. Because F is C 1 in Kd, <f(-,r) is a one-to-one mapping and is continuous in its unevaluated argument (see [HS74], chapter 8). Furthermore, if a trajectory ip(x, •) starts in some bounded region W, it will remain defined for all points in W—trajectories must either remain defined for all time or escape to infinity. As a consequence of all these conditionsi T) preserves the dimensionality of subsets of Rd (3.1) (see [HW41], theorem VI 7).. The word "Newtonian" in the thesis title corresponds to this condition on the dynamic systems studied here. As mentioned above, (f2,,P) is a probability space: an initial state XQ corre-sponds to an event in Q. P must be smooth in the sense that . ( Q c O ) A (dim(Q) < d - 1) => P{Q) = 0 23 This condition on P rules out overly determined initial states where, for example, the value of some variable is exactly specified. For B C f2 and r G E + , ip(B, —r) n U, denotes the set of initial points whose trajectories reach a point in B after exactly r time units. By the observations in the previous paragraph, P(<P(B,-T))>0 d i m ( B ) > d - l (3-2) This feature of the models under discussion is central to proofs that discrete prop-erties hold "almost surely." 3.2 Abstraction Functions The previous section presented a framework for continuous models based on systems of non-linear differential equations. The objective of the thesis is to show that such models correctly implement discrete specifications. This verification task requires an abstraction function to map continuous trajectories to discrete sequences, which can then be checked against the specification. When the discrete state space is finite, the abstraction function can be represented by an ensemble of state predicates. The simplest abstraction function that will be used in this thesis assigns a discrete value based on the level of a continuous variable. For example, the mapping (v > 0) <^ > v states that the discrete signal vds true if the continuous variable v is non-negative. In absence of any further specification, v can be taken to be false otherwise (i.e. when v is negative). 24 A slightly more complex abstraction may leave the discrete variable undefined for certain values of the continuous variable (v > 1) =>• v (u < 0) ->v A continuous signal level in the undefined region could be interpreted differently by different circuit elements—safe verification demands that a worst case interpretation be adopted and analyzed. As mentioned in section 2.2.4, a more complex but very useful abstraction mapping is the Brockett ring. For a continuous signal u, Brockett(v) states that it obeys a Brockett ring ( v2 v2 \ ( v2 v2 \ B r o c * e » ( u ) = ( + > l J A ( — + ^ < l ) (3.3) V Vmin min ' V mai umax / The constants um,-n, um,-n, vmax, and vmax define the size of the two ellipses which bound the Brockett annulus (see figure 2.1). The annulus can.be easily divided into four regions, which can be thought of as V = V low V = V rising Bz{v) = V - V high B4(v)' = V £B4 = V falling Where, for some variable v, v = dv/dt. When using a Brockett ring for abstraction mapping, the discrete signal is assigned a value based on the region in which the continuous variable lies. For example • ' , • b 3 ( V ) =^ v states that v is true when v is in B3, or v high. 25 3.3 Temporal Formulas on Probability Spaces Given the negative results for arbiters mentioned in section 2.1, the objective is to show that an arbiter satisfies its specification, including liveness, almost surely. The specification for a discrete model is naturally written as a temporal logic for-mula [Pnu81, RRH93], which motivates introducing a temporal logic defined relative to a probability space. A state predicate gives some condition about the initial state of the system— for example #3(2) is a state predicate claiming that-variable x is in the high region of its Brockett ring at time 0..,.State predicate Q holds for trajectory LO(X, •) if Q is satisfied by the initial state of that trajectory hold(Q, <p(x,-)) = Q is satisfied by (p(x, 0) A state predicate is the simplest type of temporal formula. Let G and H be temporal formulas. The constructs ->G, G V H, G A H, and G =>• H are also temporal formulas and have the obvious interpretations. The formula UG (always G) holds for f{x,-) if G holds for all suffixes of <p(x, •); likewise, OG (eventually G) holds if n-*G does not hold (recall that a trajectory is completely determined by its .initial state). The formula G —> H denotes a weak until: hold(G -> H,(p(x,-)) = hold(nG,(p{x,-)) V hold(G,<p(x,:))\. (3T G K + . (Vp€[0,T).hold(G,<p{<p(x,p),-))) A hold(H,(f(<p(x,r), •))) 26 Note that —» (until) is different from the standard logical ==> (implies). Occasion-ally the shorthand (Gi -> G 2 -> G 3) = (Gi -»• G 2 ) A (G 2 -»• G 3 ) will be used. The formula G ~> H is an abbreviation for G Oiif. For 77 G K + , the formula G ^ H holds if i? holds within 77 time units of G holding: _hold(G&-H,<p{x,-)) = rhold(G,(p(x,0)) = • 3r G [0,77). hold(H, <p(ip(x, r), •)) A formula is valid if it holds for all trajectories starting in fi, and it is valid almost surely if it holds with probability 1: valid (G) = VueSl.hold(G,u) as(G) = "3A C Q. (Vo; G A. hold(G,u>)) A (P(A) = 1) 3.4 A Discrete Specification In the discrete specification of a system, the only signals of importance are the interface between that system and its environment—in the case of an arbiter, the request and grant lines. Signals internal to the arbiter or environment can be ignored by the specification. Only arbiters with two clients are examined in this thesis (extensions are discussed in section 7.2). The interface between the arbiter and the first client consists of two boolean valued signals: a request, r i ; and a grant, gi. Likewise, signals r 2 and g 2 are the interface between the arbiter and the second client. The allowed behaviour of the clients is simple to specify. The communication between the clients and the arbiter follows a four-phase handshake: a client may 27 only raise a request when its grant is false, and it may only lower a request when its grant is true. This protocol is formalized by the temporal logic formula 2 f\ • (-.r,- -)• -.g,-) A • (r; -»• gt) (Co) »=i Mendler and Stroup [MS93] have identified five attributes that capture the intuitive sense of an ideal arbiter: 1. Closure: No assumptions are made about the relative arrival times of the request signals. In particular, it is not allowed to specify that there is some minimum time separation between requests from different clients. 2. Mutual Exclusion: Both grants cannot be outstanding at the same time. 3. Reset: If a request has been withdrawn, the corresponding grant will be with-drawn after at most.r time units. ,4. Handshake: If a grant has been given, it will not.be withdrawn until the corresponding request has been withdrawn. Furthermore, a grant cannot be given unless the corresponding request has occurred. 5. Liveness: If at.least'pne'f'equest'is outstanding, eventually one request will be granted. As noted by Mendler and Stroup, no Newtonian arbiter can satisfy all five of these requirements. Therefore, the fifth requirement is weakened to: .5'. Liveness (almost surely): If at least one request is outstanding, eventually one request will be granted almost surely. Properties 2-5 are formalized in figure 3.2. The closure property is satisfied by not stating any assumptions about the relative arrival times of the request signals. A verified arbiter will satisfy: valid (G2 A G3 A G4) A as(Gs). . ' 2 8 • (-•(gi Ag 2 ) ) (* Mutual Exclusion *) 2 • ( / \ n ( - r A - g ; ) ) (* Reset*) 2 2 / \ •(& -)• -r,-) A ( / \ • ( - g i -> rO) (* Handshake *) i=l i=l 2 / \ D((n V r2) ~> ((n A gi) V (r2 A g2))) (* Liveness *) Figure 3.2: Arbiter Specification (i G {1)2}) 29 Chapter 4 The System 4.1 The Clients In the discrete domain, the arbiter client need only fulfill the protocol require-ment (Co). Although it would be nice to keep the specification for the continuous implementation bf the client that general, the analysis presented below of the ar-biter's response will require a few more restrictions. 4.1.1 Brockett Constraints for the Requests For the reasons stated in section 2.2.4, the first continuous restriction will be that the client's request lines, stay.-'within a Brockett ring. Letting a and b represent the request.lines of the two clients, this requirement is a(Brockett(a) A Brockett(b)) (d) Where Brockett(v) was defined in (3.3). The boundaries of the ellipses of the ring depend on which arbiter model is being used. The toy arbiter examined below, 30 whose signals range between ± 1 , will have an input ring defined by Vmin — 0.9 Vmin ~ 0-9 Vmax — 1-0 ^max — 5.0 A signal v restricted to a Brockett ring obeys a number of useful rules worth stating here. The first is that it remains within a fixed range of values Bounded(v) (£ia) where Bounded(v) = H(-vmax <v< vmax) which for the toy is Bounded{v) = < v < +1) The second is that it moves from region to region in the Brockett ring in a strict sequence (see figure 2.1 for definitions of the regions) • n<Bx(v) ^ B2{v) 5 B3{v) ^ B4(v) 5 Bi(v)) (Clb) where r c = n time units (the time taken to follow a trajectory along the inner edge of the ellipse through the rising or falling regions—the maximum rise/fall time). A signal within a Brockett ring has easy to calculate bounds on its value, time derivative, and rise/fall times. To guarantee a well behaved signal, however, usually requires an' additional restriction on the minimum high/low times. This restriction is to invalidate traces that spend all their time bouncing up and down, and thus spend no time in Bi and B3 (see figure 4.1). 31 V | ^ "v Figure 4.1: Ricochet Trajectory In order to give the arbiter sufficient time to settle after responding to a change in a client's request status, these minimum times will be stated in terms of time elapsed after the arbiter has acknowledged the. signal change. The restriction for minimum low time is . {Bi(v) A.-ig„) holds for at least TIOW (C2a) where v is either of a or b, and gv is the corresponding grant output signal. The equivalent restriction for minimum high time is ' ' (Bi(v)-A gv) holds for at least Thigh (C20) The combination of these two restrictions is the second requirement of the continuous client , ' C2aAC2b ' (C2) 4.1.2 No Feedback Controllers The final continuous client restriction is unrelated to those above. In order to show that the arbiter almost surely escapes metastability, it is necessary to exclude clients . ' • • '- . -y-:- 32 which are feedback controllers that by careful design or unimaginable coincidence trap the arbiter in the metastable region. This exclusion is accomplished by requiring that the clients be relatively insensitive to variations in the grant lines when waiting for a grant. In real circuits, this insensitivity is achieved by output "metastability filters" that have very low gains when the arbiter is in its metastable region, and thus make it very unlikely that a client would accidently create a controlling feedback loop. To give a quantitative statement of the required insensitivity, let a and b be the request lines, and x and y be the corresponding grant lines. The clients are a-insensitive to the outputs of the arbiter if, given two trajectories that start from states that only differ in their x and y components, the absolute value of the difference of the a and b components of these trajectories is bounded by a times the integral of the absolute value of the differences of their x and y components. This integral is.used as a measure of the history of the outputs observable by the client. A formal definition is given in figure 4.2. The predicate waiting(a, r) holds if both clients wait for a grant throughout the first r time units of the trace that starts at state a. The predicate ClientsSame{o\, a2) holds if the only components of states (Ti and o~2 that differ are x and y. The function gapa[,(o~\,o-2, T) is the difference in the a and b components at time T for traces starting from states o\ and a2, and measures the difference in response between the two traces. The function gapxy(ai,a2, r) is the integral of the differences in the x and y components, and measures the observable difference in the traces' histories. The clients are a-insensitive if the difference in their responses is less than a times the difference in the observable histories. Clients that are feedback controllers are excluded with the following requirement: <>(-i(ri A r2 A —<gi A - ig2) V a-insensitive) (C3) 33 waiting(a,r) = V/9fZ[0,r]. Ti(<p(a,p)) AT2(<p(CT,p)) A ^gi(<p((r,p)) A-ig2(v(o-,p)) ClientsSame(ai,a2) = - ff2| = - x(a2)\ + \y{<ri) - y(<?2)\) gaPabivi^i'T) ~ \a{p(ai,r)) ~ a(>(>2,r))| + \b(<p(cri,T)) - b(<p(a2, r))| ffaPry(o-i.o-2,r) = /J" |ar(y>(o-i,p)) - x (^ ( f7 2 , + |y(y(o-i,p)) - y{<p{°2,p))\dp a-insensitive(cr) = Vo -' £ M d . ClientsSame(<T, a') = > Vr e M+. (waiting(<r, r) A waiting(cr', r)) Where cr is a state, r is a time, and \a\ — <T2| denotes the L 1 norm (sum of absolute values) of the component-wise difference between the two states. Figure 4.2: a-insensitivity If both clients are waiting for- a grant, (C3) requires that eventually a grant will be given or the clients will reach a state where they are a-insensitive to the outputs of the arbiter. It is not required that the clients settle to a specific value or even that the clients settle at all.. While waiting, a and b may wander within the range specified for r i and r2—only the dependence of this wandering on the observed history of x and y is restricted. 4.1.3 An Abstraction Mapping As was stated before, verifying.a continuous model against a discrete specification requires an abstraction mapping. This statement holds true for even the clients— many of the arbiter properties include statements about r i and r 2 , and these discrete states must be translated into regions in the continuous domain in order to reason with the ODE arbiter models. Note that this section does not explicitly mention which continuous variable will be used in these mappings; be aware that any actual ° • . 3 4 model will have a continuous variable associated with each discrete r signal and that the Brockett mappings given here will apply to that variable. Intuitively, the high ( # 3 ) and low {B\) regions of the Brockett ring would make excellent definitions of r and - r respectively. This definition, however, leads to a signal having no discrete value when in regions B2 and B4. Another possible definition would keep B3 r and define -ir as everything else, but would lose some of the symmetry which will be heavily exploited throughout the analysis below. The abstraction mapping which was found to be most useful kept both sym-metry and a discrete definition for a signal everywhere within the Brockett ring. input rising or high = B2 V B3 = #2,3 => r input falling or low = 6 ^ 6 4 = #1,4 => ->T By choosing an abstraction mapping which is defined everywhere on the input Brock-ett ring, and having the restriction that inputs are always within their Brockett ring (Ci), it is possible to invert the mapping as well r «=4> £2,3 '• -,r £1,4 Note that this mapping then has the pleasant property that applying logical oper-ations can be done equivalently in both the continuous and discrete domains. For example r = £2,3 = ~>Bi,4 = " " ( - T ) One possible complaint about this mapping relates back to the argument in section 2.2.4—the continuous input will have a defined discrete value as it passes through the arbiter model's critical parameter values (those places where the model is unstable.and therefore impossible to accurately analyze). But there is not actually 35 a problem. As investigation of the arbiter models will show, the output of the arbiter is always bounded, even when its parameters are near a critical value. And the Brockett ring restriction on the inputs guarantees that the signal will not remain long near the critical parameter value, and so the system will settle to a stable and easily analyzed configuration. In fact, (Cib) combined with the abstraction mapping will show r B3 (4.1) ->r -n^ B\ Furthermore, this equation can be used to state (C2a) in a more useful form. The arbiter's reset property guarantees that the grant will fall within T time units of a falling request. And (4.1) bounds the time between a falling request and B\. Therefore, (C2a) can be restated as r„ holds for at least max(rc, T) + TIOW (C2a) Unfortunately, no similar rewrite is possible for (C2&). A client's request going high does not guarantee that the arbiter will respond with a correspondingly high grant within any bounded time. Even if the arbiter guaranteed liveness, a request by one client might not be answered for an arbitrary period of time if the other client had already received and was keeping the grant. There is no rule symmetric to reset for raised requests, and without such a rule, no revision of (C2&) is possible. 4.2 The Toy Arbiter The first arbiter model considered is a "toy" arbiter. This arbiter has simple ODEs that are amenable to analysis, and many observations from the toy arbiter can be applied to the interlock considered in chapter 6. 36 4.2.1 The Differential Equations The client request lines, a and 6, are the inputs to the toy arbiter. The grant lines x and y are its outputs. All four variables will range between ± 1 , where values near +1 are considered high and values near —1 are considered low. The ODEs defining the dynamic system are and its dual for y. The first term of (4.3) causes x to follow a when y is near — 1. The second term forces x to —1 when y is near +1. The final term causes the system to favor values of x near +1 or — 1—stable fixed points will tend to form in these neighbourhoods, although an unstable fixed point at 0 may also be unavoidably introduced. The behaviour of the toy arbiter is revealed by its phase space portraits as shown in figure 4.3. When a and b are both low, the system has a single attractor with x and y both low.'This .'case corresponds to the discrete state where both requests and both grants are false. When a is low and b is high, the system has a single attractor with x low and y high. States near this attractor correspond to giving a grant to b. The case with a high and b low is symmetric. When a and b are both high, the system has two attractors—one with x high and y low and the other x low and y high. Respectively, these attractors correspond to giving the grant to a.or b. There is also an unstable attractor near the origin. It is this saddle point that gives rise to metastable behaviours. Because the values of a and b are (4.2) which were arrived at by algebraic simplification from x = (1 - y){a - x) - (1 + y)(l + x) + (x - x3) (4.3) 37 0.6^ 1 / -°2|V I / -o.i * I / .«!> W [\ I / -It. * -TTTT1 US// J / / / I / / / / / / / / / / / / / / / j / / / / / / / / / s s 7777T / / / / / / / / / / / / / / / / / / / s / / / s s / / s s s / s s / s s / s s s ~7 / s V I • / / / / / / / / > • / / / / / / / / — s / / / / / s \ \ — s / s s s s s. f \ V •- — — *— ~~ y s s s s s 1 \ \ — - —• ~- ^ / s- s s f \ t \ \ • - — " -- s s > V — *- *f *s ^ f \ \ V — *~ if ^ f \ \ \ -- - - *" f \ \ \ f \ \ \ \ V f \ \ \ \ \ V t \ \ \ \ \ \ t, t \ V N \ \ V V ^ a « -1,6 ss -1 -1, 6 « +1 1 0.8 0.6 0.4 0.2 >- 0 -0.2 -0.4 -0.6 -0.8 -1 fi\ ///// S/ ////// /•/ ////////\ <;////////////////// /// f t \ / / / / / / / / / / n C ^ ^ ^ , , / / / / / / / V ///sss-Z^ in/// v ^ w / / / -~\ \ \ j / / / / s | / / V s' /////////////.//////\' / / / / / / > / / / / / / / / / / / / / / / / / / / 0.5 a w +1, b w +1 Figure 4.3: Phase space portraits for the Toy Arbiter (fixed points marked by "+" for attractors, "o" for the saddle point) 38 not fixed, the exact location of this saddle point can vary. In fact, it can be located anywhere in a region of positive measure (i.e. area > 0). Even with such variations, it can be shown that, with loyal clients, it is not possible to trap a set of trajectories corresponding to a set of initial states with positive measure. This fact leads to the almost surely liveness of the arbiter. 4.2.2 The Abstraction Mapping The development of a suitable abstraction mapping for the toy's outputs is con-siderably more difficult that specifying one on the inputs. Even when the inputs are confined to very symmetric and well-spaced Brockett rings by (Ci), the output of the toy during transitions may be almost spastic in comparison. It is possible, however, to use a Brockett ring as an abstraction mapping for the outputs, albeit a rather distorted instance of the annulus (see figure 4.4). Unfortunately, it has not dv/dt i r +0.05 B, I B, \ S -0.05 +0 5+0.7 f i B'\ I \ yi l l t i l Figure 4.4:,.The Toy's Output Brockett Ring yet been possible to prove that the toy complies with the Brockett restriction on v values. Therefore, this Brockett ring can only loosely be used as the abstraction mapping—it provides bounds on the values of output variables but not their time 39 derivatives. Unlike the inputs, the toy's abstraction mapping for the outputs will not include discrete states for signals in the rising and falling sections of the ring (B2 and B4). The discrete grant signals will be defined as Bi =• (v < 0.5) = • -.g £ 3 (u>0.7) g where v is either of x or y. The clients may interpret signals in the rising and falling regions however they wish, although a discrete signal is only allowed to change value once each time its corresponding continuous variable passes through these undefined regions (for example, as x moves up from 0.5 to 0.7, —igi must hold until some time, after which gi must hold until the output leaves # 3 ( 2 : ) ) . Despite its distortion, this output Brockett ring still makes an excellent abstraction mapping. And there is considerable evidence to indicate that a toy metastability filter could be designed which would map this distorted Brockett ring into the same ring as that used by the inputs, although such a possibility will not be further explored here. One final note must be made about this abstraction function. It appears to allow the toy's outputs to stabilize anywhere below v — +0.5 or above v = +0.7. Since the clients are not allowed to respond to the outputs until #3(t>) or B\(v), the clients appear to require infinite precision—a client must differentiate 0.4999 . . . from 0.5000... even if the output stabilizes arbitrarily close to 0.5. In practice, however, the toy will never stabilize close to the edges of its high and low regions. The primarily reason for the client restriction (C2) is to guarantee that the arbiter's outputs are sufficiently removed from the edges of Bi and # 3 before the client is allowed to initiate another change in system state. Therefore, a client will never 40 need to make a decision when its grant is near a boundary; it can simply wait until the output stabilizes. 4.2.3 The Continuous Model As described in section 3.1, the continuous models investigated in this thesis consist not only of the arbiter's ODEs, but also of the ODEs defining the environment and a probability space describing the initial conditions. Specifying the ODEs for the clients, however, would remove any generality from the result, and is unnecessary in the construction of the proof. The model's ODE system Ftoy merely needs • To satisfy the client restrictions given in section 4.1 with regard to the evolu-tion of arbiter inputs a and b: Ftoy (= Co A C\ A C2 A C3. • To use the ODEs (4.2).to govern the evolution of arbiter outputs x and y: / C Ft0y. • To have no inputs (which includes no explicit reference to time). • To possibly' contain some-hidden variables which may influence the evolution of a and 6, but not x or'y. The probability space of initial conditions will likewise not be completely specified. The restriction placed on it will be that all possible initial conditions for the continuous variables must; map to discrete signal states in which the requests and grants are false—the arbiter and clients must start in a quiescent state. Equivalently, the probability space (Q, P)toy must be drawn from the universe Ut0y = (-1 < a < 0.9) A (-1 < b < 0.9)A • . /•;(-! < x < 0) A (-1 < y < 0) 41 Note that the outputs are restricted beyond just mapping to false discrete values. The size of B\ for x and y is too large to permit them to start anywhere within it. They are therefore restricted to both begin with non-positive values. The continuous model that implements the toy will consist of the ODE sys-tem and the probability space TOy=(F,Q,P)toy This model will have a state vector ° — ( x y a b ... ) which may contain hidden environment variables as already mentioned. 42 Chapter 5 Verification In this chapter, the toy arbiter is shown to fulfill each of the five properties of an almost ideal arbiter; one. section below is devoted to each property. 5.1 Closure Closure, is not a requireme'nt'for the arbiter, but a limitation on what restrictions can be applied to environment. The restrictions in section 4.1 do not constrain the relative arrival time of requests. Accordingly, this requirement is satisfied. 5.2 Mutual Exclusion The requirement is •-'(gi A g 2 ) . By the definition of the abstraction function for G the toy, this is equivalent to •-•((x > 0.7) A (y > 0.7)) which is implied by the statement proven below: D(a; + y < 0). The first step is to show that the arbiter's outputs remain bounded. 43 Lemma 1. If the arbiter's outputs start within the range ± 1 and the client satisfies (C\), then the arbiter's outputs are also bounded in that range TOy\= Bounded{x) A Bounded(y) Proof. Because the dynamic systems under investigation are continuous, showing U(x > — 1) simply requires that (x > — 1) holds initially (as it does by section 4.2.3), and that trajectories along the line (x = — 1) flow in a positive direction—that (x > 0). If all trajectories along (x = — 1) have increasing x values, no trajectory can cross into (a; < —1). From the definition of x (4.2) (x)({a\x = -l}) = a-y-ay + l = {a + l)(l-y) This construction may be read:, when system state a is in the set where (x = —1) holds, x is equal to the function (a + 1)(1 - y). If Bounded(a) A Bounded(y), then both terms of this equation are non-negative and so (a; = — 1) A Bounded(a) A Bounded(y) ==> (x > 0) 0(x > — 1) Similar arguments show that the system maintains 0[x < +1) and Bounded(y) as well. • Theorem 2. The toy satisfies mutual exclusion because one or the other of the outputs is always negative. TOy \= n(x + y < 0) Proof. This requirement is satisfied by the initial conditions. The proof then de-mands that no trajectory can cross from x + y < 0 into x + y > 0. Continuity of trajectories again makes it sufficient to show (x + y = 0) (x + y < 0). Recall-ing the definitions of x and y from equation 4.2, and rewriting them by algebraic 44 manipulation along the line (a; + y — 0) gives {x + y)({a\x + y = 0}) = (26 - 2) + (a - b)(x + 1) = (2a-2) + (6-o)(y+l) For a < 6, examine the first line. C l 0 => 26 - 2 < 0 a < 6 =>• a - 6 < 0 Bounded{x) x + 1 > 0 A symmetric argument can be applied to the second line when 6 < a. Consequently x + y < 0 on the line a; + y =.0 as required. • In addition to proving that the toy satisfies mutual exclusion, these properties are frequently used below in the remaining proofs. They are therefore gathered into Bounded(x) A Bounded(y) A •(# + y < 0) (Ai) 5.3 Reset r Only the proof for •(->ri ~» —gi) is given; the argument for r 2 and g 2 is equivalent. Translating the requirement through the abstraction mappings gives the continuous version. • O & V W ^ B i O * ) ) The proof requires two steps.. The first step is to show that falling or low input leads to a low output, and the second is to show a maximum time bound on the response. The second step will be tackled separately in a lemma before the proof of the first is given in the theorem. 45 Lemma 3. Once a has dropped low (B\{a)), x must follow within bounded time (Bi{x)). Proof. If B\(a) = (a < —0.9) holds, then a negative upper bound can be placed on x in the region ->B\(x) = (x > 0.5). If all trajectories in this region have strictly negative derivatives for their x components, they must all leave the region in bounded time. (x)({a\{a < -0.9) A (x > 0.5)}) = a - l - y - a y - x - x 3 • -y(l + a) + a-(1 + x + x3) < -(-1)(1-0.9)+ (-0.9)-1.625 < -2.425 Since the region within Bounded(x)A(x > 0.5) is only 0.5 units wide, all trajectories will satisfy B\(x) within 0.5/2.425 < 0.21 time units. • Theorem 4. If the input a falls, the output x will follow within bounded time. • ( B i , 4 ( a ) £ £ i ( * ) ) Proof. Returning for a moment to the discrete domain, the client half of the hand-shake (Co) guarantees •(-T t- —»• ->gt). By the definitions of —> and and thus • ( - T i ~> "'gi) is established. All that remains is to1 put a bound on the time taken. It was shown (4.1) that .-iri B\(a). Combining this fact with lemma 3 will produce a suitable time bound of T = TC + 0.21. • 46 5.4 Handshake Again, only the proofs of D(gi -» ->ri) and • (-'gi —> ri) are given. The argu-ments for r 2 and g 2 are symmetric. Mapping through the abstraction function, the requirements are • 02.3(a)) f In fact, a slightly stronger statement will be proven, on the basis of Bi,4(a) =>• (a < 0.9) £ 2 > 3 ( a ) (o>-0.9) Theorem 5. Once high, x will remain so until a has fallen. . . . TPy..(= ((x > 0.7) -> (a < 0.9)) Proof. The same procedure as theorem 2 will be used: proof by showing that all flow along the line (x = 0.7) has a positive x component for (a > 0.9), and therefore all trajectories on the edge of the region in question flow inward until (a < 0.9). Note that attention can be restricted to the region (x + y < 0) because of (*4i), and (x + y <0)A(x> 0.7) (y < -0.7) (x)({a\{a > 0.9) A (x = 0.7)A(y < -0.7)}) = a - y(l + a) - (1 + x + x3) > 0.9 - (-0.7)(1 + 0.9) - 2.0430 ' / > 0.187 • Theorem 6. Once low, x will remain so until a has risen. TOy \= {{x < 0.5) -> (a > -0.9)) 47 Proof. Exactly the same method is used again. In this case the region in question is bounded above, so the objective is to show that x along its boundary is negative. (x)({a\(a < —0.9) A (x = 0.5)}) = a - y(l + a) - (1 + x + x3) < -0 .9 - ( -1 ) (1 -0 .9 ) -1 .625 < -2.425 • 5.5 Liveness, almost surely Only the first half of the proof is given: D(ri ~> ((ri A gi) V (r 2 A g2))). The argument for the second half, a request at r 2 , is equivalent. Note that (4.1) ensures . • ( ' n ' ^ 63(a)) = (ri ~* (a > 0.9)) so it is sufficient to consider the case that (a > 0.9). The proof proceeds by case analysis on b. If 64(b), then b is falling. If gi occurs sometime during 6's fall, then the liveness.requirement is satisfied. Otherwise, r i still holds when 6\(b)—the situation covered in the next case. If B\(b) AB3(a), then all trajectories head towards an attractor located some-where in (x > 0.7) (see figure 4.3). There is a non-empty neighborhood of this at-tractor in which gi is true. UBi(b) is maintained long enough, then the trajectory will enter this neighborhood and satisfy the liveness requirement. Otherwise, r i still holds when 62(b), which leads to the next case. If 62(b) then b is rising. If gi occurs sometime during 6's rise, then the liveness requirement is satisfied. Otherwise, r i still holds when ^3(6), which is the final case. 48 If 63(b), then both clients are requesting a grant. This is the scenario that can lead to metastable behaviours. 5.5.1 Liveness and metastability \ , attractor region cannot be entered region 2 \ region 4 / \ . attractor / ^ \ region region 3 ' region 1 j \ •l-l : ' , • ^ • ] 0 I Figure 5.1: Regions for Liveness Proof The remaining proof obligation is • ((#3(a) A 63(b)) ~> ((62<3(a) A 63(x)) V (62,3(b) A 63(y)))). The proof involves dividing the state space into regions. It is only necessary to analyze trajectories in the region below the (x+y = 0) line because of (.4i). This region is subdivided into four parts, as shown in figure 5.1. The proof below first shows that any trajectory in region 1 will satisfy #2,3(0) A 63(x) after a bounded delay. Likewise, trajectories in region 2 satisfy 62,3(b) /\ 6s(y) with the same delay bound. Next, it is shown that any trajectory can only remain in region 3 for a bounded amount of time. Region 4—the only remaining region—contains the metastable point. As a final step, trajectories are shown to leave this region almost surely and enter region 1 or 2. In the remainder of this section, W\, W2, W3, and W4 are used to denote regions 1 through 4 respectively. Lemma 7. Any trajectory in W\ satisfies B2,3(a) A #3(3:) after a bounded delay, 49 and any trajectory in W2 satisfies 82,3(b) A #3(2/) within the same delay bound. Proof. Only the proof of the first statement is given; the second is symmetric for b and y. Note also that the remaining case from the case analysis above is 63(a) A 53(6); combining this fact with the client's protocol requirement (Co) shows that #2,3 ( a ) A #2,3(&) will hold until liveness is satisfied. Therefore, all that needs to be shown is that #3(2:) will hold within some delay bound. W\ is defined by (x + y < 0.0) A (-0.4 > y - 2x) A (y > -1) It is straightforward to show that anywhere in this region (x > —0.3) and (x > 0.0176) (the minimum for x' occurs at a = 0.9, x = 4/30, y = -4/30). Such a positive x guarantees that (x > 0.7) after at most (0.7 — (—0.3))/0.0176 < 57 time units (a very loose upper bound). All trajectories in W\ will satisfy B3(x) within 57 time units. Likewise, all trajectories in Wi will satisfy #3 (2/ ) within 57 time units.' ' •- . ; . • Lemma 8. Any trajectory in W3 leaves in bounded time. Proof. Region 3 is defined by (x + y< -0.2) A (-0.4 < y - 2x) A (-0.4 < x - 2y) A (x > -1) A (y > -1) It is easy to show that anywhere in this region (x+y > 0.37) (all flow is up and to the right), which proves that all trajectories must eventually leave the region. Because (—0.2 — (x + y) < 1.8), a trajectory must leave W3 after at most 1.8/0.37 < 5 time units. • The region that remains to be considered is W4. Region 4 contains the saddle point and the location of this saddle depends on the values of a and b, so the saddle 50 may move slightly even with 63(a) A 63(b). By (C3), either a grant is issued or the clients become ct-insensitive; it is sufficient to consider the latter case. Lemma 9. Once the clients become a-insensitive, trajectories in W4 will escape almost surely. Proof. Consider two states, o\ and a2 in W4 such that waiting(u\) A waiting(a2) A ClientsSame(ai, a2) ^ A f>(<ri) + y(oi)) = (x(a2) + y(o2)) A (ar(ffi) - ^ (x(a2) - y(a2)) It is shown that trajectories <p(o~i,-) and <p(a2,-) emanating from o\ and a2 must diverge; therefore, at most one of them remains in W4 indefinitely. This proof will demonstrate that the dimension of the set of states whose trajectories remain trapped in W4 is at most d — 1. Because dimension is preserved (3.1), this set of trapped states corresponds to a set of initial states of dimension at most d — 1, and this initial state set has probability zero by the smoothness requirement for the initial state probability function P (3.2). The initial state set which escapes the metastability thus has probability one, and so escape occurs almost surely. The remainder of this section is divided into two parts: • The proof that the trajectories <p(cr\, •) and <p(a2, •) diverge—that the distance between them in the x-y plane increases as time increases. • An explanation of why this divergence implies the dimension of the set of trapped states is at most d — 1. 51 For the rest of this analysis, it is convenient to perform a change of variables. Let u = x — y c = a-\-b v = x + y d — a —b Rewriting (4.2) yields the toy's dynamical system in the new coordinates: u = d + uc/2 - vd/2 - u3/A - Zuv2/A (5.2) v = c-2 - v + ud/2 - vc/2 - v3/4 - 3vu2/4 Let r e R + such that Vp G [0, r]. waiting(ai,T) A waiting^, T) Let u\(p) be the u component of (p(ai,p), u2 be the u component of </?(<72,/9), and Au = u 2 — u\. Define v\, u2, Au, c\, c2, Ac, d\, d2).and Ad in the same way. The proof is based on.a double cone in u-v space with the vertex at (p(ai, •) and the axis lying parallel to v — 0. Note that the vertex will move as <p(ai, •) moves. At p = 0, <^ (cr2, •) will be inside this cone, since i>2(0) — vi(0) = Au(0) = 0. Mathematically, the cone is defined by (where kv is some positive constant) . |Av| < \Au\/kv (5.3) Showing that ¥>(<7i, •) and y(cT2, •) diverge then requires demonstrating two proper-ties: • All trajectories in the cone diverge from the vertex in the u direction. In this case, Au >kAu for,some fixed k > 0 in the cone. • All trajectories that enter the cone stay in the cone. If trajectories are diverg-ing in the u direction already, then Av < —kAv (for some other fixed k > 0) holding along the edges of the cone will ensure such trapping behaviour. '- ; - - , -'52 Without loss of generality, assume Au > 0, and then consider the case where Av > 0; the other case is equivalent. In order to establish the two properties stated above, a loose lower bound on Au in terms of Aw and a loose upper bound on Av in terms of Av is determined. Finding these bounds requires finding a relationship between Ac, Ad and Au (Av is taken care of by the definition of the cone). Such a relationship can be established by placing an additional restriction on Au AU(T) >ku I \Au(p)\ + \Av(p)\dp (5.4) Jo and then rewriting the earlier, definition of a-insensitive in the new variables \AC(T)\ + \Ad(r)\ < 2a f \Au(p)\ + \Av(p)\dp Jo or (5.5) (5.6) |Ac(r)| < -2a^\Au(p)\ + \Av(p)\dp \Ad(r)\ < 2aJrJ\Au(p)\ + \Av(p)\dp Combining (5.4) and (5.5) gives the required relationship: |Ac| < 2a\Au\/ku \Ad\ < 2a\Au\/ku That (5.4) is merely a tightening of an already stated restriction can be seen by differentiating it and using the definition of the cone AU(T) > * u ( |A«(r) | + |Ai;(r)|) ( 5 ? ) •"''•"'"'> ku(l + l/kv)\Au(T)\ Which again requires Aii to be a positive function of Au. Intuitively, this equation is providing a lower limit on the rate of exponential divergence of trajectories in the u direction. 53 With Av, Ac, and Ad related to Au, it is possible to find a lower bound in W4 for Ail as a function of Au, a, kv, and ku (starting from the rewritten dynamical system (5.2)) Aw > (0.815625 - 2A5a/ku - 0A175/kv)Au For more details on obtaining this equation and those in the rest of the proof, see appendix A. Combining this equation with the requirement given by (5.7), an inequality on a, kv, and ku is found 0.815625 - 2A5a/ku - 0.1175/fc„ - ku - ku/kv > 0 (5.8) An assignment to a, kv, and ku which satisfies this inequality will guarantee that points within the cone will diverge from the vertex. In the search for an upper bound on Av, it is possible to replace the inequality defining the cone (5.3) with \Av\ = |Aw|/A;„ since only the value of Av along the edges of the cone is of interest. This replacement enables Ac and Ad to be directly related to Au, which in turn allows an upper bound to be placed on Av . . . Av < (-1.9 + 0.1175^ + 2A5akv/ku)Av Since a trapping cone requires Av to be a negative function of Av, this upper bound becomes the.inequality -1.9 + 0.1175fc„ + 2A5akv/ku < 0 (5.9) Which, for feasible a, kv, and ku, guarantees that trajectories that enter the cone cannot leave. Any assignment of a, ku, and kv which satisfies (5.8) and (5.9) will guarantee that ip((J2, •) will remain within the cone and that it will diverge from the vertex (and . 5 4 thus <p(o~i, •)). Because W4 has bounded extent, at least one of the diverging <p(ai, •) and <p((T2, •) must escape W4—completing the proof of divergence. An example of a feasible assignment is a = 0.05 ku = 0.35 = 4.06 The remaining task is to show that the divergence of <p(<7i,-) and <p(a2,-) implies that the set of trapped states is of maximum dimension d — 1. The system state is represented by the vector o~ = {x y a b ...) = (u v c d ...) which has dim(a) = d. Now consider the subvector = (v c d ...) which contains all state variables except u. For any set of assignments to <7-,u, there may be a choice of u\ such that the trajectory <p(ai, •) starting at o\ = (Ul a-,u) becomes trapped. But then any trajectory </>(<72,') starting at a state 02 = (u2 CT-,U)) which differs from <j\ only in the u. value, will escape. This fact is proven by the diver-gence argument above. From (5.1), the states <Ti and 02 chosen for the divergence argument differed only in their u values: ClientsSame(ai, <72) states that the c, d and hidden variables are the same for both states; (x(ai) + y(oi)) = (x((T2) + y{&2)) can be rewritten as (u(<Xi) =.w(<72)); and (x(ai) — y(o~i)) ^ (%(<?2) — y{cr2)) states that the u- values differ. The trajectories starting at these two states were shown to diverge, so if (p((Ji, •) is trapped then < (^c2, •) must escape. Therefore, at most one value of u for any choice of a^u lies on a trapped trajectory. This value of u can be written as a function of the other variables 55 Ufrap — /(o'-m)—the function will not be defined for values of a~,u where no state can become trapped. The manifold in Kd defined by /(<T_,u) is of maximum dimension d — 1, and if trajectories can only become trapped if they start from the manifold, then the set of trapped trajectories is likewise of maximum dimension d — 1. As stated at the beginning of the proof, preservation of dimension (3.1) shows that the initial state set leading to the trapped trajectories must be of the same maximum dimension, and the smoothness of the initial probability distribution (3.2) implies that escape occurs almost surely. • Theorem 10. The toy satisfies liveness almost surely. Proof. The case analysis showed the the toy would satisfy liveness eventually unless both requests ended up high. In the case where both requests were high, the x-y state space was broken into regions. Equation (Ai) requires that no trajectory enter the region x + y > 0. Lemma 8 showed that trajectories in W3 would enter W\, W2, or W4 in bounded time. By lemma 9, trajectories which enter W4 will escape almost surely (if suitably a-insensitive clients are used), and since they cannot reenter W3, they must go into W\ or W2. And lemma 7 showed that all trajectories in W\ or W2 will satisfy liveness within bounded time. • 56 Chapter 6 The Seitz Interlock From an analysis point of view, the toy arbiter's simple equations make it an ideal development platform. It is, however, far from an operating VLSI circuit. Once techniques have been tried on the toy, it is hoped they can be applied to a real arbiter circuit. In this thesis, Seitz's interlock circuit [Sei79] will serve as the second arbiter model. It is a widely used and well studied VLSI arbiter design. As mentioned in section 2.2.5, Kurshan and McMillan [KM91] have published a verification of this arbiter. Their verification was based on model checking using a coarsely quantized representation of the phase space and a next state relation obtained by numerical integration. Their analysis could not, however, provide any guarantees that the arbiter would eventually leave the metastable region. Instead, they avoided the issue by adding an assertion that the arbiter escaped the metasta-bility. Since this assumption does not hold for any real arbiter, its inclusion in their model is unsatisfying. Figure 6.1 shows Seitz's arbiter. Transistors q4, q5, q9 and qlO are depletion mode transistors (threshold voltage Vt < OV), and act as pull-up resistors in this 57 +5V PdHS1 qui +5V p(2Hg> q7]| T x(l) x(2) +5V r^Q5 T Cloadl +5V 10 x(4) Cload2 Figure 6.1: Seitz Interlock Circuit configuration. The remaining transistors are enhancement mode (Vf > OV). The six transistors to the left of line kk form a cross-coupled pair of NOR gates. These transistors are the heart of the interlock—the internal arbiter—and like all arbiters they are subject to metastable states. The remaining four transistors to the right of kk are the metastability filter. To turn the circuit into an ODE system, a standard first-order transistor model is used (the same model.as Kurshan and McMillan). The transistors are con-sidered to be perfect voltage controlled current sources with constant capacitances from gate to source (see figures 6.2 and 6.3). This model ignores non-linear capacitances, subthreshold conduction and short channel effects such as channel-length modulation and drain-induced threshold lowering. The transistor parameters Vt, K, and S are also assumed to be fixed and equal for all transistors of similar type. 58 drain ds . © I ds gs source gs Figure 6.2: Transistor Model (from [KM91]) '0 . HVgs < Vt (cutoff) ' . Ids• = I KSVds(2(Vgs-.Vt)-Vds) if Vgs > Vt and Vds < Vga - Vt (linear) . KS(Vgs- VtY itVgs>Vt and Vd, > Vgs - Vt (saturation) Where the transistor parameters are threshold voltage (Vt), transconductance (K), and shape factor (5 = W/L) Figure 6.3: Transistor Model Equation Unlike the toy, the interlock uses a combination of active high and active low signals. Both the inputs and outputs are active low—external requests and grants occur when the signal itself is below transistor threshold (typically 0.6V [GD85]). The internal signals x(l) and x(2) are active high, although the metastability filter operates more on the.difference-between the two rather than based on any absolute value. It is the internal arbiter that generates mutually exclusive grant signals, and so the metastability filter will be ignored in this analysis—x(l) and x(2) will be . used as the outputs. Choosing process parameters appropriate to a 2 fim nMOS process [GD85, p. 453] produces the phase portraits shown in figure 6.4. Like the toy, there.is only one attractor in the system unless both inputs are asserted. In this final case there are two attractors and a single, central saddle point. 59 V t \ 1 \ I / I / I / « 3 • I / \ 1 \ 1 2\ \ 1 V \ 1 ,> \ 1 \ 1 0 > + / '/ / S / SS S S / / A / / S / S S S S S / S / / / / / / / / / / / / / / / / / / / / / ; //S/S////// ^ *~ - ~-f *\ • ~- ^ s A —- --' s s ' ~" s s s s s s s s ' *s S x-3K-ok p(l) « 5V, p(2) « 5V n». v ^ i ™" •« 5h-^ / ^ / / / s / / / \ ^ \ v t \ I A . / \ • / \ / \ v •v • \ V \ \ t \ I t / / / / / • / :/ / s / > / / / / / / v ^ — I I o / / _ / s -— - * S -~ — — -» x(1) p(l) sa 5V, p(2) ^ ^ / S S / / - ^ ^ ^ y s / / / / •-*•*'<' s /// J f - • • • / / / / / • " - ' • • / / / / / • ' ' / / / i l l • ' / / I i I I I • ' / / / / / / / ' M I I I | I' | > t i ; i i i l l ^ \ \ \ i i l ^ v \ \ \ \ \ i - >. \ \ \ \ \ \ \ ^ v \ \ \ \ \ >- >. \ \ \ / / / / / / / / / / / / / / / / / ! • f f f f t t t t t t t t f t t t t t wOV s / / / / / / J / / / / / / / / / / / / / / / / / / A / / / / / / / / / 0 1 2 3 4 5 x(1) . p(l) w 0V, p(2) « 0V Figure 6.4: Phase space portraits for Seitz's arbiter (fixed points marked by "+" attractors, "o" for the saddle point) 60 A comparison of figures 4.3 and 6.4 shows that the interlock's dynamic system and the toy's are qualitatively the same. It is therefore not surprising that proofs of closure, mutual exclusion, reset, and handshake equivalent to those in chapter 5 could be constructed. Because the model is more complex, numerical optimization would be required when verifying bounds on the flow. The proof of liveness was actually simpler for the interlock than for the toy. This is due to the first order transistor model that ignores subthreshold conduction. When an input is asserted, it is below the enhancement device threshold voltage and the currents into nodes x(l) and x(2) are independent of variations in the inputs. The location of the saddle-point is therefore fixed, and its stable manifold is of dimension d — 1. Increasing the sophistication of the circuit model to include subthreshold conduction would result in movement of the saddle-point with varying inputs. However, this movement would be much smaller in relative terms than for the toy. Therefore, an argument similar to the one in section 5.5 should apply. A more accurate transistor model has not been adopted in the hope that further research may make it unnecessary. By analyzing the linear behaviour of the arbiter systems near the metastable point, it is hoped that a quantitative estimate of the effects of model inaccuracies can be developed. If it is known that further refinement of the transistor model will produce some maximum perturbation of the current model that is less than that needed to invalidate the proofs, then the additional refinement is unnecessary. .The never-ending list of terms that can be added to a'transistor, model .for more accuracy is-thus truncated at a reasonable length. Such a "proof despite inexact models" has not yet been formalized however, and the idea is presented here merely to explain the lack of more accurate transistor modeling in this chapter. 61 Although the internal arbiter is the most interesting component of the cir-cuit from the viewpoint of arbitration, it would be negligent to leave out at least an informal description of the right-hand portion of the circuit. The metastability filter operates on a simple principle—if the internal signals do not differ by more than a transistor threshold, there has certainly not been a successful arbitration, and there-fore both outputs should remain high (remember, a grant is output low). Only when one internal signal is significantly above the other will the first signal's filter transis-tor turn on and lower its output level. In a circuit model that neglects subthreshold conduction, this filter makes the outputs of the arbiter, a;(3) and x(4), independent of the internal nodes a;(l) and x{2) when the arbiter is near the metastable point. Even if subthreshold conduction is taken into account, the filter will not allow a grant until any metastability has been resolved, and has gain very close to zero near the metastable point. In addition to hiding metastability, the filter "cleans up" the output signal. It is conjectured that such filters can re-map the reachable state space of the outputs of an arbiter—for example, re-map the ugly output Brockett ring of the toy into a ring identical to the much nicer input Brockett ring—but no attempt at such a proof has yet been made. 62 Chapter 7 Conclusions 7.1 What has been.Accomplished In an asynchronous environment, a perfect arbiter cannot be built. The permanent indecision of metastability is an inescapable component of the mutual exclusion problem. But for a large class of clients, the probability of the arbiter never making a decision is exactly zero. . . . This thesis studied the-problem of verifying the correct operation of arbiters. Traditionally, hardware verification techniques have needed to build discrete mod-els of circuits before verifying the model against a discrete specification. Because metastability is a decidedly. continuous behaviour, a discrete model cannot do it justice. A continuous modeling environment is needed. Dynamic systems provide just such an environment. Two potential arbiter systems were described. The toy is a collection of very simple ODEs, making it possible to use many analytic and algebraic techniques in its examination. The Seitz interlock is a well studied,and commonly used VLSI design, and its dynamic 63 system model was constructed from a popular and reasonably realistic first order ODE model for MOS transistors. Verification of a continuous model against a discrete specification requires, in addition to the model, three more ingredients: • The discrete specification, in this case a precise description of the properties of an ideal arbiter. • An abstraction mapping which maps from the continuous to the discrete and back. • A temporal logic which allows proof of discrete formulas using the abstraction mapping and dynamic system model. Each of these items was drawn from verification literature in either the metasta-bility or dynamic systems field. The specification, adopted from Mendler and Stroup [MS93], gives a precise yet general definition of a two client arbiter. The primary abstraction mapping is the Brockett ring [Bro89] which, along with its other favourable properties, allows a signal's continuous value to vary even when its discrete value is fixed. The temporal logic is being developed by Greenstreet, and the arbiters represent its first full-scale use in verification. Combining these elements made it possible to prove that the toy obeys all properties of an ideal arbiter save liveness. For most clients, the toy arbiter would eventually make a decision and satisfy liveness with probability one, a proof ac-complished without requiring fixed inputs. The only clients excluded are high-gain feedback controllers that trap the arbiter at the metastable point—a highly unlikely design for a useful client. The. proofs of the first four ideal arbiter properties for the Seitz interlock are similar and were omitted, while an analogous proof of liveness 64 for the interlock was made trivial by the simplicity of the transistor model. In conclusion, this research has shown the effectiveness of the temporal logic and abstraction mappings in formal proof that a continuous dynamic system fulfills a discrete specification. In addition, it has provided a firm foundation for further exploration of arbiters using this paradigm. 7.2 Suggestions for Further Research Study of these arbiter models is not yet finished. As mentioned in the body of the thesis, the models investigated are designed to be used for at least two further explorations. The first is to show that the toy arbiter, and possibly thereafter the Seitz interlock, can act as clients for themselves. This objective would involve designing a dynamic system to act as a metastability filter for the toy. This filter would map the toy's outputs such that -their reachable state space would fall within the ring used for the toy's inputs. By showing that the outputs obey the restrictions on the inputs, it becomes possible to build multi-client arbiters through chains or trees of two-client arbiters. But before more work can be done on the interlock, the deficiencies of the model must be addressed..: Instead of simply adopting a more accurate transistor model, which—no matter how. many more terms are added—will never be perfect, it should be feasible to develop a quantitative estimate of how much variation in the model would render the current results invalid. It is possible to estimate the maximum magnitude of the effects of refinements in the transistor model. If that magnitude is less than the allowable model variation, then no further refinement is necessary, since the results will remain valid regardless. 65 Three additional avenues of research could use this material as a starting point. Unlike the two ideas above, those below have not yet been investigated to any length. • The interlock is the only VLSI arbiter analyzed using this technique; however, arbiters are such common circuit elements that many other designs exist which could be verified. These designs may have different protocols or objectives than the interlock, and so both continuous models and discrete specifications would need to be developed. • Although ignored here, noise is an extremely important and well studied ef-fect in real circuits; consequently, it would be nice to investigate its effects on the arbiters. The argument about diverging traces from section 5.5 sug-gests an exponential "stretching" process that is relatively insensitive to small variations in the signals. This insensitivity hints that noise may be inconse-quential in arbiters from a probabilistic perspective—a number of papers have claimed similar statements about synchronizers [Vee80, HLS84]. That liveness is fulfilled almost surely has required the introduction of probability into this research. Hopefully the stretch to including noise by stochastic differential equation techniques, would not be too great. • One of the largest emphases in the verification community is the push towards automation. In the actual verification of real systems, theory has always out-stripped practice because the amount of training needed to apply the theory made its commercial use impossible. The same is true of the methods used above, but automation may be possible. Hytech [HH95] is already using tech-niques similar to those used in the continuous analysis of the arbiters. It 66 may, in time, be possible to construct a theorem checker containing the same temporal logic rules used in this research. 67 Bibliography [Bla94] Robert D. Black. Towards a dynamical systems approach to asynchronous circuit design, internal report, University of Waterloo, April 1994. [Bro89] R. W. Brockett. Smooth dynamical systems which realize arithmetical and logical operations. In Hendrik Nijmeijer and Johannes M . Schumacher, • editors, Three'Decadesi of Mathematical Systems Theory: A Collection of Surveys at the Occasion of the 50th Birthday of J. C. Willems, volume 135 of Lecture Notes in Control and Information Sciences, pages 19-30. Springer-Verlag, 1989. [Cha84]. Daniel M. Chapirp. .Globally-Asynchronous, Locally-Synchronous Systems. PhD thesis, Department of Computer Science, Stanford University, Octo-ber 1984. Tech. Report STAN-CS-84-1026. [CM73] T.J. Chaney and C.E. Molnar. Anomalous behavior of synchronizer and arbiter circuits. IEEE Transactions on Computers, C-22(4):421-422, April 1973. [GD85] Lance A. Glasser and Daniel W. Dobberpuhl. The Design and Analysis of VLSI Circuits. Addison-Wesley, 1985. 68 [Gre96] Mark R. Greenstreet. Verifying safety properties of differential equations. In Proceedings of the 1996 Conference on Computer Aided Verification, New Brunswick, NJ, July 1996. to appear. [HH95] Thomas A. Henzinger and Pei-Hsin Ho. Algorithmic analysis of nonlinear hybrid systems. In Proceedings of CAV 95, pages 225-238, 1995. [HLS84] Jakob H. Hohl, Wendell R. Larsen, and Larry C. Schooley. Prediction of error probabilities for integrated digital synchronizers. IEEE Journal of Solid-State Circuits, SC-19(2):236-244, April 1984. [HS74] Morris W. Hirsch and Stephen Smale. Differential Equations, Dynamical Systems, and Linear Algebra. Academic Press, San Diego, CA, 1974. [Hur75] Marco Hurtado. Structure and Performance of Asymptotically Bistable Dynamical Systems. PhD thesis, Sever Institute, Washington University, Saint Louis, MO, 1975. [HW41] Witold Hurewicz and Henry Wallman. Dimension Theory. Princeton University Press, 1941. [KM91] R.P. Kurshan and K.L. McMillan. Analysis of digital circuits through symbolic reduction. IEEE Transactions on Computer-Aided Design, 10(11):1356-1371, November 1991. [Mar81] L.R. Marino. General theory of metastable operation. IEEE Transactions on Computers, 30(2):107-115, February 1981. [MS93] Michael Mendler and Terry Stroup. Newtonian arbiters cannot be proven • correct! Formal Methods in System Design, 3(3):233-257, December 1993. 69 [Nag75] L.W. Nagel. SPICE2: a computer program to simulate semiconductor circuits. Technical Report ERL-M520, Electronics Research Laboratory, University of California, Berkeley, CA, May 1975. [Pnu81] Amir Pnueli. The temporal semantics of concurrent programs. Theoretical Computer Science, 13:45-60, 1981. [RRH93] Anders P. Ravn, H. Rischel, and K.M. Hansen. Specifying and verify-ing requirements of real-time systems. IEEE Transactions on Software Engineering, 19(l):41-55, 1993. [Sei79] Charles L. Seitz. System timing. In Introduction to VLSI Systems (Carver Mead and Lynn Conway), chapter 7, pages 218-262. Addison Wesley, 1979. [Vee80] Harry J.M. Veendrick. The behavior of flip-flops used as synchronizers and prediction of their failure rate. IEEE Journal of Solid-State Circuits, SC-15(2):169-176, April 1980. 70 Appendix A Details of Divergence Proof In addition to the variables defined earlier, define uavg = (ui + U2)/2 and vavg, cavg, davg similarly. With these definitions, it is possible to write the derivative of the divergence of the two trajectories (starting from (5.2)): Au =. Ad + l/2(cavgAu + uavgAc) - l/2(davgAv + vavgAd) -l/4:Au(u2l + u2u1 + ul)-3/4(l/2)(Au(v%+vl)+4uavgv Av = Ac-Av+l/2(davgAu + uavgAd) - l/2(cavgAv + vavgAc) - l /4Au(u | + v2Vi + v\) - 3/4(1/2)[Av(u22 + u\) + 4uavgvavgAu) Since the states under investigation are in W\ and both are waiting, (loose) bounds can be placed on all basic variables involved -0.3 < u < 0.3 -0.15 < v < 0 1.8 < c < 2.0 -0.1 < d < 0.1 The definition of the cone gave a relation (5.3) between Av and Au \Av\ < \Au\/kv 71 while (5.6) related Ac and Ad to Au. \Ac\ < 2a\Au\/ku \Ad\ < 2a\Au\/ku A minimum for Ail in terms of Au can now be found. Note that most terms in this expansion can be chosen positive or negative because of the absolute value signs in the bounds above. In these cases, the sign is chosen so that the term as a whole has the worst (most negative) value. The only terms which cannot change sign are c (always positive), y (always negative), and squares. The latter two values have zero in their range,.so that if the term cannot be made negative, the term is zeroed out of the equation. The (very loose) bound calculated in this way is: Aii ^ Admin -\- l /2(c m ; n Au -f- uminAcmax) \/2(dmaxAvmax -f- fm,nA(fmi B) • - l / 4 A u ( 3 ^ a a . ) 3 / 4 ( A u u ^ i n + 2umaxvminAvTnin) > -2aAu/ku + l/2((1.8)Au + (-0.3)2aAu/ku) -l/2((0.1)Au/kv+{-0.15){-2aAu/ku)) -3/4Au(0.3)2 - 3/4(Au(-0.15)2 + 2(0.3)(-0.15)(-Au/fc„)) > .(0.815625 - 2A5q/ku - 0.1175/A:„)Au The differentiated requirement (5.7) that needed to be satisfied by Aw is A u > ku(\Au\ + \Av\) > ku(l+l/kv)Au Combining these.two inequalities yields the final restriction (5.8) placed on a, ku, and kv by Au 0.815625- 2A5a/ku - 0.1175/^ > ku{l + l/kv) 0.815625 - 2A5a/ku - 0.1175/A;,, - ku - ku/kv > 0 Replacing the definition of the cone by |Au| = lAwl/fc ,^ a loose upper bound on Av can be found through similar substitutions. For upper bound calculation, terms are chosen most positive (or zeroed if no positive value is possible) Ai) ^ Acmax Av -\- \J 1{dmaxAumax ~\~ umaxAdmax) l /2(c m i n Au + vminAcmax) - l / 4 A w ( 3 i 4 . - n ) - Z/A{Avu2min + 2umaxvminAv) < +2aAv/ku - Av + l/2((0.1)&„Ai; + (0.3)2akvAv/ku) • -l/2((1.8)Av+(-0.15)(2akvAu/ku)) -0 - 3/4(0 + 2(0.3) (-0.15) (fc„Au)) < (-1.9 + 0.1175fc„ + 2Abakv/ku)Av Since Av need only be a negative function of Av (we didn't need any more restrictions), the last line is the required inequality (5.9) -1.9 + 0.1175^ + 2A5akv/ku < 0 73
- Library Home /
- Search Collections /
- Open Collections /
- Browse Collections /
- UBC Theses and Dissertations /
- Proving Newtonian Arbiters Correct, almost surely
Open Collections
UBC Theses and Dissertations
Featured Collection
UBC Theses and Dissertations
Proving Newtonian Arbiters Correct, almost surely Mitchell, Ian M. 1996
pdf
Page Metadata
Item Metadata
Title | Proving Newtonian Arbiters Correct, almost surely |
Creator |
Mitchell, Ian M. |
Date Issued | 1996 |
Description | An arbiter is a circuit that grants its clients mutually exclusive access to a shared resource. The ideal arbiter cannot be built—either requests must occur synchronously, mutual exclusion is not guaranteed, or the arbiter may become hung indefinitely and fail to make a decision. This thesis explores arbiters whose failure mode is the latter; they are not live. Two specific arbiters are investigated: a "toy" arbiter, whose model was chosen for its .tractability; and Seitz's nMOS interlock, which was chosen as an example of a widely used and studied design. Both arbiters are modeled by nonlinear continuous dynamic systems, and both models are Newtonian: given an initial set of system states, the future image of that set has exactly the same dimension. The toy is shown to be almost surely live—with probability 1, the arbiter eventually, grants some pending request—while still satisfying all the other properties of an ideal arbiter. The analysis is more general than previously published results in that the inputs of the arbiter may vary while the arbiter is metastable, and conditions are given that ensure liveness even in the presence of such variations. The verification is accomplished by proof that the set of states forever trapped in the metastable region of the toy is lower dimensional than the state space of the toy as a whole. Parallels between the toy and the interlock can then be drawn. |
Extent | 3096175 bytes |
Genre |
Thesis/Dissertation |
Type |
Text |
FileFormat | application/pdf |
Language | eng |
Date Available | 2009-03-16 |
Provider | Vancouver : University of British Columbia Library |
Rights | For non-commercial purposes only, such as research, private study and education. Additional conditions apply, see Terms of Use https://open.library.ubc.ca/terms_of_use. |
DOI | 10.14288/1.0051593 |
URI | http://hdl.handle.net/2429/6067 |
Degree |
Master of Science - MSc |
Program |
Computer Science |
Affiliation |
Science, Faculty of Computer Science, Department of |
Degree Grantor | University of British Columbia |
GraduationDate | 1996-11 |
Campus |
UBCV |
Scholarly Level | Graduate |
AggregatedSourceRepository | DSpace |
Download
- Media
- 831-ubc_1996-0608.pdf [ 2.95MB ]
- Metadata
- JSON: 831-1.0051593.json
- JSON-LD: 831-1.0051593-ld.json
- RDF/XML (Pretty): 831-1.0051593-rdf.xml
- RDF/JSON: 831-1.0051593-rdf.json
- Turtle: 831-1.0051593-turtle.txt
- N-Triples: 831-1.0051593-rdf-ntriples.txt
- Original Record: 831-1.0051593-source.json
- Full Text
- 831-1.0051593-fulltext.txt
- Citation
- 831-1.0051593.ris
Full Text
Cite
Citation Scheme:
Usage Statistics
Share
Embed
Customize your widget with the following options, then copy and paste the code below into the HTML
of your page to embed this item in your website.
<div id="ubcOpenCollectionsWidgetDisplay">
<script id="ubcOpenCollectionsWidget"
src="{[{embed.src}]}"
data-item="{[{embed.item}]}"
data-collection="{[{embed.collection}]}"
data-metadata="{[{embed.showMetadata}]}"
data-width="{[{embed.width}]}"
async >
</script>
</div>
Our image viewer uses the IIIF 2.0 standard.
To load this item in other compatible viewers, use this url:
http://iiif.library.ubc.ca/presentation/dsp.831.1-0051593/manifest