UBC Theses and Dissertations

UBC Theses Logo

UBC Theses and Dissertations

Formal verification of asynchronous data-path circuits Weih, David T. 1996

Your browser doesn't seem to have a PDF viewer, please download the PDF to view this item.

Item Metadata

Download

Media
831-ubc_1996-0294.pdf [ 4.44MB ]
Metadata
JSON: 831-1.0051420.json
JSON-LD: 831-1.0051420-ld.json
RDF/XML (Pretty): 831-1.0051420-rdf.xml
RDF/JSON: 831-1.0051420-rdf.json
Turtle: 831-1.0051420-turtle.txt
N-Triples: 831-1.0051420-rdf-ntriples.txt
Original Record: 831-1.0051420-source.json
Full Text
831-1.0051420-fulltext.txt
Citation
831-1.0051420.ris

Full Text

Formal Verification of Asynchronous Data-Path Circuits by David T. Weih B.Sc, University of British Columbia, 1992 A THESIS SUBMITTED IN PARTIAL F U L F I L L M E N T OF T H E REQUIREMENTS FOR T H E D E G R E E 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 April 1996 © David T. Weih, 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 The University of British Columbia Vancouver, Canada DE-6 (2/88) Abstract Asynchronous designs are typically modelled with non-deterministic next-state re-lations. When a deterministic model is available, specialised verification techniques can be used to automatically verify relatively large designs. This thesis demonstrates that verification techniques developed for deterministic models can be applied to speed-independent self-timed circuits. We introduce local formulas, and show that the validity of a local formula is independent of the order in which the components of a speed-independent circuit perform their operations. Local formulas provide a natural way to specify the input/output behaviour of a circuit and are well-suited for specifying data-paths. We demonstrate the practicality of our approach by de-scribing the verification of three designs: a F IFO, an adder, and a vector multiplier chip. Contents Abstract ii Contents iii List of Figures v Acknowledgements vi Dedication viii 1 Introduction 1 1.1 Formal Verification Techniques 2 1.1.1 Theorem Proving 3 1.1.2 O B D D Based Model Checking 4 1.1.3 Symbolic Trajectory Evaluation 5 1.1.4 The Voss Prover 6 1.2 Automatic Verification of Asynchronous Data-Path Circuits 7 1.3 Related Work 8 1.4 Overview of Thesis 10 iii 2 Theory 12 2.1 The Circuit Model 12 2.2 Definitions 16 2.3 A Specification for the F I F O 23 2.4 Properties of Speed-Independent Circuits 25 2.5 Discussion of Hypotheses 30 3 Local and Global Formulas 32 3.1 Local Formulas 33 3.2 Global Formulas and Period Functions 35 3.3 Unspecifiable Behaviour 39 4 Implementation 40 4.1 V H D L Circuit Descriptions 40 4.2 Symbolic Trajectory Evaluation 42 4.3 Model Checking for Speed-Independence 46 5 Vector Multiplier 48 6 Conclusions 53 6.1 Future Work 54 Bibliography 57 Appendix A Proofs 62 Appendix B Source Code 74 iv List of Figures 2.1 A Self-Timed FIFO 13 2.2 Splicing Traces 21 3.1 4 Bit Adders 33 3.2 Adder Environment 34 3.3 Pipelined Asynchronous Adder 37 3.4 Global Formula for Pipelined Adder 38 3.5 Global Formula for Flat Adder 38 4.1 VHDL Code for Source Component 43 4.2 VHDL Code for Sink Component . 44 4.3 VHDL Code for FIFO Cell • • v 4 5 5.1 Bit Slice of the MAS Block 50 6.1 Vector Multiplier: Abstract State Machine 55 v Acknowledgements I owe a great debt.to Mark Greenstreet, who was a tremendously helpful supervisor. Some of the material in this thesis was prepared in collaboration with Mark as a paper for IEE Proceedings - Computer and Digital Techniques. The theoretical framework presented in Chapter 2 owes its clarity to his suggestions. I would also like to acknowledge the ISD group for making hardware verifi-cation a lively and social pursuit. In particular, Mike Donat and Mark Aagaard let me practice explaining my ideas to them, while Andy Martin essentially took a two day holiday from his own work to help me prove a theorem. Finally, I would like to thank my family and other friends who supported me in many ways during my thesis. M y parents and grandparents encouraged me and provided some very practical support. Mike Wilson and Jen Weih gave me with the opportunity to occasionally escape from work. And last but not least, deep thanks to Andrea, without whom nothing would have been the same. D A V I D T . W E I H vi The University of British Columbia April 1996 To my beloved wife-to-be, Andrea Wadman viii Chapter 1 Introduction Many techniques have been developed for formal hardware verification. There has been a need for this variety because each method has strengths and weaknesses which restrict it to a particular subclass of verification tasks. The verification method de-scribed in this thesis has capabilities not found in existing techniques. In particular, this method allows automatic verification of asynchronous data-path circuits. Synchronous and asynchronous designs differ primarily in the timing models used to describe their behaviour. In a pure synchronous design, computation is per-formed by combinational logic and storage is performed by clocked latches. In this framework, the state of the latches after a clock event is a deterministic function of the values held in the latches before the clock event. Specialised .verification meth-ods, such as symbolic trajectory evaluation (STE), exploit the fact that synchronous designs have deterministic next state functions which allow a symbolic "next state" operator to be implemented efficiently. This allows large synchronous designs to be formally verified with a high degree of automation [Bea93, Dar94]. Asynchronous designs, on the other hand, do not use a clock to determine the 1 timing of state changing operations. Because the timing relations between circuit components cannot be completely determined, asynchronous designs are usually modelled using non-deterministic next-state relations. Symbolic model checkers have been used to verify small designs; however, the state-space explosion problem prevents fully automated verification on the same scale that has been achieved for synchronous designs. This thesis presents a formal framework in which asynchronous circuits can be verified using synchronous models. The key observation is that for speed-independent circuits without output choice the sequence of operations performed by any component depends only on the original state of the circuit and any input values applied. The exact relative ordering of component actions doesn't matter. This motivates specifying the desired behaviour in terms of input and output se-quences for each component, which is a natural specification for data-path circuits. Because the synchronous implementation of the circuit corresponds to choosing a specific ordering for component actions, verifying the input/output sequences of the components in a synchronous model guarantees that the asynchronous circuit will produce equivalent sequences. 1.1 Formal Verification Techniques In order to set this work in context, a brief overview of the major categories of verification techniques is provided. Much of the information contained in this sec-tion is drawn from [Gup92] and [Seg92]. Most methods can be divided into two categories, theorem proving and model checking. Because of their relevance to this work, two particular methods are included in this discussion: symbolic trajectory evaluation (STE) which is based on an efficient OBDD-based model checker; and 2 the Voss Prover which combines STE with a theorem proving framework. 1.1.1 Theorem Proving The process of verification by theorem proving typically proceeds by describing both the specification and the structure of the hardware in terms of formal logic_and then formally showing a relationship (such as implication or equivalence) between them. Automated theorem provers (such as HOL [MG93]) have been developed to assist the creation of the required proof. In order to grasp the size of this task, it is important to realize that a formal proof consists of a finite sequence of statements, where each statement is either one of the fundamental axioms provided by the theorem prover or can be derived from the previous statements by a primitive rule of inference. The collection of these axioms and inference rules is typically quite small (5 axioms and 8 inference rules for HOL) requiring a very large number of steps in order to prove theorems. For example, a proof showing that the combination of a NAND gate and an inverter is equivalent to an AND gate takes a sequence of 365 statements. Also, while these theorem provers are partially automated, in order to prove theorems of any size, human guidance is required. This interaction may be required approximately once for every 1000 proof steps. Despite the large multiplier, we can see from the number of lines required for even a trivial example that considerable human assistance is required for larger proofs. A further drawback is that providing this assistance requires that users possess a high level of training in formal logic. However, theorem provers are extremely powerful, and there are many exam-ples of their use in verifying both hardware and software systems [OR+95]. Theorem proving has two main advantages which help make it a powerful technique. First, being based on a general mathematical logic (e.g. higher order logic in HOL), theo-3 rem provers can be used in a wide variety of different situations. Second, it is well suited to hierarchical methods. This is extremely important when dealing with large systems and systems (such as hardware) which contain various levels with different levels of detail (for example, verifying an arithmetic unit made up of functional blocks which are made up of gates). 1.1.2 O B D D Based Model Checking Model checking is a technique which has strengths and weaknesses that are almost exactly the reverse of those of theorem proving. Model checking proceeds by de-scribing the system as a finite state machine. That is, for a system with d boolean valued signals it creates the state space 2d and a state transition relation R C 2dx2d. Given an initial state predicate, Qo, and a desired property, p, verification proceeds by exhaustively searching the states reachable from Qo under R for states where p is false. Thus, it provides a verification of the behaviour of the system described by the model provided, as opposed to theorem proving which shows functional or structural equivalence between the specification and implementation, both of which are described in the same language. One advantage of the model checking approach is that a single specification may be used to verify different implementations with the same intended functionality simply by repeating the decision procedure. This can be contrasted with theorem proving where the proof will typically need to be reformulated to match the new implementation. This process typically has a completely automatic decision procedure, allow-ing users with little understanding of the underlying theory to use the system to verify properties. It can also provide counterexamples to failed assertions, which is a significant aid to designers whose fundamental goal is to create a correct system 4 . (rather than simply to determine the correctness of the current design). There are significant drawbacks to model checking. The first is that the specifications are restricted to being simple enumerations of the desired properties, and it can be difficult to determine whether the specification completely captures the desired properties of the system. The second problem is the fact that the complete model must be described before the system may be verified. The state is "described" rather than constructed, because symbolic techniques using OBDDs [Bry86] have been developed which represent the model and its transition relation as functions from sets of states to sets of states which allow the verification of systems with large state spaces (for example [BC+94] with more than 10 1 2 0 states for a synchronous pipelined A L U and IO 5 0 states for an asynchronous stack). However, the state space must still be described in some manner, which limits the size of systems that can be verified. However, model checking is well-suited to verifying control circuitry, which will typically have a complex state relation but relatively few states. 1.1.3 Symbolic Trajectory Evaluation Symbolic trajectory evaluation (STE) is a model checking based technique which traces its roots back to symbolic simulation. The inclusion of OBDDs significantly increased the power of symbolic simulation while retaining the ability to model low-level properties such as bounded delays and charge sharing. To reduce the impact of large internal state, a third logic value X is added to indicate an unknown value for a node. This allows the system state to be placed in a lattice, and efficient algorithms have been developed for verifying large designs in this framework. In this method, the stimulus to the system and the required behaviour must be described in a restricted form of temporal logic. STE is a process for showing that the trace 5 of states simulated implies the trace of states described by the consequent. This is a relatively efficient verification method, allowing the verification of large circuits, such as a 32-bit pipelined RISC processor [Dar94]. Like model check-ing, the specifications are typically behavioural, allowing reuse of specifications for different implementations, and the user does not need to have a complete under-standing of the details of the internal model in order to use the tool effectively. However, to realize efficient symbolic simulation STE depends on the exis-tence of a deterministic next state function. It is also limited by the properties of the underlying OBDDs. For example, there is no variable ordering which allows multiplication of bit vectors to be represented by a diagram of a size which is less than exponential in the number of bits. This is a "hard" limit in the capabilities of STE, since (like model checking) it works directly on the circuits states and does not lend itself to hierarchical methods. Furthermore, the lattice structure which allows efficient verification also restricts the class of formulas which can be checked. 1.1.4 The Voss Prover The Voss Prover combines the powerful low-level capabilities of STE with a simple theorem prover [HS95]. This allows STE results to be combined together to show the correctness of circuits too large for STE to verify on its own. Theorem proving is limited by the extremely small steps which it must take in deriving proofs and STE is limited by the OBDDs which form its underlying representation. The Voss Prover solves these problems by using the verification results provided by trajectory evaluation as components which are manipulated to form proofs. A fully programmable script language is provided for writing proofs. This language includes abstract representations for data (such as integers) which 6 free the proof from the boolean representation provided by trajectory evaluation, and allows human intervention to take place at an extremely high level. As opposed to HOL, where each proof step must either be an axiom or the application of an inference rule, the Voss Prover has specialised rules for composing STE results built in, as well as the ability to include limited domain knowledge. This makes proofs shorter and easier for the operator to understand. An example is the verification of a pipelined IEEE 64-bit floating-point multiplier [AS95]. 1.2 Automatic Verification of Asynchronous Data-Path Circuits The goal of this research was to develop a method for automatically verifying asyn-chronous data-path circuits. With this in mind, let us review some key properties of the above verification techniques. Theorem Proving Despite its strengths, theorem proving is not suitable for our purposes because it is not automatic. There are partially-automated theorem provers, but they still require significant manual effort by users with considerable mathematical sophistication. Model Checking Model checking is automatic, but general model checking on its own it is not sufficient because its complexity can be exponential in the size of the circuit being verified. This causes a state-space explosion for data-path circuits which typically have a large number of state-holding nodes. 7 Symbolic Trajectory Evaluation This specialised form of model checking takes advantage of a deterministic next-state function to allow efficient verification. It is still automatic, but can not handle the non-determinism of an asynchronous circuit. Voss Prover While the Voss Prover is a powerful extension of STE in many respects, it still does not handle non-deterministic next state relations. From the above summary we can see that theorem proving does not provide an automatic decision procedure, that we can not use model checking on its own, because of the large state space required to describe data-path circuits, nor can we simply use trajectory evaluation or the Voss Prover, because the next state relation of an asynchronous circuit is non-deterministic. For this work model checking was used to show speed-independence, which was used to justify transforming the asynchronous circuits into equivalent syn-chronous models. Then STE was used to verify the synchronous models. The theoretical justification for this transformation is presented in chapter 2. Although the implementation described here uses OBDD based model checking and STE, the theoretical framework presented could be applied to other methods as well. 1.3 Related Work This work is motivated by the observation that the current state of a speed-independent circuit depends only on the initial state of the circuit, its in-puts, and how many times each component has performed an action. Muller and Bartky [MB59] used similar ideas when they described circuits whose states could be 8 modelled on a semi-modular lattice. The handling of traces is influenced by Udding's thesis [Udd84], where he classifies systems based on the reordering of traces. While he uses this as a method to describe input and output choice, we use the equivalence of reorderings of traces to simplify verification. Using a synchronous model for an asynchronous circuit can be seen as an extreme example of the reduction of the next state relation described in [Pel93]. The circuit model presented excludes designs with arbiters, and we note that many published examples of asynchronous designs meet this requirement. The Cal-tech Asynchronous Processor [Mar89a] and the self-timed divider of Williams [Wil91] are other examples of self-timed designs that do not use arbiters. A notable excep-tion to this is the Counter Flow Pipeline Processor [SSM94] in which arbiters are used to coordinate the interactions of adjacent pipeline stages. Another well-known published design which is not tractable by this technique is the micropipeline [Sut89], which combines delay-insensitive control circuitry with a bounded-delay data-path. A more general theoretical framework than the one presented in this paper would be required to verify either of these last two designs. This work requires that designs be shown to be speed-independent before they can be verified. Here this step is performed using model checking and the composition of specifications [AL90], but there are several design methodologies which ensure that the circuit produced is speed-independent (or delay-insensitive, which is stronger). The survey [Hau95] provides an overview of design methods for delay-insensitive circuits. Petri net-type methods [Mur89] are used as a basis for many of these methods. One is I-nets [MFR85], which can describe systems which are not delay-insensitive, but where delay-insensitivity can be shown by the Foam 9 Rubber Wrapper constraint [MFR85]. Another method is Signal Transition Graphs [CLW85], where various levels of restriction can be placed on the graphs in return for more efficient automatic synthesis of a circuit. Finally, Change Dia-grams [KK +92] are similar to STGs, but avoid some of the restrictions while still maintaining efficient verification of design properties and circuit synthesis. Martin has implemented a compilation technique [Mar89b] that uses a lan-guage similar to Communicating Sequential Processes and compiles it into speed-independent circuits. Van Berkel [vB92] uses the language Tangram in a simi-lar manner. As opposed to Martin and Van Berkel who create their own speed-independent components as required, Brunvald and Sproull [BS89] use a subset of Occam (a language based on CSP) and provide a delay-insensitive module imple-menting each of the language constructs. Ebergen [Ebe91] uses traces to describe both the specification and the design, and can automatically reduce the specification to a design built up of small number of basic components (such as wire, fork, C-element, etc.). Lastly, Spars0 and Staunstrup [SS93] describe a method for designing multi-ring circuits from building blocks which are speed-independent by construc-tion. A vector multiplier from their paper is verified as the major example in this thesis. A speed-independent circuit produced by any these techniques is amenable to verification using the method presented in this thesis. 1.4 Overview of Thesis Chapter 2 describes the theoretical framework and results which justify the use of synchronous verification tools for asynchronous circuits. Chapter 3 provides a detailed discussion of the specification method used. Chapter 4 describes how the process was enacted for the examples, and Chapter 5 presents a large example circuit 10 which was verified to show the capabilities of this method. Chapter 6 provides conclusions and suggests possible areas for future work. 11 Chapter 2 Theory This chapter introduces the theoretical underpinnings of this work. The key theo-rems are stated in section 2.4 along with sketches of their proofs. Detailed proofs are provided in appendix A. To motivate the theorems, a FIFO is used as a simple ex-ample. The circuit model is introduced in section 2.1, and the necessary definitions are laid out in section 2.2. These are used to give the specification for the FIFO in section 2.3. Finally, section 2.5 provides a brief discussion relating the hypotheses required in the theoretical results to circuit design. 2.1 The Circuit Model We model a circuit as a set of nodes V, a state transition relation i2, a set of circuit components C, a set of environment components E, and an initial state predicate Qo- Each node corresponds to a boolean-valued signal. A state is an assignment of values to nodes; we write S to denote the circuit's state space, where S — 2V. For v in V and s in 5, we write v(s) to denote the value of node v in state s. The components provide a decomposition of V and R described shortly. 12 clt c2t c3t c4t src Figure 2.1: A Self-Timed F IFO Figure 2.1 depicts a simple four-stage F IFO that is used as an example throughout this chapter. The FIFO is one-bit wide and uses a dual-rail cod-ing [Sei79], where the signal carries its own completion information. In this case, a single bit x is encoded by a pair of wires (x.t,x.f), with (T, F ) representing true, (F, T) representing false, and (F, F ) as an extra value empty which is used to sep-arate data values. Thus, the transition from (F, F ) to (T, F ) encodes the arrival of a true value. The acknowledgement part of the handshake cycle takes place on the request line r. This is raised when a stage has passed an empty value, and lowered after it has passed a data value. This circuit has fifteen nodes, twelve circuit components, and two environ-ment components. We assume that it is initialised to the all-empty state. V = {x[t].t,xC:].f,xCt'].r|t€ {0 . . .4}} C = {Clt,clf,nl,c2t,c2f,n2,c3t,c3f,n3,c4t,c4f,n4} E = {src, snk} Q0 = f\ -oc [z] . t A -ix [i] . f A x [i] . r i=0,...4 Each component c in C U £ has a set of inputs Ic and a set of outputs Oc, where Ic and Oc are subsets of V. Furthermore, we assume that each node is connected to exactly one output. In other words, the outputs.of the components in 13 CUE partition V. The behaviour of component c is given by the state transition relation Rc. To simplify the presentation, we exclude vacuous transitions: i.e. if (s, s') is a state transition in Rc, then s ^  s'. Only outputs of c change in a transition in Rc, V(s, s') € Rc. Vu eV.{v£ Oc) V (v(s) = v{s')) (2.2) Furthermore, the behaviour of a component depends only on the value of its inputs and outputs. If s1 and s2 are two states and c is a component such that all inputs and outputs of c have the same value in both s1 and s2, then if c can perform an action in s1 it can perform an equivalent action from s2. More formally, Vs\s2,s3eS. ((Vu £ ICU Oc. v(s1) = u(s2)) A (s1, s3) 6 Rc) => 3s4 e S. ((s2, s4) e R c A (Vu € Oc. v{s3) = v(s4))) A component is enabled in state s if there is another state s' such that (s, s') is in Rc-enabled(c, s) = 3s'. (s, s') € Rc (2-4) It follows from equation 2.3 that if there are two states, such that c is enabled in one but not the other, then these states must differ in the value of some input or output of c. Vs, s' € 5. ((enabled(c, s) A ->enabled(c, s')) (3v G Ic U Oc. u(s) ^  u(s'))) Continuing the FIFO example, the input set, Iclt of C-element clt from figure 2.1 is {x[0] . t , x [ l ] .r} and the output set, Ocit is {x[l] .t}. State transition 14 relations for components clt, src, and snk, are given below, Rat = {{s\s2) € 5 x 5 | (x[l] .rfs1) = x[0] Ms1)) A (x[l] .ti*1) # x[0] .t^1)) A (x[ l ] . t(s 2) = x [0 ] . t (s 1 ) ) A Vu 6 {V - {x[l] . t } ) .u (s 2 ) = u ^ 1 ) } fl,rc = {(sSfi2) € 5 X 5 | (x[0] .t^ 1) Vx[0] .fis1))) # (x[0] .r^ 1) A (x[0] . t ( 5 2 ) VxtO] .f (s 2 ))) = (x[0] . ^ s 1 ) (2.5) A ->(x[0] . t (s 2 ) Ax[0] . f (s 2 ) ) A Vu G (V - {x[0] .t,x[0] . f } ) .u (s 2 ) = vis1) } Rsnk = {(s\s2)eSxS \ (x[4] .r^ 1) = (x[4] . t (s ] )Vx[4] .f (s1))) A (x[4] . r (s 2 ) ^ (x[4] .tfc1) Vx[4] - f^ 1 ) ) ) A Vu 6 ( V - { x [ 4 ] . r } ) .u (s 2 ) = u(s J ) } where S = 2 V with V from equation 2.1. Given a set of nodes V, a set of circuit components C , and a set of environ-ment components E, we define the state transition relation for the circuit and its environment as the union of the state transition relations for each component. Let R denote this state transition relation. R = U Rc (2.6) cecuE If more than one component is enabled in state s, then s can have several possible 15 successors. This non-determinism corresponds to unspecified delays for the compo-nents. Furthermore, each successor corresponds to the action of a single component. This gives an "interleaved semantics" for the circuit. Section 2.4 shows that allowing simultaneous actions of different components does not affect the properties which can be specified in local formulas. To verify properties of a circuit, we consider assertions about reachable states. The set of reachable states is given by the circuit's initial state predicate Qo and its state transition relation R. A trace is a sequence of states such that the first state in the sequence satisfies QQ and each pair of successive states in the sequence is in R. We will write traces(R, Qo) to denote the set of all traces which can be formed using the transition relation R and whose initial state satisfies the predicate QQ. If t is a trace, we write t° to denote the initial (first) state of t, and tk to denote the k + Ist element of the sequence. A trace is either infinite or ends in a terminal state, where s € 5 is terminal if there is no state s' such that (s, s') 6 R. A state s is reachable if there is a trace t such that s appears in t. The predicate reachable(R,QQ,s) denotes that s is reachable by a circuit and environment with combined state transition relation R, starting from a state satisfying Qo. 2.2 Definitions This thesis considers speed-independent circuits whose circuit components have no output choice and whose environment components have stable inputs. A circuit is speed-independent if once a component is enabled to change its output(s), it remains enabled to perform that change until it performs some action. A component has output choice if it can be enabled to perform one of two or more mutually exclusive actions. A component has stable inputs if once it is enabled, the values 16 of its input nodes remain unchanged until it performs an action. Discussion is restricted to circuits that are speed-independent, with circuit components that do not have output choice, and where the environment components have stable inputs. A circuit which has these properties will be called an eligible circuit. Definition 1 (Speed-Independence) Given a circuit (V, R, C, E,Qo), the circuit and its environment are speed-independent iff Vc G C U E. V(s*, s2) G Rc. Vs 3 G 5. ((s\ s 3) G R - Rc) A reachable(R, Q0, s1) => (3s4 G S. ((s3, s 4) G Rc) A (Vu G Oc. (v(s2) = v(s4)))) Definition 2 (Output Choice) Given a circuit (V, R, C, E, Qo) and a component c G C U E, c has output choice iff 3(s, s 1 ) , (s, s2) G .Rc - reachable(R, Qo, s) A (s 1 ^ s 2) Definition 3 (Stable Inputs) Given a circuit (V, R, C, E, Qo) and a component c G C U E, c has stable inputs iff V(s, s') G R. (reachable(R, Qo, s) A enabled(c, s)) ((s,s')eRc)y(\/veic.v(s) = v(s')) Note that if (s, s') ^ Rc then c's outputs cannot change either, by the definition of outputs given in equation 2.2. Definition 4 (Eligible Circuits) A circuit (V, R,C, E,Qo) is eligible iff it is speed-independent, no component in C has output choice, and every component in E has stable inputs. Section 4.3 describes how the FIFO from figure 2.1 can be shown to be speed-independent and that all of its components have stable inputs. Only the src 17 component has output choice: from a state where x[0] . t and x[0] . f are false and x[0] . r is true, the source may set either x[0] . t or x[0] . f to true, but not both (see equation 2.5). The F IFO is an example of an eligible circuit. The next five definitions describe technical properties of traces that are needed for the proofs in section 2.4 and appendix A . A trace is weakly fair if every persistently enabled component eventually performs an action. The occur and index functions give the number and locations of occurrences of actions by a particular component in a trace. Two traces are choice consistent if each envi-ronment component outputs the same sequence of values given the same sequence of inputs. Splicing is an operation that combines two traces while preserving prop-erties of local formulas and weak-fairness. Definit ion 5 (Weakly Fair Trace) Given a circuit (V, R, C, E, Qo), a trace t is weakly fair iff Vc G C U E. Vi G N. enabled(c, t{) => 3/ € N. {j > i) A {{tj, tj+1) G Rc) V -ienabled(c, tj) Note that for a weakly fair trace of a speed-independent circuit, any enabled com-ponent eventually performs an action. Definition 6 (Occurrence of a Transition) Given a component c, a trace t, and a natural number k, occur(c,t,m) denotes the number of times that c occurs in t°,..., tm, formally defined as follows. occur(c, t, 0) = 0 occur(c, t, m) = occur(c, t, m - 1) if m > 0 and Vu G Oc- u(i*m - 1) = v(tm) occur(c,t,m) = occur(c,t,m - 1) + 1 if m > 0 and 3v G O c . (u(< m _ 1 ) ^ v(tm) 18 Definition 7 (Index of a Transition) Given a component c, a trace t, and a nat-ural number k, index(c,t,k) denotes the location of the kth transition of component c in trace t. That is, index(c, t, k) = min{m € N | occur(c, t, m) — k} Let i be a trace of a circuit that includes a component c. We write t\ to denote the state immediately before the first time component c effects a state transition in t and t\.post to denote the state immediately after this transition. More generally, tkc = £«'»<Mct>)-i a n d tk.post = tindex^k\ Since the components' output sets partition V, there can be no change on any v G Oc from index(c,t,k) to index(c, t, k + 1) — 1. This means that assertions about tk.post can be expressed using tk+1. As a result, assertions about a node's inputs at the time of its kth action are written about the state tk while assertions about the outputs of the kth action are commonly written about the state tk+1. The notation vk(t) denotes v(tk), and valid(vk,t) indicates that component c is enabled at least k times in t. Definition 8 (Choice Consistent Traces) Given an eligible circuit (V,R,C,E,Qo), let c be a component in E and let t and u be traces. The actions of c are choice consistent in t and u (written t=cu) if, given the same 19 history of inputs, c produces the same outputs in both traces. More formally, t^cu = ((r° = u°) A Vfc G N. PreEquiv(c, t, u, k)) PostEquiv{c, t, u, k) where PreEquiv(c, t, u, k) = Vu G h U Oc. Vj G { 1 . . . k}. valid(vJc,t) = valid(vi,u) A valid(vi,t) => (v(ti) = v(uc)) PostEquiv(c, t, u, k) = Vu G Oc. Vj G { 1 . . . k). (valid(v3c,t) (v{t3c.post) — v(uJc.post))) If is a set of components, t=ou denotes Vd G D.t<=,iu. Consistency is an equivalence relation. If t is a trace, each pair of successive states in t can be associated with the component that effected the transition. Given two choice consistent traces t and u, splice(t, u, m) produces a sequence where the first m transitions are effected as in t, the corresponding transitions are deleted from u, and the remainder of u is appended to the prefix from t. Theorem 1 will show that splice(t, u, m) is a trace. Figure 2.2 shows two traces and their first six splices (where c1 denotes the ith action by component c). Definition 9 (Splicing Traces) Given an eligible circuit (V, R, C, E,QQ), let t and u be traces with t° = u° and t=£U. Let m be a natural number such that tm exists. The mth splice oft and u is defined inductively. Let cm be the component which makes its nth action going from the state t™'1 to the state tm, and let im be the index of the point where cm makes its nth action in splice(t, u, m — 1), if cm ever 20 u c 1 a 1 d 1 c 2 d2 61 c3 a 2 b2 d3 a3 c4 .. splice(t, u, 0) I ' 1 a1 tf1 c 2 d2 61 c3 a 2 b2 d3 a3 c4 .. splice(t, u, 1) a 1 c1 d1 c 2 d2 b1 c 3 a2 b2 d3 a3 c4 .. splice(t, u, 2) a 1 61 c1 d 1 c2 d2 c 3 a 2 b2 d3 a3 c4 .. splice(t, u, 3) a 1 61 c 1 c/1 c 2 d2 c 3 a 2 b2 d3 a3 c4 .. splice(t, u, 4) a 1 b1 c1 d1 c 2 d2 c 3 a 2 b2 d3 a3 c4 .. splice(t, u, 5) a 1 61 c1 d1 a 2 c2 d 2 c 3 b2 d3 a3 c4 .. t: a 1 b1 c1 d1 a 2 b2 c2 d2 a3 b3 c3 d3 Figure 2.2: Splicing Traces makes such an action. Formally, ( t m - \ t m ) e R C m n = occur(cm, splice(t, u, m — 1), m — 1) + 1 im = index(cm, splice(t, u, m — 1), n)if it exists If im exists, then splice(t,u,m) is the sequence that satisfies the following equations splice(t, u, 0) = u v(splice{t,u,m)k) = v(tk) if k < m and v G V v(splice(t, u, m)k) = v(tm) if m < k < im, and v € 0Cm v(splice(t, u, m)k) = v(splice(t, u,m- if m < k < im, and v £ 0Cm v(splice(t,u,m)k) = v(splice(t,u,m - l)k) if im < k if im does not exist then splice(t, u, m) is not defined. The following property gives a sufficient condition for splice(t, u, m) to be defined, and it is shown in theorem 1 of section 2.4 that splices are traces. Property 1 (Splicing) Given an eligible circuit (V, R,C, E,Qo), let t and u be traces with t° = u°, t=£U. If t is weakly fair, then splice(t, u, m) exists. 21 The combination of weak fairness and speed-independence ensures that im exists. The next four definitions describe the properties of traces that are used for specification and verification. Local formulas refer to the values of the inputs and outputs of a component when the component performs its kth action, specifying properties of bounded prefixes of traces. Two traces are equivalent if they have the same truth values for all local formulas. Global formulas are predicates over states. Periodic global formulas and shifted local formulas are used to specify safety properties of unbounded traces. Definition 10 (Local Formula) A local formula is either vk where v £ ICU Oc, k G N, and c is a component with stable inputs or ->f where f is a local formula or f A g where f and g are local formulas. A local formula L is valid for trace t if valid(vk, t) is true for each term of the form ^ in I . If L is valid for trace t, then it holds if the values of the nodes of the circuit in trace t satisfy the formula. The predicates valid(L,t) and L(t) denote that L is valid for trace t and that L holds for trace t respectively, and the notation comp(L) indicates the set of components which appear in the local formula. Finally, (R, Qo) \= L denotes that L is valid and holds for every weakly fair trace of the circuit with state transition relation R and initial state predicate Qo. Definition 11 (Equivalent Traces) Two traces t and u with t° — u° are equiva-lent iff for all local formulas L {valid{L,t) = valid(L,u)) f\{valid(L,t) (L{t) = L(u))) 22 The notation t = u denotes that the traces t and u are equivalent. Because envi-ronment components of an eligible circuit have stable inputs, t = u t=E u. Definition 12 (Global Formula) A global formula is a predicate over states. Definition 13 (Shifted local formula) Let L be a local formula and comp(L) be the set of components that appear in terms of L. Let i be a natural number and p be a function from comp(L) to the naturals. The shift of L by i times p is obtained by replacing every term of the form vk in L with v'c*p^*k. The notation shift(L,p,i) denotes the shift of L by i times p. Definition 14 (Periodic Global Formula) Let ( V , R, C, E, QQ) be an eligible cir-cuit. Let G be a global formula, let C ' C C U E be a set of components, and let p be a function from C ' to the natural numbers, with p(c) > 0 for all c G C ' . G has period p if only components in C ' are enabled in states that satisfy G, and for every trace whose initial state satisfies G there is a choice consistent trace that returns to a state satisfying G after each component c in C ' has performed p(c) actions. More formally, G is periodic with period p iff Vs € S. Vc € (C U E) - C'. G(s) => -,enabled{c, s) A V i e traces(R,G).3u€ traces(R,G).3m G N. (t^E u) A G{um) A (Vc G C ' . occur{c, u, m) = p(c)) The predicate periodic(G, C", p) indicates that the global formula G is periodic with period p on the components in the set C ' . 2.3 A Specification for the FIFO Local formulas provide a natural way to specify the input/output behaviour of speed-independent circuits. For example, a natural specification for the FIFO shown in 23 figure 2.1 is that the infinite sequence of values output by the source must be the same as the sequence received by the sink. This is expressed by the formula Vi € N. ((x[0] .t)\n.po8t=xl4] .t\nk) A « x [ 0 ] .tVIK.post = x[4] . f « n t ) which is equivalent to (dropping the post notation) Vi € N. (x [0] . t^ 1 = x [4] . t«jnfc) A (x [0] . f [tc1 = x C4] . f L ) (2.7) Recall from the discussion after definition 7 that x[0] .t '^ 1 refers the value of x[0] -t immediately before the src component performs its i + I s ' operation. This is the value that was output by the source at its ith operation. On the other hand, x[4] .t\nk is the value that was input to the snk component at its ith operation. Local formulas can only specify properties with a finite number of terms. Periodic global formulas extend the result to infinite sequences. For the FIFO example, it is convenient to assume that the FIFO is initially reset to a state where all stages hold empty values (as in equation 2.1), and consider a period function that returns the FIFO to this state. Because the source alternates between sending empty and full values, the source must perform two operations per period, as must the sink. This motivates the following choices of G and p. p(src) = 2 p(snk) = 2 (2.8) G = Qo where Qo is given in equation 2.1. Note that this specification does not say that the FIFO periodically returns to an empty state for all traces. It merely requires that there exists at least one trace for which the FIFO has this behaviour. Let L be the 24 local formula defined below. L = (x[0] . t 2 r c = x[4] .t\nk) A (x[0] .f]rc = x[4] .f\nk) A (x [0] . t 3 r c = x [4] . t2snk) A (x [0] . f L = x C4] . f ]n k) (2.9) Intuitively, the first line states that the data is propagated correctly, and the second states that the empty is propagated correctly. Theorem 3 in the next section shows that establishing that (R,G) (= L and that G has period P is sufficient to establish Vi € N.(R,G) \= shift(L,p,i), which for G, L, and p as defined above is equivalent to the specification given in formula 2.7. Since the formula L asserts that the first value output by the circuit is equal to the first value supplied, showing shift(L,p, i) shows that for any i, the ith value output by the circuit is equal to the ith value supplied, which verifies correct FIFO behaviour. 2.4 Properties of Speed-Independent Circuits The splice operation has two properties that provide the foundation for this work. First, the splice of two weakly fair traces is a weakly fair trace. Second, splicing preserves the values of local formulas. These properties motivate the following theorem. Theorem 1 (Splicing) Given an eligible circuit (V, R,C,E,Qo), let t and u be weakly fair traces with m a natural number such that tm exists. If t° — u° and t=E u, then splice(t, u, m) is a weakly fair trace and splice(t, u, rn) = u. Proof (sketch, see appendix A for details): The key observation is that the actions of concurrently enabled components commute without changing the values of local formulas or affecting the property of weak fairness. Let a be a trace, i be a natural 25 number, and c and d be components such that (a ' ,a , + 1 ) G Rc, ( a , + 1 , a , + 2 ) G Rd, and d is enabled in state a\ Let /3 be the sequence such that 3k = ak if jfe # * + 1 u(/? , + 1) = v{ai+2) iiveOd v{3i+1) = v{a{) \iv$Od Note that any component that has output choice must be an environment com-ponent and therefore has stable inputs. This and speed-independence ensure that {3',3i+1) G Rd and ( 3 i + 1 , 3 i + 2 ) G Rc- Thus, 3 is a trace. Given an arbitrary com-ponent e with stable inputs, it is shown below that vk has the same validity and value in traces a and 8 by case analysis on index(e, a, k), and that if a is weakly fair then 3 is weakly fair as well. The theorem is proven by induction on m. The base case is m = 0, which is discharged by noting that splice(t, u, 0) = u. For m > 0, note that the component that effects the transition from tm~l to tm must be enabled in state splice(t, u, m — l ) m _ 1 . By the induction hypothesis, splice(t,u,m — 1) is weakly fair and t=Esplice(t,u,m— 1); thus, this component must eventually perform an action, and any environment choices must be identical in both traces. Therefore, the sequence splice(t, u, m) can be obtained from trace splice(t, u, m — 1) by a finite number of commuting operations, and the claims of the theorem follow from the properties of commuting. • The key property of speed-independent circuits that we exploit is that if two traces for a circuit start in the same state and the environment provides the same inputs, then all components with stable inputs have identical input and output sequences in both traces. This equivalence is formalised by observing that both 26 traces satisfy the same local formulas. Theorem 2 (Equivalence of Traces) Given an eligible circuit (V, R, C, E, Qo), if t and u are weakly fair traces with t° = u° and t=£U, then t = u. Proof: Because every local formula L can be represented by terms of the form vk and the operators - i and A, if every term of the form vk has the same validity and value in t and u then, by induction on the structure of L, the theorem holds. Let vk be a term of L, where c is a component with stable inputs. If vk is valid in trace t, let a = splice(t,u,index(c,t,k)). By the definition of splicing, vk is valid in both t and a, and vk(t) = vk(a). By theorem 1, vk(a) = vk(u). This establishes vk(t) = vk(u) as required. A symmetric argument applies if vk is valid in u. Finally, the case where vk is not valid in either i or u also satisfies the claim of the theorem. • Theorem 2 provides the basis for verifying specifications of the form (R, Qo) \= L. If the circuit satisfies the hypotheses of theorem 2, it is only nec-essary to verify a single trace for each initial state and sequence of inputs from the environment to show that all possible traces starting from an allowable initial state and with suitable environment behaviour will satisfy L. Chapter 4 describes how this can be shown using STE. However, a local formula only specifies properties of a bounded number of actions of each component. Infinite traces can be verified by using periodic global formulas and shifted local formulas (as defined in section 2.2). Theorem 3 (Recurring Local Formulas) Given an eligible circuit (V, R, C, E, QQ), let G be a global formula and L be a local formula such that Qo G and (R,G) \= L. Letp be a mapping from comp(L) to the natural numbers. 27 Then, periodic(G, comp(L), p) Vt > 0. {R,G) \= shift(L,p,i) Proof: Let i be a trace of (R,Qo)- The proof proceeds by induction on i, with induction hypothesis (R,G) \= shift(L,p,i) A V ( € traces(R,G).3u£ traces(R,G).3m£ N. ( u^t (2.10) A Vc G comp(L). occur[c, u, m) = (i + 1) * p{c) A Vc € {CU E) - comp(L). ^enabled{c, um) A G(um)) The base case is i = 0. From shift(L,p,0) = L and (R,G) ^ L we see that (R, G) (= shift(L, p, 0). The second half of the conjunction follows from the definition of periodic global formulas. The induction step relies on properties of the subtrace u' = u m , u m + 1 , . . . where m is provided by the induction hypothesis for i — 1. Since u' is in traces(R, G) we can see that L holds for u', and since occur{c, u, m) = i*p(c), this is equivalent to (R, G) |= shift(L,p, i). The second half of the conjunction follows from the definition of periodic global formulas as applied to u'. This completes the proof. • When using symbolic trajectory evaluation for verification, it is convenient to perform the actions of all enabled components as a single state transition. The next theorem shows that the validity and value of local formulas is preserved under 28 such an execution model. Let R be a state transition relation, and let R+ = {{s\s2)eSxS\ V c G C u £ 3s'eS.{{s1,s')eRc)A(VveOc.v(s2) = v(s')) (2.11) V -nenabled(c, s1) A (Vu e Oc. v(s2) - vis1)) } Transition (s x,s 2) is in R+ iff s2 is the state reached by performing an action of each component that is enabled in state s 1 in a single state transition. Note that the definition of occur does not require that components act one at a time. Theorem 4 (Combined Actions) Given an eligible circuit (V, R,C, E,Qo), for all local formulas L, (R,Q0)\=L <=> (R+,Q0)\=L Proof (sketch, see appendix A for details): Let u be a trace of (V, R+, C, E, Qo)-We construct a trace t of (V, R, C, E, Qo) such that t = u. The key idea is that if u includes a transition (t',t'+1) where n components perform actions, then we can effect the same change in t with n separate transitions. Because the original circuit is speed-independent, each component that was enabled in state u' is enabled when its turn arrives. Furthermore, because any component that occurs in a term of L must have stable input, all input nodes of the component have the same value when the component performs its action in t as in u. This guarantees that L has the same value and validity in t as in u. To see the converse, consider a weakly-fair trace t in (V, R, C, E,QQ). The proof proceeds by creating two traces, u in traces(R+, Qo) and a in traces(R,Qo), such that a and u have the same relationship as the one described in the preceding 29 paragraph for t and u, and t = a. The traces are formed by considering the set D of components which are enabled in t°. The trace u is formed by the simultaneous action of all components in D1, while a is the trace formed by having them all as the first ID1] actions in a. The process continues with the set D2 of components enabled in u1. • 2.5 Discussion of Hypotheses While the requirements of the theorems in section 2.4 may seem technical and re-strictive, many of them have natural intuitions and are satisfied by common design methods. One of the basic requirements is that the circuit to be verified be el-igible. This means that the circuit must be speed-independent, that none of its components have output choice, and that all of its environment components have stable inputs. Speed-independence has been chosen as a requirement because it is a readily testable guarantee of freedom from timing hazards. One key point for the next two properties is that for the proof of theorem 1 to work every component must either have stable inputs or no output choice. The formalism also only permits the verification of local formulas which describe the inputs and outputs of components with stable inputs. This makes the choice to restrict components with output choice to the environment reasonable, as it allows us to represent arbitrary data values as inputs to the circuit and guarantees that we will be able to make assertions about any node which connects the circuit to its environment. On the other hand, it does prevent us from handling circuits which contain arbiters. Now consider theorem 2. In many ways it provides the foundation of this work. Its main requirement is that the two traces t and u be choice equivalent. 30 Although the definition of of choice equivalent traces is somewhat complicated, the meaning is simply that the environment provides the same stimulus to the circuit in both traces. Theorem 3 requires that the global formula G be periodic, which means that we could choose an order for components to act such that we arrive back at G. Thus, the theorem's conclusion is that we can build arbitrarily long representative traces by returning repeatedly to states which satisfy G. Finally, theorem 4 requires that we have a transition relation R+ which contains transitions formed by simultaneously performing all enabled transitions in R. 31 Chapter 3 Local and Global Formulas The combined use of global and local formulas is essential to the power of this verification method. They have different expressive abilities, and understanding their function and use is required before applying this theory to practical problems. In this chapter, the two different asynchronous implementations of a 4-bit adder as shown in figure 3.1 are used to illustrate a discussion of the two types of formulas. The local formulas describing correct function are discussed in section 3.1 and the global formulas and period functions describing the adders' periodic behaviour are discussed in section 3.2. Finally, section 3.3 describes a form of behaviour which cannot be verified using this technique. Both designs use the same dual-rail codes as the FIFO described in section 2.1 and are speed-independent. The design on the left calculates the carry for each input pair and carry-in only after all three inputs are valid. This satisfies the stable inputs condition. In order to create a pipeline and allow a possible throughput of one operand per component delay, the adding components are embedded along the diagonal in a block of buffers (FIFO cells). In the second (flat) adder, the carry unit 32 Cin Cin Buffered Adder Fast Adder Figure 3.1: 4 Bit Adders can produce a result as it receives two inputs of the same value, creating a data-dependent throughput. This is still speed-independent, even though the carry unit does not have stable inputs. This realizes a logarithmic average-case latency [Sei79]. Both adders are verified using the same environment, shown in figure 3.2. 3.1 Local Formulas Local formulas are a form of modal logic specifically designed to describe invariant properties of speed-independent asynchronous circuits. Given the same initial state and inputs from the environment, a speed-independent circuit will produce the same sequence of values on the nodes attached to components with stable inputs. How-ever, because the circuit is asynchronous, it is not possible to know the timing of these values. Local formulas are assertions about properties which are independent of the relative timing of components. If a local formula only refers to the inputs and outputs of a circuit, then it is also independent of the internal circuit structure. This allows the same specification to be used with two different implementations, such as the two adders described above. 33 jnkS4 Figure 3.2: Adder Environment Recall from definition 10 that local formulas are boolean expressions formed from terms of the form vk, where v is an input or output node of a component c with stable inputs. The index k denotes that we are describing the state of the node v at the kth action of c. Since environment nodes are required to have the property of stable inputs, and they are the place where the actions of the system are apparent to the outside world, they are natural candidates for acting as the components c in local formulas. Also recall that vk, refers to the value of node v at the instant before the ktb action by c. Accordingly, the output on node v for c's first action is expressed as v2c. Finally, local formulas are typically used to describe a single step of a system's function, which in this case is a single set of operands. With this in hand, we can describe the desired functionality of the 4-bit adder. For the sake of conciseness, [A3 2 r c a 5 , A 2 2 r c a 2 , A l 2 r c a ; , A0 2 r c a 0 ] is used to repre-34 sent the bit vector supplied by the source components for the a operand with their first action, and binary addition is used as shorthand for the logical notation using A and ->. [S4«nfcs^ , S3 j n f c j 5 , S2\nks2, Sl\nksl, S0* n j b o] = [0, A32rca3,k22srca2, kl2srcal, A02srca0] + [0, B32srcbs, B22srcb2, Bl2srcbl, B023rcbg] + [0,0,0,0,Cin 2 r c c i n] (3 .1) Since it refers only to nodes through their association with environment com-ponents, this specification does not reflect the internal structure of the adder. This allows the same specification to be used for any implementation of the adder. 3.2 Global Formulas and Period Functions Global formulas serve as an "invariant", to which the system will return after one of the cycles described by the period function p. These formulas are not genuine invariants, however, for a number of reasons. First, they are not expected to hold throughout the device's computation. Second, the asynchronous implementation is not required to return to a state where this formula holds. However we can think of the system as returning to the state G because if there is one trace for which the global formula recurs with period p, then by the equivalence of traces, conclusions drawn for this trace can be applied to all traces with the same inputs from the environment. Before further discussion of the conceptual basis and use of global formu-las and periodic functions, let us recall their definitions. A global formula G is a predicate over the instantaneous state of the system, and the period function p is a function from a set C' C C to the counting numbers such that only components in 3 5 C are enabled in a state satisfying G and for every trace whose initial state satisfies G there is a choice consistent trace that returns to a state satisfying G after each component c in C' has performed p(c) actions. Also recall that the set C' of compo-nents whose behaviour is described by p must contain all of (and typically only) the components which appear in the local formulas. Thus, the period function p, like the local formula, should not change with different implementations of the device. Most devices can be thought of as having clear cycles of operation. For the FIFO this is the insertion and removal of a single piece of data; for the adder it is the production of one sum from two operands. If we consider an environment which supplies one set of data and then waits until the outputs have been produced, we can see that the system returns to a particular state. This is the state which the global formulas describe. Note that this state may never reappear after the initial situation because the real environment may supply data before the outputs have been extracted. However, we know that we could have waited for the outputs to appear, which means that each set of data can be considered as if it were the first. As established by theorem 2, having a representative trace which exhibits correct behaviour ensures that all traces behave correctly. We consider the trace which returns to the state described by the global formula after each computation, and it serves as our representative trace. There is a high level of interdependence between different nodes in asyn-chronous circuits, due to the handshaking protocols. As a result, any unspecified values in the initial state will quickly propagate through the entire system. Thus, the global formulas typically describe the state of every node, and are dependent on the implementation details. If we consider the two adders, both of their global formulas describe them in an empty state. However, since the pipelined adder sys-36 Figure 3.3: Pipelined Asynchronous Adder 37 tern contains more components, its global formula will specify that they are empty, in addition to the components which it shares with the flat adder. In this case the global formulas are similar, but in general there is no requirement that they match on anything other than specifying the initial state of the nodes connected to the environment. Figure 3.3 shows the internal structure of the pipelined adder. The flat adder has the same structure with all of the FIFO elements removed. For simplicity's sake, consider a generic predicate empty which takes lists of components as its argument and is true if any components with a data output have their output set to the dual rail code for empty, any components with acknowledge lines have this signal set to show an empty state, and any internal state is set in a manner which does not enable any transitions. The global formulas for the two adders can then be expressed by figures 3.4 and 3.5 below. empty [ s r c c i , srcaO, srcbO, s r c a l , s r c b l , srca2, srcb2, srca3, srcb3, f i f o O l a , f i f o O l b , f i f o 0 2 a , fifo02b, f i f o 0 3 a , fifo03b, f i f o l O s , f i f o l 2 a , f i f o i 2 b , f i f o l 3 a , f i f o l 3 b , f i f o 2 0 s , f i f o 2 1 s , f i f o 2 3 a , fifo23b, f i f o 3 0 s , f i f o 3 1 s , f i f o 3 2 s , majO, majl, maj2, majl3, vjoinvO, v j o i n v l , vjoinv2, vjoinv3, xorO, x o r l , xor2, xorl3, snkO, snkl, snk2, snk3, snk4] Figure 3.4: Global Formula for Pipelined Adder empty [ s r c c i , srcaO, srcbO, s r c a l , s r c b l , srca2, srcb2, srca3, srcb3, majO, majl, maj2, majl3, vjoinvO, v j o i n v l , vjoinv2, vjoinv3, xorO, x o r l , xor2, xorl3, snkO, snkl, snk2, snk3, snk4] Figure 3.5: Global Formula for Flat Adder The period function provides a connection between the global formula and 38 the local formula. Although it refers to the actions required to return to the global formula, which is implementation dependent, like the local formula it is implemen-tation independent. Since it only needs to describe the periods of components described in the local formula, typically it will describe the number of actions of the environment components at the inputs and outputs of the circuit. This can be seen from the adder examples. The cycle of operation for the adders is receiving two bit arrays of values followed by empty values to separate them from any subsequent data, and producing another array representing the sum (also followed by empty values. Thus, for both adders the period function is 2 for all of the input and output components. 3.3 U n s p e c i f i a b l e B e h a v i o u r This method allows us to specify and verify behaviours which can be described by formulas whose terms are the values of nodes immediately before the kth action of components. We can neither describe nor verify properties which correspond to the relative timing of the actions of distinct components. For example, structural properties of a circuit may maintain invariants (such as the fact that the n + 1st input to a n stage FIFO may not be accepted until there has been at least one output action) which can neither be described nor verified by this method. However, the goal was to verify data-path circuits. For such circuits, assertions about the sequences of values are a natural method for specifying behaviour. 39 Chapter 4 Implementation This section describes how the results from chapter 2 can be applied using existing verification tools to verify self-timed designs. The overall scheme for the verification is: • The structure and behaviour of the circuit and its environment are described using VHDL. • The specification is written as an initial state predicate, a local formula, a global formula, and a period function. These formulas are verified for the circuit using symbolic trajectory evaluation. • Speed-independence and stable-input assumptions are verified by model check-ing small clusters of components separately. 4.1 V H D L Circuit Descriptions "Behavioural" VHDL is used to describe the functionality of the components of the circuit and the environment, and "structural" VHDL is used to describe the 4 0 interconnection of these components. The VHDL model provides R+ as described in section 2.4. Augmenting the models for environment components facilitates verification. In particular, added registers provide data corresponding to the environment's out-put choice and record the outputs of the circuit. This matches the specifications which describe the input/output behaviour of the circuit. Since trajectory evaluation only allows assertions about data values at particular times, we add a counter which increments each time a data value is received and use it to direct data values into an array. This bridges the gap between asynchronous behaviour and synchronous specifications. Thus the occurrence number of an action will correspond to its po-sition in the array of recorded values. Counters can also be added to record the number of actions taken by the components, for the purposes of establishing that the period function p is correct and to disable the environment components after the period has completed. Since only components which are in the domain C of p may be enabled in states satisfying the global formula G, a correctly functioning circuit will eventually halt in a state satisfying G if all of the components in C are disabled after the number of actions permitted by p. These registers and counters are auxiliary circuitry in the environment com-ponents. In order to fully verify the circuit, this auxiliary circuitry must not inap-propriately restrain the environment components. It is important that the choice variables stored in the source components' arrays do not reduce the output choice of these components. However, these variables are symbolic and simply serve as reference names for the values for the purposes of verifying a general formula with only one simulation run. It is also important that the restriction of the components to a fixed number of actions by the counters does not prevent them from correctly 41 representing general source components. If we were not taking advantage of the periodic behaviour of the circuit, we would require an infinite number of registers initialised to arbitrary boolean variables in order to emulate the output choice of the environment. However, because we know that verifying a finite number of steps is sufficient to show general correctness, only a small number of registers and boolean variables are required. Three examples of V H D L code excerpts are provided: figure 4.1 shows code for a source which supplies a a data value and then stops; figure 4.2 is a sink unit which records the last data value to arrive; and figure 4.3 shows the code for a single F IFO cell. This code is for an F IFO which passes data values in inverted form. Note that some of the internal variables (such as index, and done) must be set by the S T E antecedent. 4.2 Symbolic Trajectory Evaluation Symbolic trajectory evaluation (STE) is a verification technique for circuits with deterministic next state functions which verifies specifications written in a restricted logic called "trajectory formulas". Although restrictive, trajectory formulas readily express requirements of the form "the value of a node n at time t is the function / of the values of the nodes [ n i , . . . , rik] at times [t\,.. Using choice variables to control the output choice of the source components and counter indexed arrays to store inputs to the sink components allows us to represent local formulas using this structure. The specification that a global formula G has period p can also be expressed in this form. After augmenting the models for the environment components with "period counters" as described in section 4.1, we verify that all trajectories that 42 ENTITY s o u r c e I S PORT ( s r ou tT o u t F d a t a ) ; END s o u r c e IN B I T ; OUT B I T ; OUT B I T ; IN B IT r e q u e s t s i g n a l f r o m f i r s t F IFO c e l l d u a l r a i l TRUE d u a l r a i l FALSE a u x i l i a r y v a l u e t o f i x o u t p u t c h o i c e ARCHITECTURE d a t a . f l o w OF s o u r c e IS SIGNAL cTou t : REG_BIT REGISTER; SIGNAL c F o u t : REG_BIT REGISTER; SIGNAL d i n d e x : REG_BIT REGISTER; — One d a t a p a s s i n g a c t i o n SIGNAL e i n d e x : REG_BIT REGISTER; — One empty p a s s i n g a c t i o n BEGIN — T r a n s i t i o n t o s u p p l y e m p t i e s when n e x t c e l l has d a t a c l r : BLOCK ( NOT e i n d e x AND NOT s r AND ( cTou t OR c F o u t ) ) BEGIN cTou t <= GUARDED " 0 " ; c F o u t <= GUARDED " 0 " ; e i n d e x <= GUARDED " 1 " ; END BLOCK c l r ; — S t u f f f o r d e a l i n g w i t h s u p p l y i n g d a t a and t o g g l i n g i n d e x d r e f O : BLOCK ( (NOT ( cTou t OR c F o u t ) ) AND s r AND NOT d i n d e x ) BEGIN cTou t <= GUARDED d a t a ; c F o u t <= GUARDED NOT d a t a ; d i n d e x <= GUARDED " 1 " ; END BLOCK; ou tT <= c T o u t ; o u t F <= c F o u t ; END d a t a _ f l o w ; Figure 4.1: VHDL Code for Source Component 43 ENTITY sink IS PORT ( r inT inF ); END sink; OUT BIT; — request signal to l a s t FIFO c e l l IN BIT; — dual r a i l input f o r inverted TRUE IN BIT — dual r a i l input f o r inverted FALSE ARCHITECTURE data.flow OF sink IS SIGNAL regT SIGNAL regF SIGNAL gr SIGNAL done REG_BIT REGISTER REG_BIT REGISTER REG_BIT REGISTER REG_BIT REGISTER BEGIN — T r a n s i t i o n to acknowledge an empty c l r : BLOCK ( NOT ( inT OR inF ) ) BEGIN gr <= GUARDED "0"; END BLOCK c l r ; Stuff f o r dealing with v a l i d data val : BLOCK BEGIN regT regF done END BLOCK; ( ( inT OR inF ) AND NOT done) GUARDED inT GUARDED inF GUARDED "1" GUARDED "1" r <= gr; END data_flow; Figure 4.2: VHDL Code for Sink Component 44 ENTITY f i f o c e l l IS PORT ( inT : IN BIT; inF : IN BIT; - dual r a i l TRUE input - dual r a i l FALSE input - dual r a i l TRUE output - dual r a i l FALSE output outT : INOUT BIT; outF : INOUT BIT; r : OUT BIT; sr : IN BIT — request signal from previous FIFO c e l l — request signal from next FIFO c e l l ); END f i f o c e l l ; ARCHITECTURE data.flow OF f i f o c e l l IS SIGNAL gTout : REG_BIT REGISTER; SIGNAL gFout : REG.BIT REGISTER; BEGIN ct : BLOCK (( inT = sr ) AND ( gTout XOR inT )) BEGIN gTout <= GUARDED inT; END BLOCK; cf : BLOCK (( inF = sr ) AND ( gFout XOR inF )) BEGIN gFout <= GUARDED inF; END BLOCK; — NOR gate r <= NOT ( gTout OR gFout ); — required because guarded variables can't be outputs outT <= gTout; outF <= gFout; END data_flow; Figure 4.3: VHDL Code for FIFO Cell 45 start in a state that satisfies G end in a state which also satisfies G and that for each environment variable e, the corresponding counter ends with value p(e). The form of trajectory formulas makes this very easy when most components return to an empty state at the end of the period. More care (and therefore more time) is required if data values can remain in the circuit at the end of the period. 4.3 Model Checking for Speed-Independence Verification using local formulas is based upon the assumption that the circuit is eli-gible. This means that speed-independence must be verified for the circuit as well as the the stable-inputs property required for components appearing in local formulas. In this approach, the designer identifies small sub-circuits (typically single com-ponents) whose interfaces observe common self-timed handshaking protocols, and where the speed-independence of the sub-circuit depends only on its environment observing the handshaking protocol, not upon the particular values applied. There-fore, each sub-circuit is model checked with generic sources and sinks attached to the interfaces. These generic environment components have non-deterministic next-state relations that ensure that they observe the handshaking protocol, but allow them to apply arbitrary data values. In this context two properties are verified using a model checker [LGS94a]. First, the sub-circuit is shown to be speed-independent (and to have stable inputs, if required) in this generic environment. Second, the sub-circuit is shown to observe the handshaking protocol as well, by showing that its behaviour on the lines to each neighbour is a refinement of the behaviour between a sink and a source (the simplest circuit which implements the correct handshaking protocol). That this demonstrates the speed-independence of the complete circuit can be seen either from the discussion in [AL90] on composing specifications, or 46 from the protocol verification described in [SM95]. Because the sub-circuits are small, model checking is fast and completely automatic. The property of stable inputs can also be expressed as a predicate and verified using model checking. As an example, consider the FIFO shown in figure 2.1. The design is parti-tioned into six sub-circuits: the source, the sink, and the four FIFO stages where stage 1 consists of components clt, elf, and nl, and likewise for stages 2, 3, and 4. The descriptions of the src and snk components in equation 2.5 provide generic sources and sinks for the four-phase handshake protocol of the FIFO. The FIFO stage to be verified is composed with a generic source connected to its data input and a generic sink connected to its output. Model checking shows that this compo-sition is a speed-independent circuit and that at its input interface the FIFO stage only performs actions that could be made by a generic sink and that at its output interface the stage only performs actions that could be made by a generic source. 47 Chapter 5 Vector Multiplier For an example with a significant amount of data path complexity, we chose the vector multiplier described in [SS93]. The multiplier uses an iterative serial-parallel algorithm implementing the "paper and pencil" method for multiplication, with the accumulating sum stored in carry-save form until it is to be output. The key func-tional unit is the M A S (Multiply-Accumulate-Shift) block. With each bit of the serial operand, the parallel operand and the carry word are added to the accumu-lating sum (the parallel operand is first ANDed with the serial bit), and then the parallel operand and the carry word are shifted to the left, while the sum bits circu-late in the M A S bit-slices. When the result is to be produced, the sum is converted from carry-save form by extending the serial operand with enough zeroes to ensure that the carry word is completely cleared. A detailed diagram of the M A S bit-slice is shown in figure 5.1. Unlabelled devices in the diagram represent asynchronous latches (fifo cells) or sinks. There is a source (labelled with a 0) which produces a stream of dual-rail false values. The switches are asymmetric: when the control line is a dual-rail false, data is passed directly through; when the control line is true, the 48 right input is passed to the left output and no operation is performed on the other input and output. This circuit was modelled at the level of functional blocks. That is, behavioural VHDL was used to describe the net behaviour of each component, rather than building them up from gates or transistors. The two control signals organise the different time scales in the multiplier, which functions in nested cycles at three levels. The lowest level is the cycle de-scribed above which occurs once per serial bit. At each iteration of this cycle, both C l and C2 receive a single T value, followed by an empty. The middle level consists of actions which take place once per complete serial operand, such as loading a new parallel operand into the MAS block, and here C l receives an F, while C2 still re-ceives a T. The highest cycle hinges on an operand Last, which is supplied with each operand pair and tells the multiplier whether or not to convert the accumulated sum from carry save into binary representation and produce it as a result. This results in extending the serial operand with a number of zeroes and then producing F's on both C l and C2. These multiple cycles complicate the formalism developed in the preceding chapters. Theorem 3 requires a period function p in order to show that we can verify unbounded traces. However, in this example there is no clear p. If we consider the mid-level cycle which occurs once per operand pair, we see that an an output is only produced by the vector multiplier when the Last input is true. This means that the the number of actions taken by the output components is data dependent. To avoid this problem we use the outermost cycle (Last true to Last true) with a fixed number of operand pairs to define the period. However, this also fails to produce a well defined function p, as we do not know the number of operand pairs which will be supplied to the multiplier between Last's. Thus, we can show that 49 Parallel operand [i] P[i] SW1 2E IE SW2 Ctl1 Ctl2 S[k] Cy[i] - N JL>L And Adder <> <> Sum[i] P[l-1] ctn Ctl2 S[k] Cy[i-1] Result [i] Figure 5.1: Bit Slice of the MAS Block (from [SS93]) 50 for a particular n, the multiplier will function if n input pairs are provided before the output is produced. Since the initial and final states satisfy the same G , we can also assert that the system works for sequences of a particular n. Table 5.1 below shows verification times for small n's. The rapid increase verification times with the number of pairs is a result of the O B D D representations of the accumulated sum. A O B D D ' s size increases considerably when its value depends on the interaction of many variables, and the most significant bits of the accumulated sum depend in a complicated fashion on all of the bits of each operand pair. Device S T E Time (in s) Fifo (7 stages) 3 Adder (4 bit) 4 Vector Multiplier (1 pair) 14 Vector Multiplier (2 pairs) 22 Vector Multiplier (3 pairs) 602 Vector Multiplier (4 pairs) stopped after 340 min Table 5.1: S T E Verification Times Initially, we had hoped to use the middle level (once per serial operand) cycles to define p, and then to describe the possible behaviours of holding the sum in carry save form or exporting it after conversion in a complicated local formula L. The difficulty arises due to the fact that the multiplier may or may not produce the result, which means that we need to include the component which outputs the results, but it may undergo 2 or 0 transitions depending on the value of the input Last. This example had the most complicated periodic global formula G. Because of rings contained in the circuit, not all components return to an empty state. Correctly determining G was the most time consuming aspect of verifying the vector 51 multiplier, although this included finding a suitable initial state for the system. Part of the difficulty was caused by the existence of periodic global formulas which do not correctly initialise the system (and result in incorrect function). Part of the difficulty in describing the global formula comes from the restric-tions for the trajectory formulas used in S T E . Disjunction is not easily expressed in S T E , and as a result the global formulas have to be described exactly as a function of the inputs and initial state. This requires a precise understanding of the circuit and its cycles. For example, for the vector multiplier the data values wait in different points of the circuit depending on the value of the Last variables associated with the last two operand pairs. Including disjunction would allow the global formula to be a general predicate which includes all of the possible final states, although it still would not handle the fact that the output behaviour depends on the input data. 52 Chapter 6 Conclusions This thesis presents an approach to verifying speed-independent circuits that ex-ploits the observation that the sequence of operations performed by each compo-nent of the circuit is independent of the order in which the operations are performed. The specifications have three components: a local formula, a period function, and a periodic global formula. The local formula and period function capture the desired input/output behaviour of the circuit and are usually simple and intuitive to write. The periodic global formula describes a set of states that are equivalent to the initial state with respect to the handshaking protocol. Typically, the global formula is not an "interesting" part of the specification, but it is needed for efficient verification. While it may be complicated and depend on user knowledge, the knowledge which is required is a detailed understanding of the circuit's function. So, while the system is not automatic, it requires information which the system designer is likely to have (as opposed to requiring a deep understanding of formal logic). We have implemented the verification techniques described in this thesis us-ing a combination of model checking and symbolic trajectory evaluation. Model 53 checking is used to show that the design is speed-independent. These tests are performed separately for small sub-circuits in the design to avoid the state-space explosion problem. Symbolic trajectory evaluation is used to verify the local formu-las and the periodicity of the global formula. This are done using a deterministic circuit model that allows large designs to be handled efficiently. Although symbolic trajectory evaluation was used for the given examples, the framework of local and global formulas provides a general basis for applying verification methods designed for deterministic (i.e. synchronous) models to speed-independent circuits. Using the Voss Prover (STE combined with a specialised theorem prover) would significantly increase the size of circuit which can be verified by this method. As examples of this technique, several speed-independent data-path designs have been verified, including a simple FIFO, two designs for an adder, and a vector multiplier chip. 6.1 Future Work The inability of this theoretical framework to completely verify the vector multiplier (that is, verifying correct behaviour with an arbitrary number of input pairs before producing an output) points out where shortcomings could be addressed. We believe that the theory can be extended to allow multiple global formulas {Gi, G 2 , . . •, Gn} with local formulas describing the input and output sequences which move the sys-tem from one to the other. This creates an abstract finite state machine where the arcs are verified local formulas describing transitions from G{ to Gj. With this added structure the vector multiplier can be thought of as having 2 recurring states: the empty state after producing an output; and the state where it has a partial sum stored and is waiting for a new input. Figure 6.1 represents the corresponding 54 abstract state machine. Receive final pair and "Last" signal and produce output Figure 6.1: Vector Multiplier: Abstract State Machine A simple theorem prover could be used to manipulate results and record proof obligations. If the check for speed-independence and trajectory evaluation were included as tools for showing base-level facts, results could be combined using specialised rules in a manner analogous to the Voss Prover [HS95]. A further ex-tension would be a formal framework in which subsystems of the circuit could be verified independently. For the vector multiplier this would allow us to verify the multiplication in the MAS block one bit at a time (as in [AS95]), permitting the verification of systems with much larger data-paths. This research could also be extended into other models for asynchronous cir-cuits. Delay-insensitive circuits, which allow both components and wires to have arbitrary delays, are a subcategory of speed-independent circuits, and can already be verified using this method. More general classes of asynchronous circuits would require more structure, but any hazard-free circuit should be possible to verify using a synchronous model. For example, hazard-free timed circuits are still deter-ministic. One possibility would be to show that they are a refinement of a speed-55 independent specification using model checking [LGS94b], or the separation of events in time [HB+94], before verifying synchronously. Finally, some circuits are not speed-independent at their lowest level, but have a deterministic model to which they should correspond. An example is the Counter-Flow Pipeline Processor [SSM94], which contains arbiters and is therefore not speed-independent. There are two approaches which may allow us to work with these circuits. Arbiters could be modelled by speed-independent components with a choice variable supplied by the environment that determines the direction of the grant in the event of two requests. Correct behaviour can then be shown regardless of the choice variables supplied, which shows correct function given any permitted behaviour by the arbiter. The other approach would be to observe invariants in system behaviour which allow a formal equivalence to be shown between the circuit and a deterministic model which could be verified using STE. The Counter-Flow Pipeline Processor might be accessible using this method. Invariants could be shown based on the pipeline rules [SSM94] which show that each instruction executes in an environment where it appears that all previous instructions have executes. However, this approach would require sophisticated users to develop specialised invariants for each circuit. 56 Bibliography [AL90] Martin Abadi and Leslie Lamport. Composing specifications. Technical Report 66, Digital Equipment Corporation, Systems Research Center, October 1990. [AS95] Mark D. Aagaard and Carl-Johan Seger. The formal verification of a pipelined double-precision IEEE floating-point multiplier.. In Proceedings of the 1995 International Conference on Computer Aided Design, Novem-ber 1995. [BC+94] J.R. Burch, E .M. Clarke, et al. Symbolic model checking for sequen-tial circuit verification. IEEE Transactions on Computer-Aided Design, 13(4):401-424, April 1994. [Bea93] Derek L Beatty. A methodology for formal hardware verification, with application to microprocessors. PhD thesis, Computer Science Depart-ment, Carnegie Mellon University, 1993. [Bry86] Randal E. Bryant. Graph-based algorithms for boolean function manipu-lation. IEEE Transactions on Computers, C-35(8):677-691, August 1986. 57 [BS89] E. Brunvand and R.F. Sproull. Translating concurrent programs into delay-insensitive circuits. In Proceedings of ICCD, pages 262-265, 1989. [CLW85] T.A. Chu, C.K.C. Leung, and T.S. Wanuga. A design methodology for concurrent VLSI systems. In Proceedings of ICCD, pages 407-410, 1985. [Dar94] Mohammad Darwish. Formal verification of a 32-bit pipelined RISC pro-cessor. Master's thesis, Department of Electrical Engineering, University of British Columbia, 1994. [Ebe91] J.C. Ebergen. A formal approach to designing delay-insensitive circuits. Distributed Computing, 5(3):107-119, July 1991. [Gup92] Aarti Gupta. Formal hardware verification methods: A survey. Formal Methods in System Design, l(2/3):151-258, October 1992. [Hau95] S. Hauck. Asynchronous design methodologies: An overview. Proceedings of the IEEE, 83(1), 1995. [HB+94] Henrik Hulgaard, Steven M . Burns, et al. An algorithm for exact bounds on the time separation of events in concurrent systems. Technical Report 94-02-02, Department of Computer Science, University of Washington, Seattle, 1994. [HS95] Scott Hazelhurst and Carl-Johan H. Seger. A simple theorem prover based on symbolic trajectory evaluation and BDDs. IEEE Transactions on Computer-Aided Design, 14(4):413-422, April 1995. [KK +92] M.A. Kishinevsky, A . Y . Kondratyev, et al. On self-timed behaviour ver-ification. In Proceedings of TAU'92, March 1992. 58 [LGS94a] Trevor W.S. Lee, Mark R. Greenstreet, and Carl-Johan Seger. Automatic verification of asynchronous circuits. IEEE Design and Test, 12(1):24-31, Spring 1994. [LGS94b] Trevor W.S. Lee, Mark R. Greenstreet, and Carl-Johan Seger. Auto-matic verification of refinement. In Proceedings of the 1994 International Conference on Computer Design, Boston, October 1994. [Mar89a] Alain J. Martin. The design of a delay-insensitive microprocessor: An example of circuit synthesis by program transformation. In M . Leeser and G. Brown, editors, Hardware Specification, Verification and Synthesis: Mathematical Aspect, LNCS 408, pages 244-259. Springer-Verlag, 1989. [Mar89b] Alain J. Martin. Programming in VLSI: From communicating processes to delay insensitive circuits. In C.A.R. Hoare, editor, University of Texas Year of Programming Institute oh Concurrent Programming. Addison-Wesley, 1989. [MB59] David E. Muller and W.S. Bartky. A theory of asynchronous circuits. In Proc. Int. Symp. Theory Switching, pages 204-243, 1959. [MFR85] C.E. Molnar, T.P. Fang, and F.U. Rosenberger. Synthesis of delay-insensitive modules. In Henry Fuchs, editor, Proc. 1985 Chapel Hill Con-ference on VLSI. Computer Science Press, 1985. [MG93] Thomas F. Melham and Michael J. C Gordon. Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, New York, 1993. 59 [Mur89] T. Murata. Petri nets: Properties, analysis, and applications. Proceedings of the IEEE, 77(4):541-580, 1989. [OR+95] S. Owre, J. Rushby, et al. Formal verification for fault tolerant architec-tures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107-125, February 1995. [Pel93] Doron Peled. All from one, one for all: on model checking using repre-sentatives. In Proceedings of CAV 93, LNCS 697, pages 409-423, 1993. [Seg92] Carl-Johan H. Seger. Introduction to formal hardware verification. Tech-nical Report 92-13, UBC, November 1992. [Sei79] Charles L. Seitz. System timing. In Introduction to VLSI Systems (Carver Mead and Lynn Conway), chapter 7, pages 218-262. Addison Wesley, 1979. [SM95] J0rgen Staunstrup and Niels Mellergaard. Localized verification of mod-ular designs. Formal Methods in System Design, 1995. [SS93] Jens Spars0 and J0rgen Staunstrup. Delay-insensitive multi-ring struc-tures. INTEGRATION, 15(3):313-340, October 1993. [SSM94] Robert F. Sproull, Ivan E. Sutherland, and Charles E. Molnar. The coun-terflow pipeline processor architecture. IEEE Design and Test, 11(3) :48-59, Fall 1994. [Sut89] Ivan E. Sutherland. Micropipelines. Communications of the ACM, 32(6):720-738, June 1989. Turing Award lecture. 60 [Udd84] Jan T. Udding. Classification and Composition of Delay-Insensitive Cir-cuits. PhD thesis, Eindhoven University of Technology, 1984. [vB92] K . van Berkel. Handshake circuits: an intermediary between communi-cating processes and VLSI. Technische Universiteit Eindhoven, 1992. [Wil91] Ted E . Williams. Self-Timed Rings and their Application to Division. PhD thesis, Stanford University, May 1991. 61 Appendix A Proofs The actions of simultaneously enabled components commute without changing the values of local formulas. This fact is the keystone of many of the theorems in this paper, and is formalised by the following lemma. Lemma 1 (Commuting Actions) Given an eligible circuit (V, R, C, E, Qo), a weakly fair trace a, and a natural number i such that a1+2 exists, let c and d be the components such that (a\al+1) G Rc, (a'+1,al+2) G Rd, and d is enabled in state a1. If 3 is defined to be the sequence of states such that 3k = ak if k ^  i + 1 v{3i+1) = v(a'+2) ifveOd v(3i+1) = u(a') if v $ Od then 3 is a weakly fair trace, and a = 3. Proof: To provide structure for this proof it has been divided into sections. Here is an outline of the proof obligations and their structure. 1. First, we must show that 3 is a trace. This requires two steps. 62 • We need to show that (/?',/3 t+1) G Rd- There are two cases. — d has no output choice - d has output choice • Next we show that /3l'+2) G # c. 2. We have to show that a = (3 by showing that vk(a) = (/?) for any component e with stable inputs. This is broken up into two cases. • eeCl)E-{c,d} • e <?Cl)E- {c,d} 3. Finally, we show that /3 is weakly fair The proof will follow this outline. The following is a review of some facts which will be used repeatedly and without further justification throughout this proof. First observe that if d — c then a = (3, and therefore a = (3 and (3 is a weakly fair trace. Thus, we will assume that d / c for the rest of the proof. Since a is a trace, we know that reachable(al) is true. By the definition of /?, for all k ^ i + 1 we know that (3k = ak, and from now on we will write a' and a'+2 for /?' and /3 , + 2 . Finally, since d is enabled in state a\ we know that there exists at least one transition € Rd- We will use s to denote the final state of this transition. Showing that (3 is a trace Showing that (o',/3 i + 1) G Rd 63 Case 1: d has no output choice By speed-independence and the fact that (a', a'+1) G Rc, we can see that there exists an element of Rd which starts at a t + 1 and produces the same outputs as the transition (a\s). That is, 3s' G 5. ( a i + 1 , s') £ Rd A (Vu G Od. u(s) = v{s')) The absence of output choice implies V(s, s 1), (s, s2) G Rd- (s1 = s2) In particular, a t + 2 = s', implying that Vu G Od- v(s) — v(ai+2) which, by the definition of Q shows that 3t+t. = s, and therefore (ai,3i+1) G Rd-Casel : d has output choice Here we know that d has stable inputs. Since (oj t,a' + 1) G Rc, this yields Vu G IdUOd.v{ai) = v{ai+1). Because (fs inputs and outputs are the same in both a1 and a t + 1 , d must be able to perform the same actions. 3s' G 5. ((a\ s') G Rd A Vu G O d - u(s') = u(a i + 2)) Because (a\s') G i?d, we know that Vu g 0 d . u(s') = u(a') and can see that s' = 31+1, and therefore (8',3'+1) G 64 Showing that ai+2) G Rc By the definition of speed-independence and the fact that c was enabled in a 1 , we know that 3s' G 5. ((f3i+1, s') G Rc) A (Vw G O c . u(a') = v(ai+2)) Since only outputs of component c can change in a transition in Rc, we can see that the s' described above is equal to o ! + 2 and therefore (3i+\ai+2) €RC. Showing that a = /? We will show that vk(a) = vk((l) for any component e with stable inputs. Case 1: e $ {c,d} Note that for all numbers k where k ^ i + 1 we have ak = flk, and that the index of e is never i + 1. This implies Ve G C U £ - {c, d}. Vu G 7e U O e . Vfc G N.occur[e, a, k) = occur(e, /?, A;) and therefore Ve 6Cu£-{c,ti}.VA; G W. valid(vk,a) = valid(vk, f3) A valid(vk,a) =^.(vk(a) = which is the definition of a = /?. Case 2: e G {c, Now suppose that e = c and that c has stable inputs. If c does not have stable inputs, then vk cannot appear in a local formula and we are done. 65 Let nc = occur(c, a, i) = occur(c, 8, i) Considering the definition of 8, we can see that VA: £ N. k ^ nc + 1 index(c, a, k) — index(c, 0, k) A index(c, a, nc + 1) = i + 1 (A-l) A index(c, 8, nc + 1) = i + 2 and therefore VA; £ N.Vv £ Oc. (k / nc + 1) A ua/id(u£, a) => (t,(a«'»«M<:.*.*)) = „(/j'W«(c,/?,*)^ Now suppose that A; = nc + 1. Recall from the discussion in section 2.2 that assertions about the outputs of a component after its kih action are written as v(tk+1) (or equivalently v(tk.post)), while assertions about the inputs to a component at the time of its kth action must be written as v(tk). This means that Vu 6 Oc.Vk+1{a) = u( 0«'n<Mc«.»»e+2)-l) = y(am<Mc,a,nc+l)) = v(ai+1) Vu £ Oc.Vk+1(8) = v^dex(c,p,nc+2)-l^ _ v(pindex(c,P,nc+l)j _ v(ai+2j but by the definition of 3 and the fact that d ^ c w e know that Vu £ Oc. (u(a i + 1) = u(a i + 2 )) which shows that for u £ Oc we have vk(a) = vk(8). The final case is v £ Ic, where we can see that Vu € Ic-Vc{a) = t,(a»'n<M<**.»c+l)-l) _ Vu £ Ic. Vk{8) = t;(/3'nder(c,/3,nc-t-l)-l) = y^i+l) 66 Since we assumed that c has stable inputs and we know that c was enabled in state a 1 , we know that Vve J c . «(/?*') = v((3i+1) and that therefore for v 6 Ic we have vk(a) = vk((3). The argument for e = d is similar, and can be created from the above argument by changing equation A . l to read VA; € JV. k ^  nd + 1 => index(d, a, k) = index(d, P, k) A index(d, a, nd + 1) = i + 2 (A.2) A index(d, (3,nd + I) = i + 1 This shows that a = /?. • Arguing that (3 is weakly fair The argument proceeds by contradiction. Consider a component e. Suppose that (3 is not weakly fair, and that there is an k such that e is enabled in f3k and that e remains enabled for all j > k. Pick a number n > k such that n > i + 2. We know that e is enabled in (3 for all j > n. However, for all j > i + 2 we know that a3 = (3J, and so e is enabled in OJ for all j > n as well. This is a contradiction because we know that a is weakly fair. This concludes the proof. • The next lemma uses repeated commutation operations to move an action an arbitrary number of steps. Lemma 2 (Splicing Step) Given an eligible circuit (V, R, C, E, Qo), If t and u are weakly fair traces and m is a natural number such that tm exists, splice(t, u,m — 67 . 1) = u, and splice(t,u,m — l)=£t, then splice(t,u,m) = splice(t,u,m - 1) and splice(t, u, m) is a weakly fair trace. P r o o f : By applying definition 9 (splicing) and the fact that t and u are weakly fair traces, we can see that splice{t, u, m) is the sequence of states splice(t, u, rn)3 = V if j < m v(splice(t, u, m)3) = v(tk) if (m < j < k) A u G Oc v(splice(t,u,m)3) = v(uJ) if (m < j < k) A v ^  Oc splice(t, u, m)3 — u3 if k < j where c is the component such that (f 7 1 - 1,tm) G Rc, nc = occur(c,u,m — 1), and k = index(c, u, nc + 1). First, we assert that exists. This is a consequence of the fact that u is weakly fair and c is enabled in state u m _ 1 . The proof proceeds by induction on k. The base case is k = m. Because the circuit is eligible, only components in E have output choice, so if c ^  E then Vs G S.(tm-\s) G Rc^ s = tm which combined with f ™ - 1 — u m _ 1 gives us um = tm. If c £ E, we know that i =c u. By i m _ 1 = - « m - 1 and the definition of choice consistency, we can see that Vu G Oc.v{tm) = v{um) A Vu £ O c . u(im) = u^™- 1) = u (u m _ 1 ) = u(um) which is enough to see that um = tm. For the induction step, we know that index(c, u, nc+l) — k, and that if we can create a weakly fair trace a such that a = splice(t, u, m) and index(c, a, 1) = k — 1 then by the induction hypothesis we would have a proof of our claim. However, 68 by speed-independence we know that that component c is enabled in all states i " 1 - 1 , . . . , tk~l, which allows us to apply lemma 1 and exchange the actions of c and the previous component. This creates the required trace a. • Theorem 1 (Splicing) Given an eligible circuit (V, R,C, E,Qo), let t and u be weakly fair traces with m a natural number such that tm exists. If t° = u° and t=EU> then splice(t,u,m) is a weakly fair trace and splice(t,u,m) = u. Proof: The proof proceeds by induction. The base case is m = 0 which is dis-charged by observing that u — splice(t, u,0). . For the induction step we have splice(t, u, m — 1) =# £, splice(t, u, m—1) is a weakly fair trace, and u = splice(t, u, m— 1). Since t and splice(t, u, m — 1) satisfy the conditions of lemma 2 we can see that splice(t,u,m) is a weakly fair trace and that splice(t,u,m) = splice(t,u,m — 1). Since splice(t, u,m — l) ~E t and splice(t, u, m — 1) u, this gives splice(t, u, m) t and splice(t, u, m) = u. • When discussing traces from traces(R,G) and traces(R+ ,G) it is convenient to describe two traces t G traces(R,G) and u G traces(R+,G) as corresponding if t is the trace formed by concatenating the execution in some order the components active in all of the changes (u',u'+1), and where the choices made by elements in t are the same as those made by elements of u. To formally define corresponding traces, we define notation for describing active components, i.e. those components which jointly perform a transition in u G traces(R+, G). Note that we use \u\ to denote the number of states in a trace u, and |D| to denote the number of elements 69 of a set D. Definition 15 (Active Components) Let (V, R,C,E,Q0) be an eligible circuit, u be trace in traces(R+, G), and t be a trace in traces(R,G). Let Dl denote the set of components active in the transition from to ul D{ = {ceC\3veOc.v(ui-1)^v{ui)} and mi denote the number of state changes required in t to allow all of the compo-nents in all of the previous sets Dl to act (with D° defined to be the empty set) m i = £1^1 j = o Definition 16 (Corresponding Traces) Let (V, R,C,E,Q0) be an eligible cir-cuit. Two traces t G traces(R,G) and u G traces(R+,G) correspond if every com-ponent which performs an action in the trace t performs the same action as part of a combined transition in the trace u, and these actions in t are clustered in subse-quences corresponding to each single action in u. That is, V i , j eN.mi<j< mi+1 => (3d G Di+1. [t3, t3+1) G Rd) where Dl and m t - are as described in definition 15 above, and the choices made by each environment component are the same Ve G E.Vi G N. (Vu G h- valid(vl,t) A «*(*) = ««(u)) =» (Vu G Oe. «*(<) = u'(u)) The proof of theorem 4 (combined actions) requires the following lemma. Lemma 3 (Corresponding Traces) Given an eligible circuit (V, R, C, E, Qo) and two weakly fair sequences t G traces(R,G) and u G traces(R+, G), if u cor-responds to t then t = u. 70 Proof: Because every local formula L can be represented by terms of the form i £ and the operators -> and A , if every term of the form vk has the same validity and value in t and u then, by induction on the structure of L, the lemma holds. Let vk be a term of L, where c is a component with stable inputs. We will show by induction on the index i of the kth action of c in u that vk has the same validity and value in u as in t. The induction hypothesis will be u* = tmi A VceCuE. I ( -Y I ± \ K t index(c,u,i) / \ index(c,u,i) / . \ \ (occuT\c,u,i) = occur(c,t,mi) A (vc y'''[u) = vc (t)) Base: i = 0 This can be discharged by observing that mo = 0, t° = u°, for every component c, occur(c, u, 0) = occur(c, t, m0) = 0, and that every local formula v° is invalid in both i and u. Step: from i to i + 1 From the induction hypothesis we know that u' = tm', and for any component c we have occur(c,u,i) — occur(c,t,mi). Consider a component d in Dl+1. If d has no output choice, then because it is speed-independent and enabled in tm' it must produce the same values on its output no matter what other components in Dt+1 have acted before it. If d has output choice, it must be in the environment and thus have stable inputs. Because it is enabled in tm' none of its inputs may be changed by the action of any other component, and because environment choices in t and u are defined to be the same it must produce the same output given the same inputs. The combination of the above facts shows that Vd 6 Dl. stable{d) (Vu € IdLiOd.v°dccur{c^m')+1 (t) = v ^ ( ^ , ) + i ^ 71 and u1+1 — t m , + 1 . Since every element in Dl has acted once in bo'th the trace w ' - 1 , . . . , u* and the trace tm',..., tm'+1 and no other components have acted, we can see that for any component c we have occur(c, u, i + 1) = occur(c, t, m; + 1 ) . This proves the claim. • Theorem 4 (Combined Actions) Given an eligible circuit (V, R,C, E,Q0), for all local formulas L (R,Qo)\=L {R+,Q0)\=L Proof: The proof will be broken down into two parts, one for each direction of the implication. First, we will show that for any L (R,Q0)\=L => (R+,Q0)\=L Let u be any trace in traces(R+ ,Qo). We will create a weakly fair trace t in traces(R,Qo) such that t and u correspond. Because we know that (i l , Qo) \= L we know that L is valid and holds in t, which by correspondence gives us that L is valid and holds in u. Since this is true for any u in traces(R+ ,Qo), this gives (R+,Qo) (= L. Using m, as described in definition 16, the trace t is created induc-tively using the induction hypothesis (u% =. tm') A Vc € C U E. occur(c, u, i) = occur(c, i , m,) We start by setting t° = u°, which then satisfies the base case of i = 0 because for all c we know that occur(c, u, 0) = occur(c, t, 0) = 0. The induction step proceeds by extending t by the actions of the components of D' (again, as described in 72 definition 16) in any order, and by having any components with output choice make the same choices in t as they did in u. By its construction, t corresponds with u. To show that , (R+,Q0)\=L => (R,Qo)^L let t be any trace in traces(R,Qo). We will create traces u in traces(R+ ,Qo) and a in traces(R, Qo) such that a corresponds to u, and t = a. Because (R, Qo) |= L we know that L is valid and holds in all traces u in traces(R+ ,Qo), and from the fact that u corresponds to a and a = t, we can conclude that L is valid and holds in t. Since t and L were arbitrary, we will have proven our claim. We construct u and a inductively in parallel, with the induction hypothesis that the subtraces u°,..., ul and a 0 , . . .ami correspond and that Vc G C U E. Vu e Ic U O c . Vfc G AT. ua/?d(ucfc, a) => (ucfc(i) = ucfc(a)) (A.3) Start by setting u° = t° = a0. This trivially gives us the base case. For the induction step, let Dl be the set of components enabled in tm'-1. Since t is weakly fair, these actions are all performed at some point in t. Extend a by appending after a171'-1 the actions of the elements of D\ acting in any order, and requiring that if they have output choice they produce the same outputs in a as in t. This is possible because they are all performed in t and enabled in t m ' - 1 . Now let u1 = am'. Because a was formed from t using commuting operations equation A.3 holds, and by construction a 0 , . . . , a"11 corresponds to u°, u1. In this manner we can create a and u such that u corresponds to a and a = t, which proves our claim. 73 Appendix B Source Code This appendix contains the source code for the files used in the verification of the FIFO, the two adders, and the vector multiplier which is described in the body of the thesis. Also included is the Synchronised Transitions (ST) code used to describe the components for the model checking to show that they are speed-independent. Except for the three files describing the FIFO cell, source, and sink, all files are contained in this appendix. An inventory of the files involved is as follows: Behavioural V H D L building blocks for the FIFO and the two adders These are all speed-independent components using dual-rail codes for their data. source.vbe This describes a data source. The VHDL code is contained in Chapter 4. sink.vbe This describes a data sink. The VHDL code is contained in Chap-ter 4. fifocell.vbe This describes a stage in a FIFO chain. The VHDL code is contained in Chapter 4. maj3.vbe This describes a component for computing the majority of three values. vjoin.vbe This describes a C-element. xor3.vbe This describes a component for computing the exclusive or of two values. 74 Structural V H D L describing complete FIFO chain and adders flfochain.vst This describes the structure of the fifo chain. add4.vst This describes the structure of the buffered 4 bit adder. fadd4.vst This describes the structure of the unbuffered 4 bit adder. FL code describing verification of FIFO and the two adders aspec.fifochain.fi This code verifies the behaviour of the fifo chain. aspec.add4.fl This code verifies the behaviour of the buffered 4 bit adder. aspec.fadd4.fi This code verifies the behaviour of the unbuffered 4 bit adder. Synchronised Transitions code describing FIFO and adder components mc.sti This contains ST code describing the components which are imple-mented in behavioural V H D L . Behavioural V H D L building blocks for the vector multiplier These are all speed-independent components using dual-rail codes for their data. They use a slightly different handshaking protocol, so there is some repetition from the components developed for the F I F O and adders. src.vbe This describes a data source which provides a single bit of data and then stops. srcn.vbe This describes a data source which can produce multiple bits of independent data before stopping. sink.vbe This describes a data sink. alatch.vbe This describes an asynchronous latch. aswitch.vbe This describes an asymmetric switch. fadder.vbe This describes a full adder. fand.vbe This describes an A N D gate. fork.vbe This describes a fork element. mux.vbe This describes a multiplexing component. fl.vbe This describes a component for computing a special function for the control portion of the vector multiplier. 75 f2.vbe This describes a component for computing a special function for the control portion of the vector multiplier. Structural V H D L describing the building blocks of the vector multiplier pisobit.vst This describes a bit slice of the PISO (parallel in, serial out) component used in the control block of the vector multiplier, component used in the control block of the vector multiplier. The VHDL code is contained in this appendix. piso4.vst This describes a 4 bit PISO component used in the control block of the vector multiplier. control.vst This describes the complete control block for the vector multi-plier. masbit.vst This describes a bit-slice of the MAS block in the vector multi-plier. masblock.vst This describes an 8 bit MAS block for the vector multiplier. vm.vst This describes the complete vector multiplier (without data sinks and sources). testvm.vst This describes the addition of sinks and sources to the vector multiplier to allow verification. F L code used in the verification of the vector multiplier complib.fi This contains FL code for making assertions about the basic multi-ring circuit components. blocklib.fl This contains FL code for making assertions about the major blocks of the vector multiplier. aspec.vm.fl This contains FL code to verify the behaviour of the vector mul-tiplier. Synchronised Transitions code describing vector multiplier components mc.sti This contains ST code describing the components which are imple-mented in behavioural VHDL. 76 » u r- « M M H a a b Z 2 § XJ O O « ±> *" 2 O i> MO C i i is 11 n o p A U t ee ai a b. H U U ee O -H « •v. a IT) *0 ON <* —< 1 g —< >.l 5JS H H MM'-- - ta a H H H H H H H , , M H M M M M M M f - " f - « { O M D a o n a a D D n Z Z Z 2 2 2 2 2 b Z M M M M M M M H O H B-5 n a H h 9 O B o o a U ^ ees J3 U I "8. tfu ( •H U S f a m Bg gg 77 */> o •M J: o « e ••3 m O in o rs *> .. © :t n u > M • «-< at •H ii *M <u « 0 " J JJ «M MX (H W *0 «W «/> > H H § 2 -1 H H M M M H H H B 0 8 H 03 03 D) M M O O O M co b b n M M M M M M 0 JO H a z z § £££££££££££ H H HHHHHHHHHHM M M M MMMMMMMMMMMMMMMMMMMMMMMOQ D i n o n D c a n a n n n o n n a f f l f l n n n a o a OOHH m m tn ut to to r* p« 3 g eeese esses esse Bses'sees? a a - x i E S to g o S £ CO CO £ £ 2 %\ £ E « 2 £ CO CQ J 2 — C C 3 3 > O Z — > 3 3 « O Z — C C > O | f j ^ d ^ d 582 ~H 82 —5 82 — fi5 5 to 5 G 5 K 5 5 5 a 3 o c V> O -H « In « m h •• o to *u l i • * n U tt ca 2g H H M M » 03 03 z z z z z z z z b z Ed S a 2 W H H « 2} M to w -H M M HQ goto: 5 a H H O h t> &.MM c e e O W O , -H • • -H ?s§ si - - s fl 3 3 — •o o o c H b. O K w too - * u A CO tX CK o o X K CQ O H u. II 3 O Cu .. .. t» AI a 3 3 PC O O O z UJ w H U c 5 5 e « 8 3 l i f t -OK OK > •WU f I -*0 — I I • • • O li Q V V *J Q ~ - V V ' V V V o pap) ~ g a s «SUUK«COH JJ J «JCSJ3OOOO>5—K HWWZ ( • H Z b d B H> Z b D I D coco -o 5 M M W P L | W 5 P 5*3 p 1 1 s . I i I i s : I - g i g § > a 78 m m • . I O U ) i f i i e > 9 h h f~- r - 3 £ 03 CQ r - ca m I H n m r - o n n o o o 9 Hb. > >Hb . H > > H b. H U. > «H 0 ' P. A A A A A A O A A A A A A A A A - « B B 0 I H o « — — -rt CU XP» D O £6 *" £ o « H E ^ aS a m B C > 3 3 H C C > 3 3 H C C > - H > m o o r * t f - H - H > a o o . . « - H a " o o o • M f l e i a lessee a Bessee a eesiee a eersiie a le-s^ee • « • 9 0 A A A A O A A A A A A O A A A A A A O A A A A A A U A A A A A A I> A A A A A A Q» — K n i t O - ' B B a i l l O — • • > • • • O — O — B B B B B I I 0>— B B I B B I I t) « M <M « * «M <M ii es. s l e P ee s s e p ee a S e e ee 2 i E P ee s i » P ee S § S-S rt'S55>S§? • cS55>SSS ^ £ 5 5 > £ g g „ £ . S 5 > 5 § g ^ £ 5 5 > S g g x uS - £ 2 ^ £ 2 ~ .22 ~ £ 2 - £ 2 ; M M -A -H -rt -H -H g K I M * M <H <M *U a 7 9 o o 03 03 b . b . XI XI S S " S i ri • • «H ^ >r* o o ca ca H H •a « ee Xt « M CO 03 H H H M H m ca H H M M f-« 03 03 b 3 S O H O O > > > <J « M M f « 01 CO •> 3 0 ee. > 3 3 « 0 O O 1 M M H ca ca b z z S ki Xi M a - [ o o *n XI >1«N >HM 4 J 3 . 3 2 CV l"» « > •93 > H fN > > > > > > H H H H H M M M M M ca a oi 03 co o o ee a a S S 3 O O C • > > : O H N n V O W O H N (*>* O O e £ E £ £ £ £ o o u u o a a O r t N M V O <N O H C t n O O O H H H ^ H H £ £ a xt ca to 5 S ee OJ <N ee o rt c* CN ee O IN CN CN CO CO H H 03 GO 03 03 H H H H « « to to o r * o n ee ee ( D n tn u o CO CO O H ba > O O H > 3 3 - * ee n o O u o U Ck. o. a CT* -H O tN CO • 9 p 3 H H M M CO 03 5 5 H H H H H 03 S 03 S S £ 5 5 5 3 * U U J XJ JJ D W (0 > O t-t D XI « XJ XJ XJ XJ xJ 10 W to (0 W XI « JQ * XI H H H H M w M M 03 ca CO 01 353*1 H M H 0) M 03 CO H b . H b . x> x> - C C 3 3 . •H-W o 0 ! H H M M •> «. 0) 01 H H H H H H H «-<H M M M M W M H H C Q M cQcocQcocaeagg^ oi 5 5 5 5 5 5 5 S 8 3 ca co H b. ) 03 CO 03 03 JJ XJ s i s - 5 8 2 H H H H H H CQ CD 01 H H H M M M BQ 01 a z z z CO CQ H M H H H R H : z S s 03 03 03 0 - H b . H t> « « XI J 3 xJ xi - 3 3 > J 0 0 > « 8 c? 80 m m h - - o o o o o o o o O O l l O O O O O O O O W t - I O ja ja ja O O fl ~t-i *-* >H O O i 3 > •-i s s i s g B e e e s e e s a e e e e e e e s i a s eessee t e e s a e e X B O H U . H U . H U . H U . S J» > 0 a A A c i u a o ^ > . a i 3 . Q u u u o A A A 0 A A A A A A A A A A A A A * * * i l i i A i i 5_StSS«S ee . o -I - s i ee Iss ee ••£«« ee - s s s ee z i Si ~ ?,2 £2 - £2 O O M > O O i ) O H K D U 1 p H b> o > • « « 9 O A A A A M — • • • • gu. X H u . « *> a u H > 3 2 « o of « o o *d O O I > o O J O CQ 03 I o H fc» e > A ja J h * * 1 1 1 I •82 9 < an *J u u H > 3 ? ' H S U O O I J: S2 a a - -82 s i ee. A o o u r i CQ CO C l s r 1 52 - 32 n n ii ti ii \ 3 §3 'i es. AJ 4J 4J h > 3 3 5 • O C O €2 81 £ £ £ £ £ £ £ « A A o o » to A A A A A A A B B B B B B B B I S3 A A « « A A U eee-gs o u o 5 > A A A A A A A i 4 « Cl (N OQ C > > < I M M * 0» <N H H A - M M m n M M co a 5aA > > A A A A A A m m - -e m n n U< H N « « > > CM <N a a t- u . 0 « ee A J3 n a n n n ffl « « A A A A A ^ " I I B I I ee « A A o o o o : IS -*.eeeee ^2 ee E a XJ o o O > I * SS g p 52 ee ' 3 n i i E < B G > 3 3 < ctf -H > a o o 28 ; SS CQ ffl «•* c c > £2 Xi XJ O O - £2 E CO CO . t- u. -1* c c H tfrtrt : CO CO M M CO CQ a a > > a a A A A A A A " B • • B B B M M - - M M rt O O A A rt rt rt 03 GO M M CO CO rt O O « rt rt rt 0) CO *n rt CQ a • H fix o rt H ftu u a a > > a « o *M A A A A A A O cc -£2 ee ca co XJ XJ SS55>Sgg ; £2 : «*ee £2 S h o r t H b. A > > A A ee ca ca H U. _ . . XJ Xi - £2 : O A A A - p —• B I B O O rt rt 03 CO a • A A O O • - M M O O CQ 00 rt M e* k > > to a A A A A ."ee © fr; e c 82 rt CQ pa 1*1 H C > 0 0 A A A A A A tt u N tt n il a « > 03 CQ -H rt > < <W A A A A A A * £ CO 03 1 H h. 22 e e SP? 5 os > > > rt o O P . o o o o M rt » * CO S O O CO CO a tt > > a a " §§ 00 00 8 £ tn t* h. A> AJ o f C C > 3 3 m p C r t r t > « 0 0 «S 2 e e A A 22 > > « O e e •3 e e M H C ti n ae -H «2 2 > > « a A A A A • • I • e e > 3 3 > « O O g£B 0 a i l o cw • H e e e n o ! a <DJO *u 2 M M M SP3 A A A f-1— MOB & "S2 © o <N M CO 00 H b. O © 00 0 M rt H fa > > « * z 52 . ' s a e > (-> c c , I CCrt rt ! M M «• » r t m CQ CQ rt rt 0) 0Q fr« C M rt H b. « « > > « « 1 » < CQ 00 ; . s e e > M CC rt rt > * O 0 - £2 M M M M M M M M -M M M M M M r t r t M o Q c o o a o o c a o o c o a M M H b > H b . H b > H h . X r t A A A A A A A A A A - i i i a i t t i i i i CO CO < at « « , - 22 l A u u o o > & n g P Q n a Q O Q O Q n M r t A A A A A A A A A A S2 2 O g C Q C Q G Q G O A i A i £2 83 n n n n . - o o .H M Cf * 2 r> m m * ^ i", n n m « ci » •» rt 5 5 5; J "r _ a a a n a n n • • • • • • • i i n i a a o P ? - 1 8 P 2 S S S S S Z E u u n » S > • « S J J O O O O 5 > « « > B « > m m > o o > A A A A A A A AAAAAAAAAA U AAA AAA _ £ S i -SSS "So, 1 CO. CO. CO. Cf, CJ. s s a s s e Z • s s « p > £ e > > « 2 e e >Sse e s s ? ? a • • ! B s e e e s e | | » • . . n i i * . . g l l L . . B | | > - g l e g ~ g - B C - e - c • ~ B Z £ 84 jaxt A A xJ XJ o v* - O O i sees > « « < e« ms es, z 32 h > 3 3 i < A. to o o t I N N ll • O O U sees v > X t X l X t U A A A A t c i g i i H XI o XJ XJ XJ > 3 3 * IS O OTJ • o O XJ sees > « « « o O A A A A I* — • • • » '3 s> ~ 32 XJ' XJ J i > P 3 < : a o o i f i n h - O O XJ i-i CO (0 W O H U> r> > X t X t XI O Ck. •s ee. XJ XJ xJ H > 3 3 * r, OS to O 0 "0 O 2 O O O O O O O O • 5S1 I t S M S •32 : •see a . . O A A A A A A A « » > > A A A A P. •22 eee . . O A ee XJ XJ 0 0 > tt . .ne PC <o o o - a M M H M CQ CQ CQ 0) eeee u « XI » n O O O «H O CQ CQ CO CQ P H H e H o tfXi ca o o o o tH s eeee o « xi m 552 •3 8 ee -55 6 82 O O O f » CQ CQ CQ CO o « X l to -11 o MM \> > > * O O O f-l CO CQ CQ CQ (*. b. la. b* O « XI «0 U A Xt tt O O O O i O O O «H r CQ CQ CQ CQ 0 o « xi ta t © © © O « eeeee O O X - O O V o CQ CQ I o . H U. -• o o u O CO CQ W O H k O > « « « 1 C XJ 3 & 0 B i "5! yr1 82 CO CQ H b . i xJ u J > 3 3 < - 5 o i CQ a H S « xJ xJ xJ o n o u o 0 A A A A 3 o o. '$ ee. xj XJ *J « 2 9 O A O 0. m < ~&6 z 52 y* y* U O O XJ CQ CQ W ( • • V H « fl fl A A A • • I CO CQ H €*• fl xJ XJ XJ g83 O A A . . 8 i e -S6g S8 — H www tounuoi 85 o o O f H < - i r « O O O O O O O O M n t*\ o o o o © o rt rt *n o o © o © © rt rt e e e B e s s eeeeeeeess l i s e e e e e e e e i s eeeeeeeei:: ja o o n o S > 00.ax.uuou>> c >>> « « i 3 j a o o o m i » > B « J J £ U U » M > > A A A A A A A A A A A A A A A A A O A A A A A A A A A A A A A A A A A A A A A A A a N • a B a • — I I I I H I I I I B - n — M i l i i I I » i II II I « < n - » i B i • i » i i » r> > H •»"»_ •rtO. Ot 0 0. fiO. e e g g e e - g « *$ e e a g ee . . e . e e e e g e s a > „ • S H C - B • H e e e e e e 3 , 3 ' > • • B e e B e r " " ' " <N p > i r t p « r t o ^ 1 _ - V 8 - I O O O O O r t r t « - - r-,i-,—,r-,i-ti-l-4r4 - r - ' ^ - t r t r t r t r t f S r * - - - P* M Ol O O O O O O O O rt rt O O O O O O r t r t r t O O O O O O O O r t P« n 5 5 5 P9 ffl ffl a CQ CQ CQ O rt O O rt CQ CQ CQ CQ CQ 03 CQ CQ © rt CQ CQ 03 03 CQ CQ CO CQ O M O O (N N CQ 03 sssmsg? a s e s s s e s t f c g ? .ssaesssg? e gs? ess rt rt A A A A A A A A A O A A A A A A A A A A A A A A A A A A A A A A A O A A A A A A • • • • • • i l l -p— • • • ^ ~ I I I ^ ~ I I I ee - -3 - si ee si ee „ -3 - si „ e ffl CQ CQ CQ xi rt 3 CQCQCQCQCQCQAJAJ fflCQanfflfflAJAi& -32 - "22 £2 & "SS z 22 ^ - P 8 - 3 ~ M V 8 CC 0 < 8 6 c c — o u o Ai > O MO 5" *4 9 rt C 85 •Ort M 0 rt a «w u • u t> • a rt •H-H e o«" M «M jB j • 0 rt ii S rt > Urt Dirt O M rt Ai TJ > 0 DS 3 ,J TJ TJ TJ TJ 0 0 0 0 ^ o o o o ttXY H H <M n n 0 9 rt M rt — I rt , * r t a a • rt H « 3 Ai R ( 0 3 « > — W O m u o*H n o • oi « A> —x: < • j . —— jz < 0 | —XT AI 5 a a — — XI rt rt C *i rt rt O 0 9 rt to u o Ai <M 0 TJ 0 1 o . ! Ai > Ai Ai Ai 03 n o H bu rt 0 0 > 5A e e •• H C C > CC rt rt • 03 CQ rt « 0 > A A A « S CQ CQ f* u. H C C > tt rt rt « 2 2 ees . CB > •see •• t> c c > at-*** 0 2 2 03 03 f ) H f c H » 0 > C 0« - i i ee A A A — • • a M CO. •See 3 2 e 8 7 JJ o 58 & a u — 3 • O $ O 22 C C N X ! 9 — 3 — § — O • CM o « » £ Xt w r* c* i i X O U -ri —- TJ Q JJ O CT> C U rt C • "O J> O R «f 1 S C O B C -H O in * TJ . — co - a <* c a * < o e o v t 8 0 <u C O V . O H «C -rt O «H S <M h w >, JJ JJ co a <u tn U tx u — ... c — • 1 4 0 -rt -H CD ~ — f H O M U fH - C C C C C C C C N •U XI O w . -H^ -H-^ -H-W-*.* a BU > -rt — M C O O r l r t N N n n H O C » JJ H • eg ~ x i H t a x l « > X t < 3 X t > 9 X t « i u co i—I Ck «H "O — U • • • • • • • • -rt « <M-H «" -H C — • *J G U O • U O ' • U • « O O O O O O O O -rt O JJ -rt C H O « ( I H H I - I H H W P - I H CCDS O " 5" a5.-*i s - • a " s-a-a-a-a-a-a-s^  - i i as A C U U H K H C - ffl Z O C »B-rt-<-H-H-rt-H-H-H .................. O C CP — o . •O •Hfl'MUa r-t • JJ «. • - H h h h b h k r t r i - b b b b b b b k JJ • U-H <u u . > H -H<H n e i J ww k i « « « a a « « « b . * • >< cp u • r t - H B o w <M<U c o i o o « > > > > > > > > n i i i i H t t i ( o c a o a « l4<MXiJ • O f t Z Q JJ JJ > « C -*H T3 -H i to u » - H * J £ H r-t ^  o Q g c a n • • > • • • • • c c c c c e c c o a c _ « « <rt > U H 0>*rt "Ufl • J M -rt-rt I C-rtH-rt-rt-rt-rt-rt-rt-rtl-rtTJC «M O h-HU *8 >. I I r-i r-1 C C C C C C C C • H O O W ^ N W n n JJ JJ c — "-H TJ > * X 3 TJ * T J P U K C-H-H-rt-H-rt-rt-H-rt O « X I * Xt A XI « Xt U-H*J -rt T J * fl • C Z K Z O y - H O O H H N N n M C C * — — HO O O _ « U CQ &] * "v. U« X l « X l « X l«XtU4JJJj-l4JJJJJjJJ-> 3-4<H — — V > > t J T 3 T J T J T J t J T J a . h © O O O O O O O O fc C « fl « fl « JJ Jj JJ Jj JJ JJ JJ JJ JJ JJ JJ JJ JJ t-ifHfHi-.f-«r-.fHfHrH Jj -H •s. O O O O O CD (p CP CP CPCPCPCPC9C9CPC9CP -v -v, -v. -v. CJ) C — T J • e > h JJ JJ C « 3 to C u •J "H • . •4 < < to c e c I B H H l l W H H • H O W © CTJ U O to to I I JJ JJ § § § M M M I. I J O M V * J< I c c c to ca to -« JJ JJ JJ C -rt C C C U O O r-t U c XI « W K U • CO (0 10 • JJ u u u ta JJ JJ JJ to C to to CO CP O O (H O O « XI « o o o o o n i4 u n t>> I • to a a v i l l i •rt JJ JJ JJ JJ C -rt-4 -rt-rt •rt c c c a JJ JJ JJ • • * H H H 88 c •rt X) - C " C M o in -© - c • rt C M -H 4 O • n 0 C O XI — u 5 - c"c u i i B H n - 4 J 3 X ) o •-•% •3 - -— C - "c "e • -H -rt v — Q •HXIX) ?! « — • « a —- -rt -rt Lot C H M - H a 0 a "c "c C -H -rt STE 1 O 0 0 • x i a > let A i 9 i-i g o 2 53 — Q I ! 0 « 5 < - V M — AJ M a *J C 9 -3-U B C X 0 0 0 <M IM B » 3 O Xt » a o o *M rt 0 «M S 0 A i XI A i O A i ?. -rt IS C C C C C W | i-4 M M r» «*i Xt 0 XI 0 X) o o o o o M M M U U 0 0 0 0 0 M M M M M A i A i A l A i A i 0 0 0 0 0 X) 0 XI « XJ o o o o o M Vi (* h Vi 0 0 0 0 0 J J J J J w4 -rt -rt -rt -rt C C C B C •u M 0 — • -rt AJ — B rt 0 * — rt rt 8 A i • rt 0 0 3 A i 0 O 3 0 0 — A i O U 0 M Oi*M 0 0 •• • 9 e —x: < • j . >i——x: < 0 9 — X! Ai x: 0 « AJ rt rt c -< rt 3 AJ • • rt 0 U O AJ Xl *M «4 O A i | | C A i A i 3 m-^-* +* A i C C W rt rt 0 0 2 0 O a 0 H 0 M A i 0 rt U O B 0 9 Ui*> T> 0 O 0 0 O M T-i rt T J > e B o o u u fc, &. — 0 0 0 H A i A i 3 S i t 0 O 4 Ai*u 3 01 & n • • A i < < -rt XJ XI B S — ' — 0 O r t —. 0 H A i M « M <M rt rt S3? c e o O B 3"* * n s •2S a u — xi A i A i E C 55 i o a M M «U IM b, h . — u jj n g S S A i «M X » B I • • A i < < rt XJX! C — • t • 0 • 0 — M — X! • V O H •1 •o O u 0 -rt O a > x •rtrt a n A i O rt A i I 3 A i Ort rt IM rt Crt ) rt <M O 0 rt C 5 O O * ^ A i A i AJ rt rt •HCB 4 X 1 O - - C O C Crt -T J • rt rt " T J 0 XI 4 O - - r t X) 4 55°8' a M M - T J O X l f t u T J • M — — M rt O — IM • I • I I < C C O | M •S e & o & « « A i IM • O C A i A i A i A i —• c o i i r -g£8 • A i O M rt A i >10 0 AJ « 0 A i A i 0 S>. H' S I S H rt — O C U P c o 0 rt A i 0 A i — > 9 0 ~*m*4 c rt -rt fi — • o rt O O -n IM > rt C I I I IM A i A i g C ~ 4 r t 855 •s 1 A i A i n s M B A i 0 89 C C f l c c •«H •rH -rt -H -H XI flXt 0X1 — 1/1 — a a o o 14 t-t Bu Bu -< to to a u J J 0 -rt o 03 Sail S 5 m U « « o <w b K «w « •rt TJ J3 JM B • O n e — ~ H O O 4 JJ«4 g 5 8 SS 14 U «U <M Bu Bu — O n u n 3 3 U o o q XI « XI « Xt o o o o u kl M (4 h t-t to to to to ca CD CO 0 « n i and 13, to e ca ~u o to "kH h I* l l 14 -rt x «j B B B 22 H co to w co n H IN N C l M XI * XI « XI to •• O J= J J - J J ft rn « « o o m - i o o o o o to( B | « to( W | lions cell: >al wj J J u •rt -H c c J J J J -rt -4 B B t) i> 11 11 i> c c c c a Fund Fifo to d< V CD -v. U O u — to — • « CP 0} a o > • V • o 0 U B « T » . V , ( J J J J J J -rt -rt •rt B B fi H H a > x <M D c c B C "rt _ G C Bu -rt -rt « m ri -a, 0X1 Bu O b.h.b . ' g D I B I o o o to O fi J J J J J J J J G O Q 0 CP CP J J — 0 > « B •rt OP B r> -rt C — - n o •rt o a T I - e V i I «M JJ JJ Q C -rt -rt 5 o c e H U H H 0 >i B « O TJ U O •a =s o 2 q -rt b. < o « a J J 3 B I CM O J J O J J o 55 JJ 0 « CM O tn to cn <a 01 H CD Xi a « XI • C C C C C C C C u o -rt i <ut< CO 0 >M G — C J CD — - - - - -rt M _ b. C •rt X Du C H W C H I •3 • J J CO H I 5 e ) h O J U J 1 4 to to I I Jj J J • r» o» o» B " B fi* *B f 4 r t r t - H O O O H 0 Xi 0 U O O H U 0 Xt 0 U O U U a rl >« h • to 10 to •3 a 0 H4 B • o O H It to o TJ W M • J J O - « M « H • • O U H X ™ H 0 *M M • %4 O • > H • r t H fi Q «M h « 4 £ J . 0 H J J X ! H > K H Q H CD W H J J •o > m x a 3TJ T J T J T J m « « « *•» O O O O 9 - i 33 0 • XI Xt O B O O J J J J a n CP.-l.rt.rt.rt.rt.Hr-' .rt XI 0 0 0 0 I a-4 t4 t4 >r* m H M h h m h M h k K 0 0 0 0 0 0 0 0 0 > > > > > > > > • • • • • I I I C C C C C C C C • H O p H H t l D r l r l U 0X1 0X1 0X1 0X1 Bu 6u b> b* P C C C C C C C C H O O H O 0X> 0 i JJ JJ Jj JJ J C 0 g B • •rt e 9 H > 0 C H (0 o c 3 — » § c _ to • H TJ H B O CBi C _ O H | H TJ C J J *> c — O H J J H C C CD 5 I J J c *3 H TJ C W JJ JJ r H 0 I C T J I a J J h »4 n J J J J J J co B to co ca CP H O O H O O 0 Xt 0 o u o o o ca u u u u l co to to (0 JJ I I I I H JJ JJ JJ JJ C H H H H H C C C B 90 i . «N 4? $33 • 3 « * 0 •CO «s o o « rt cn AJ o "0 w n -- 5 tt 9 • U u « TJ 9 o CC B2 U S S3 § ° X 0 55 S3 B) O O 03 03 3 AJ 1 • ) O > AJ •jjr. U O « IM > <H c • « • • O O O S2? " - B O TJ 0 i D>AJ 9 § « 3 8 v IM 2 V — Q 0 & Q A l AJ TJ £ • 0 • • C O C O -0 O 0 JJ TJ A i TJ AJ • rt 0 T J « O rtTJ TJ 0 W - 0 » f « t » A J u S 8 S •§ • • W O H TJ V V V O «C 9 2 V V V S ui rt 9 <2?g 0 M O £ 2 * A 45 *M 0 0 rt AJ > t » 4 0 « rt M 0 0 0 > C AJ 0 o a t> H » e < M TJ 2 v v TJ A 9 rt Cd tt « D rt > « 0 H • rt IM CC w o A O P 4 A DC AJ * ~H tt -t H TJ ' ' 0 0 O O Ul JJ TJ 0 0 0 0 rt JJ AJ 0 0 ~ A J r t 0 TJ O 0 0 M TJ > - - 0 » Ul <M AJ 0 O TJ M Ot 0 O 41 * sz AJ . j— o 0 TJ 0 AJ rt TJ AJ 0 — 0 > -0 0 4 3 TJ TJ 2 2 2 0 0 4 AJ AJ AJ 0 0 0 TJ TJ TJ AJ AJ AJ A O O rt H M H f l 0 0 0 r t A> AJ AJ rt 4 4 0 0 TJ TJ TJ j> — — p X t — — Q 3 s i b . a 0 3 *8 25 — — Q =s a M H b . AJ C . 0 rt • C O • 1 J? rt t » M U a t 91 M H TJ Ed * 41 TJ & 33 A i »M 0 —. u a P A i rt > TJ Ai<M M M M W 0 0 A i A i 33 A i IU A i « J •J > TJ a o o. O a A a A i AS3 B* -,33 -33: > A i 0 A3-° 0 AJ "M A i • • j g o o TJ M M » a a A i A i *i*43 43 o fl CQ CQ A i r*» r> 41*4? OBI < A • A i «M M I A i - • — 0 O O -O TJ TJ M M C M rt Dt 4 4 *• 4 rt A i A i a 4 > A i 41 41 * JJ O ^ T TJ H 0 CQ CQ T AJ r»> r i •» 4 Cd 4 A S D T J l CC — H TJ > 4 3 TJ 0 > 3 3& E 4 t i f - i . TJ 4 4 3 t>3 0 0 • > a rt 8 0 rt u P 4 A i A i 4 - « 3 * • 8 - o A i O H C X M 4 0 > 0 A i 9 AJ 4 ^~3* 1 5 — r-i * V O B E —' v K *3 u o JZ JZ •rt JJ s-s WO CO o 3 > » C-H O H ki © « TJ xi 5 TJ CO 0 0 0 XI 0 c t- -(H H H h M CQ CQ M to ea 2 2 M O O M - H b. U A£ 4-1 JJ -rt M (- O 3 3 C ' ' a o o -H -SI" 5 1 23 • z a a M Cl TO OiQ ? W 2 a o u w a q SS • 8B.! Q JJ JJ Q 3 3 3 "ZOOO M fc. U. H W Z urn Q a § *J u « u TJ 0 TJ o C TJ •H C >. * rH CO TJ s-s CT M O U «w 0 J j *J IS o u O CO •rt X C 0 •rt TJ O O c 0>Z • CQ H K x o —y 0 •• Z JJ JJ X 5 TJ 3 3 0 J CHOZOOTJD •rt <u 2M H b. C 0 < O O CT-rt O • M b ! 2 1 TJ a • a o o CT Z • o a a u u u s§§ o o o u n i t 8-0 •• Z JJ JJ X Q TJ 3 3 0 3 CCNDZ O O TJ CO •rt *u 2 M H b. C 0 < O O CT-rt Q ! ^ a § -H — X O O OKTJ C n Q Z » a o C u -rt tn AC 3 to h TJ O V> C a -* ° -OXi — M rn JJ O CP *4 Ji -rt y • • JJ it o u tf> -rt JJ 3 irt it CT 0 C TJ to •rt * - r t 0 M JJ JJ N 0 0 A -rt N r- TJ c r-t o o ^ * 0 V U tl -rt M HOD JJ *M *** JJ tn H er. Xt * C 0 H U bj U -4 O Q.TJ a to S JJ H • •si? O Q O WWW Q D Q SSS 8B5 H a w c > a a T J o • a 3 0 9 0 3 H © XI xi to c U H T J U 9 0 U U U H H -H M M H M CO CO M CO CQ M O O M H H CQ CQ 2 2 2 S & H j * JJ JJ JJ H « « 0 0 TJ -6 2 w o e CC H O ass. X H M o w w s S -rt U O>0 U c u £ i H CO -rt CQ W i O JJ tc u -H U R M n o v v kC S o JJ JJ Q U 3 3 J t* •* 2 O O CQ M H b« o b o p <M •• JJ JJ © 3 _ 3 3 0 J JJ O 2 O O C CO IflWMhll, O - -1 o OTJ q sa1 I TJ CQ JJ JJ 3 3 O O H b. JJ JJ gg 93 m i-• - H - a n m M C ( S 3 « - o n <N > 0 0 O XI u N O V - . J J * 0 > 0 J J " • H O • O JZ M H M M •» • - ffl O H •» t* H H t-.fr* H H h h O H H CQ in D D mm M M M M O M M fr* bt I H O * J J J fr* U , * J J J J * - H 0 - c c 3 3 o u c - - - i - H - H O O 0 4 - H - . 0 i i 55 BBS O * * H J « a s.. 0 OtO Q D D U U U Q Q Q §68 O Q -5 0 fr* O Q O o D>2 • Q O Q U U U O D D 555 888 0 2 « J J J J X 8 3 3 0 J 0 o T J m c _ 0 1 0 » - H Q J J J J X Q 3 3 0 >J C * * Q Z 0 0 T J ffl • H U J 2 • J J J J 3 3 O O J J J J x i _ 3 3 0 . . . 2 O O T J n t* U. C „ 94 5 « fr* - ssssssa - 6888888 K H B B H H B H -O fr*b.J$fr*b.j3jj!^ Z O O U O O U U C Q M < C < < D 0 < « O » 0> 0> D> 0»rt Q © b. D> O C « -foe •- •-< - q u o fr* u. 2 ** b . 2 O O U Q Q U C f r * < < < i ( 0 A < 3 o o> o e» » e» o> o «a fr* b. 2* fr* b. 3 Jc7 u JJ > « to 3 o C CQ M to U c to 10 >. a « a TJ c U H x: o rt g l l to fr* s rt *° c M JZ m JJ x: > O <M O O x: D> CD C rt O 3 O >4 rt AJ rt a JJ o u C in Men u OA OT X! O tux: - rt » rt a> TJ • rt •9 (0 u ~ JJ JJ < rt to M U CD C • 3 M rt • O rt TJ M • rt y c o ! * o> * & • x: c < r t : © r t — >X) w tn i i a> JJ i c r t n 3 t JJ to a J tO rt « JJ >rt 3 O. 3 H O T3 - H M £ «/>fr* M r t a o x : • *• fr* < fr* fr* M M - CQ 00 -fr* fr* fr* fr* fr* fr* fr* fr* fr* fr* M » H H M M M M M M f r * f r * M CQCQCQS10303CQCQCQS3CCI M D M M D M M M o o Z Z fr* fr* fr* M M CQ CQ S i s io O S o H t w U H b U H h O O 0 O fr. « « « x i X l « i u u a « « « M jj* fr* b. J S3 O H O rt «J ffl X JZ" o JJ « rt fr* £81 O O O O O O §ss§§§ 888888 1 1 1 1 P > 1 V V V V V V K «1 fr* b. JJ£ J *9 JJ Z O O O CQ a « M < < < „ m o o> Ol OP t* b. 3 fr* b. z o o o o o u M < 4 < CQ CQ < O 0> 0> Ol Oi Ol cn 2 § < < s < 3838 n H a • •> V V V V * CQ O 8 fr* h> Jk> JJ . J z o o u n a . M. < < < m a o oi B H p 95 o o O H Ai co a « H 14 « in TJ ( <7\ 4 <T\ r-i ->2 ii I 3 » ( (J I 14 O I U A !« u to i « a H to * i to » H « g a T J H M £ V J - H M H O f i tw H H H - - H • - H - - H (0 (0 H H M H H M H H M H H H O H H O H H O I H H H coca coco co CQ s o n H H H O O z z b z z D z z n z z z M M O M H O M M O M t H M S CO U H b 6 2 Ai Ai JC X - H U . O H U . U H U . U 3 3 O - 3 « « « x i x i < i u u a o o 0 — fi " s * i — z to 511 l i s 318 0 8 . . . * 0 V « flUZHCu U CO to q & & o»Q W 0 • a ia U Id O ggg 0 0 II B 0 V « vvs§ Z H th U CQ - sss * < V 2§ SSS; ' 5 & & u n to < « O « H a co K 38 V V O Z H k U n o C Ai "2 * H O C * «w O o a o H M O H y v v B « m q> H <*TJ a I v* to • 3 * 1 o o to • H H 4 H H 1 ca ca M M H M H XI *S Ai CO > X I H T ) JC « -Ai t4 to C 0 to Ai CO 3 CO - to O «M TJ H V* M J3 H H v > H O T J M H - JC H H O n 3 * 0 M O o a H b. 0 0 . 8 ' O C Q 96 rt o •3 rt C Xt JJ O V> U M C AJ a a c Sf «M o H rt H § c 2 rt z - O r t O rt 3 rt J J 6 fN CO O fN 41 Ql - - • O > — rt 10 t-t rt a * J ^ « J=rt tn M J J 3 <n 3 U en o w u t-i-r* O r t > <M U ft «J • X! rt 0> rt O U. C XI rt > C M . o o t 0) £ ^ rt X ) J J J J J J > O r t - 5 § 1 .•rt a o •o JS x: <w H H U --J fr* fr-it t-» w CQ ca 3 Z Z z5£ M O t" 'SB! fr* rt -M fr* fr* OS 22 H fr* U. rt j c c c o * rt #3 t 3% u-i I -a J J J J 3 « o •o fr* u & K D J SS u u fr* M M U Z 5 3 ftSi M Z « rt CQ 10 C •• D => Q fr* O fr* rt rt i s i s c z — z U O r t e c u irt -rt Jtf o c- o o Z U C o — J J x< *» 8 z s » b. b. ) u u z o> J J J J fr* 3 3 rt O O C J fr* b. J< rt rt U o o : S"a:52fr. O O O J J v v n II II 97 u c P- M o u 1/1 rt «"*! rt J • > -rt « : Hb.MHb.MHb.< - C C U C C O S S t - H r t « J r t r t # 3 0 0 < EC K Cd U M CO W " D U O G U Cd K CC CC I M H H b. rt rt O CO ffl * o'o rtgg <M | .. .. 2 J J J J •J 3 3 •J O O Cd S o S i i i U K rt — O rt O « a a u H Cd u O Q Q ' o 8 * b. J J J J J 3 : 3 3 6 C 3 3 0 O H U. o> 0» J i Jri u u « «» « fr* b . U >.Z 0) OiCQ H J J rt J J J J • 3 3 . O 0 z o o o O 3 U U 5 e * cd a> c in •} tn T J oi rt en - - H « - fr* co m - fr- fr. H H M fr* fr* rt H fr* H fr* H M fr* MMUlMMIIlHHIBHHMfflBH (QCO COCO COCO S D CQ CO — ) O fr* fr* : Z Z D D z 4 M M O O rt 5 3 2*.<*S - H b . U H b . O H U . O H U . y O O U e e a x i x t a u u « u t a « u u « . M 3 « O T J H T J W « O 3 as - a H M - I M - M W Z Q 5 O 5 5 S OlO 55: 335. . 8886 J J J J J J J J • • 3 3 3 3 U J o o o o y fr* b. fr. b. O U I U I U U H : 01 o> & & co • l 8888 Is V V V V J J J J J J J J • • 3 3 3 3 * O O O O O H b. H b. Q Z & » D> &C0 3 3 o o H b. « W a o> J J J J 0 33c o o H U . - O O D U O 235 98 o •rt <-H J J o W O K C U & 3 § u y a> • H J J CD 9 -rt o a • " -H « C J J O H » D H 3 N U B •• r o -rt t 4 CD *J 5 J 3 H 4 u 3 3 U 3 M M •4 O H > tu CJ 5 H V lb C J 3 H > C M • CD O 1 a xz H H jj J J J J J J > U H CN H 3 fi TJ H CO M -4 « O H - - H - •* H CO CO M M C Q H H C Q M M C O H H M OQ co coca coco s o n H H H O O Z Z 3 2 Z S Z 2 D S Z Z M H O M M O M M O M M M O H CN C C C CN H h M h l h H H I x H tj - c c o c c o n c w M C N U <N •HH C -rt -H « H H I U U « - ~ >M I I I I I I I I is" i 2 K — ° H -C -rt _ 2Q 55 c . — P H i c o 5 c < •rt H H fa. —o W O N e ca C O H H HHJfi O 3 y 2 — o O o « H W O H O Q u c 5 c o — J J J J » J J %& 3 3 K H O o o y co 5 H fa. O C H CJ O J 4 CO 12 u >, z b> a»ai M 2 M H J J M " H i f Q 2 « C U a i 8 co • > « J co SB a n V V fa. fa. fa. • (N IN CJ CJ CJ cc;«ee o o o n n n v v v m J J ft H O H M ( V V C C CO a H ( w j < 2 3 o S N N U U O Z 99 X « * - - C H CN CN O *H iH h tu (Oil * »U) » - W 4 J - - W . . . « * ) - , > CJ - - u J J •• J C J i j e - H r-b.Xr-U.M-* H b . J c H b . J f - H H b . J i H b . J C - H > c c u e H H U N I N u c ( N C N U O O U C - H - H U W H U B CP w w e - H ww « w w e - H w w * w « « - H U U « O U O - H - H A A A A A A A A A A A A A A A A A A A A A A A A A j ( —' ii n (I n — it u u h ii ii n — u 11 n u u 11 « — u n n u u u n -5 Ck UOi U b UCj 2 jS M J J * Si M H U. O J J * SS M H Uu O J J CX • M H b> O * J H b t J i H H H b . j e j J J J J t - H H b.JC4JJJJ ( - H -t H b . JC -U J-> J< -H • • H C C O C C 0 H C C U 3 3 O C « H C C C J 3 3 0 C « H C C 0 3 3 U C CC-HHCfl-H £ £ - * H - H « 0 0 « - H Ct-rt-H «J O O B-H CC - H-HcgOO « - H o o •• o *• o - •• o j * o. — a. — Q, o. • -C H <N **1 « - I H - H M . . . -rt CQ — « — — — — S . .m —« • -m . .rn - -PI — — « -N -fr* .. .. UO m n> -rt . — —• — rim-trtr'i.rtNM-H — — — (N (N -rt <N t„ M fr* t* fr* fljf — — LO - *J n m U i i *J - - f c - — W — — W N N U n n U w U — — Cw — M ffl M M M O fr.h.JtWrtTJ *•** rt t . f c . J £ H k . * ! H 6 . J « - r * J < - - ^ - « rt h U. * H a n a n > 0 ^ - H u « c f i i- u. o c A U - H - H U - H H u n h u h L u c xi -rt -rt u - H m fr* u. n u i ( > H > o o « r t o e . o < « n v ) a i A i A « L > u « u u a - H o a. p. « t o z - e b Z Z Z • • - * > . n w rt f* rt O r t r t r t fr* W U . A A A A A A Jtf A A A A rt A A A A A A A A A A A A A A A A rt A A A A Z u Z O — n 1 1 1 1 11 c — « u 0 n a— i i a n o i i n H H i i N i i f i t i i i i i o a— 11 n 11 D Z Z fr* - u cw wo" " A * rto'Srt 2 z 2 w O n S H A < « u x M J J rt £ a tn w o C J J J r*s P* X • X j J j J ^ J j r t t t » * f * U . J < r t 4 J H U , J i i > U . J i H U . J i H 6 « ^ H 6 . ^ r t JJ fr- U . JC fr* O Z — M JJ O J *4 •• t « 3 3 U 0 C V fr* C C U C rtfr«rtrtUrtrtl>OOOrtrt U O O U E rt fr* rt rt U rt cj o X H k r t cj 2 2 a £ 0 0 < a * D r t h .-1 cc rt 0 rt x t « f t o - * w w * u j U j » 8 C j c j « ) C j a « r t xi cc a. o* 0 tn - & H O C C C - Z Z O O U O O O O O p x a : « r t - r t - r t — p b o Z u cw — .* cw . - mo . — n o , Z O O Z r t W M M C rt rt u cj cu u tn cn p « « a a a « o m u cn m 3 H o n a *» o w S l y £• o tn J J g g o o ~ a $ « <j\ J J M « rt . . . . . . . . . . . . p rt rt rt a cc o > . . . . ( - . . . . * - . FH H fr* fr* fr* ** & X 1 U O O f r * I fr*fr*Mfr*fr*MJjrtrtfr*fr*fr*MWWfr*rtfr* (-> P fr* u to rt M M C D C H M C Q S C Q C Q M H H O n O H B H • •» D» o t j to rt 0 m m - r t m c Q o f f l f f l m co _ CQ . . . . rtC Q W > K U C fr* fr* fr* fr* E? £ I* G " f r > H C r t > > l - •* - C 3 - * Z Z P 0 Z Z P 0 P P Z Z Z b ^ b b Z O Z fr* H H fr* fr* > « CC I I fr* fr* fr* fr* & « • . . J J J J H H O < J r t M O * J O O i - i C r t M 0 3 0 0 r t r t r t H ffl ffl H H X fr* fr* M JJ rt rt fr* fr*fr*rtrtfr* fr* fr* © r t 0 0 0 r t . O * J 03 03 OQ J J ** rt rt 03 3 a 03 rt rt rt 03 0) rt M M 3 Xl J J T J *o * " fr* fr* _ H O C CO ffl 0 ffl ffl ffl ffl ffl ffl M O 0 rt rt o , z g b z z > o cn c fr* fr* fr* fr* c w t o T J <-» rt o o rtfr*o M o o rt rtrtZZDODDZZZDOZZZ co -rt 0 0 t* V* «M « * M rt rt 0 J J 5 o w c M 1-1 O r t a Srt a rt rt rt rt rt o J J rt J J or t Q u a *» 0 0 rt J J 01 W • a t* W w Crt c U C U M J J Z a o J J T J « •• J J •• •• cc fr* —fr* u . j 4 9 f r * f e £ o f r * b j » ! o f r * c « . i < o f r * b . j < : w r t o fr* 0 t o 0 rt u c P s —rt rtUtnrtrtutnoouOrtrtuuoou>c p. z a r t - o ft o rt 3 ** P H ( v a 0 w w c w t o 0 a o * u o 0 r t K H a a H < u « j o o z — < 1 1 • • i - ' O Z — fr*u.«jj a rtrt O J J rtrtn o w o 1 1 1 > 1 1 » u o j i w u u - H O >> Cw U W C O l - J J C rt fr* 0- fr* Cw U 3 3 «J C M fr* — f r * b J < V f r * b . j * O f r * C b J C 0 r t O M T i a > - < X C C O S e C O O O T J r t I M rt * , — * • - * . u w o o u o r t r t u s - e u t o T j s o a 3 ° 9 fr* cc 0*0.0 tn tn 0 0 0 0 rt > > p • u S D o £ :. i s ; i i : : :5 S .. u a T> O O M 0 H W O hM fr* CC O a B . 0 t n U 0 U U 0 rt \> p Q u i s : : :  ; _  3 100 OI ^  H H H — — •— »-» «H -H i-i r-i -H O O -4 — —. «— — —. — O O -H O O -H O -H — —- — — U) — — W H H U f N f S U JJ JJ — — OJ 1/3 —' — V l O O U H H U i ' JJ — — Ot — — tfj - - in . - O O O t J J J U . J C H U . J C J i 5 - H - H H b k J C H b . J C H U . J f M JC -H - H H b. Jf. H b. H b. 2 H b. JC JC - H * • H U - H - H U H b . U H b . O C Xt • H ^ O ^ ^ O - H H U H U . O H U . U C Xt • H - H U - H - H O O O U - H - H U H b . U C CD n c u u « O u < U U »-< O 0 « 0 . « W W « W t O « O U » 0 0 « - H O a O . « W W a t O t O B O U c O O t J * - H -H «o en > A A A A A A A A A A A A -H A A A A A A A A A A A A A A A A -H A A A A A A A A A A A A A A A A I n H D U t t n B H a H t l H a— I I I t i l II 1 I I M I I U I Q.— D Q I I t i a t l H H B a U l l t l f l l l H ,. a. .. o, - H O -W O < - H - H O " H O < <H - H O ~< O LO W {J O JJ fi x o. to w o U JJ O X O. 01 W U O JJ b . J £ H b . j f H b . J C H b . J C - H JJ H b . j t f H b . X H b . J C H b . J C H b . J C - H J J H b . j C H b . X H b . J C H b . J C H b . J C - H - H U O O U - H - H U O O U C - H H - H - H U - H - H U 0 0 L>-H-H U O O U C - H H - H - H U - H - H U O O U - H - H U O O U C n a i A i A o u u a u u c i - H x t « e w f c « w w * w w « u o « t j o e - H x t K Q > o < e < o u ) a H W 0 O o e o u « - H •• o p - o p — « 6 . — CQ K -•H -H a a i 101 H M CO X CO — •• hi U •» O H H X H « H I) •• M w O M M CQ CO <0 CO - CQ M M M CO CO CO 1 O M H M H H H O H H co ea to 2 £ z z M O M M H H - H H H CQ CO H H •ess O H H H H C Xt rn <NJ XI H o XtXIXt C M H . H U . - H u - o n r * H X H C H - M — e c c U B H - O H W O M M M . « M X H X O X x x x H x u N u e u p u u u C S H H C O H O M VO e e *C H H * (J « CO H M M M X • c — OHM • » « « HCkHDuHCCHF^H H . r n H X l H O p X I X l X ) • H H H t v H C J UHOHfN cucxtc H M u c e c 3 W M M H ° H 0 , g W M M - C «H -H - | , . . - H M N C V M O M H a * « H H H H X M O H t N i e . c * H - C I I I c c c j M M M C N U H l n MMM X C X E X H 3 - xxx -OMUMUCJO o o o « a x « x e x « M « « « J 0 U U tn x - w - * - « i - x » - . . U k fa. fa, b Ubtbh. « M «<N .« • M « « « a Hh.Hb.Hb.X OHrN » C H C CN H H B - E E C U. M CM B O H H b H H H « M M O M •J • - . . 0 ) . . . H -H *H -H H H H - H H < N H < 0 H M H M M I H C N H H X H O H C N 0 C E C B H H E M C C B J M M M M O O W W H M M W W W W W W W W W W M W « H J X H B O B J «J M H fa. H t XI XI O C H H X H H O 1 O O * r A A A i 4 X X X X : u E c u 4 a tn a * o o -u ux M M " to to X H fa. X H H U XJ Xt O H H « J J M O O e H bu i 0 0 3 H ft* 2 u o o o fl X) XI <0 5 3 • HHb.UHU.OHb. c c a«<9XlXl« u u _ ge H H H M M M CO CQ CO Z 2 2 J J H Q , X • O H M — O H H M M co m 2 2 to ea co H to m • u X H : U H 4 « o O O r H U. X rt CN 0 o o * i i — H - - H - . . H H H , E - H M H H M H H M M H H H H O H M O H H O B I I D H co co ca co co co . . ca M M O H M O H M O O O H S 82 O H b. S 2 * i * J X 3Xt«OU<000(d-- « H - - H -H f-t M H H M H M M CO H H 00 M CQ CQ CQ CO CO 2 2 § 2 2 lb 2 H M O M M O H Hb.MHU.HH O O X H H X CN - C C U E E U C H H - M M - . H CQ CQ H M H to bom H O O 2 D 2 2 2 W O H M M fa. M O <N X H b. X C O H H O • H « o o «0 -102 C H b . C H U . C M « « M XI XI rt o c c u n c u • M M ( H H < JC f* fa. JC H fa. JC *a o o a o o « - - C H U . C H fc. C H U . w « -3MXIXIM i H M J l l M M J i M M j e c c u c e o c c o M - - CN - - CN - • C H h C H I x C H b . H «9 Q M X I X l M I N N J f N N J f N N X e c u c c u c e u t a rt b . JC K h JC H b . JC C Ut-tw-, u n c i O r taoooooa x ai WJ O CN CU H b J C H b . JC H fa. JC C C O r t r t O O M O rtrtaooaoo« H h. U O O W - J J U U JC 10 rt TJ U U U 10 C TJ OJ tO * > rt > A A A A A A — ii u u ii u n U 0, io aS e- b. « u jj J J jc J J rt a - t - 3 3 O « C 5) DC O 0 « T I r t M O O rt M (/) JJ JC JC JC rt B C U C 10 10 * rt 23. H b. JC rt •• H C C O C a; rt rt #3 rt o o jc a. H fa. C H b. C O O M rt rt rt JJ rt rt JC rt rt rt C C U C C U C C 5 H f r i b O JJ rt H b . J C J J J J J C r t • 3 H G C U 3 3 W C 0 S r t r t « O O « r t ^ H ^ r t U ,H . . w - - rt . . H H h H H I x H E H b . C « « C X > X ) C H h . « « XI - -JC H b, JC H U . J C r t r t J C O O J C rtrtJCrtrtjZrtrtjZ rtrtJCrtrtJCrtrtJC 0)to2Hh.2Hb.2 O O u E E u ^ r t U r t r t O r t r t u ^.^urtrtOrtrtu c c u c c o c c u S S i l M i l ^ y BB a to to a u u a u u « u u a u u f l u u < u u < M M »O M M B M M B M M A A A A A A A A A A A A A A A A A A A A A A J * A A A A A A A A A A A A A A . A A A A u „ A A I I I II — I I I I I I I I I X — H I I M I R R H I J« ~ B n n B B D K U O — « • • « * > • • • • JJ — • P U f Q, O b «M Q, JC O. O Qi 3 0 < C rt P* «" < C r t ( N < C rt CN k- < C r t f N HJrfJ S J J J J S ^ ^ S H U . S ^ S ..2fr,b.St>b.Sf.b1S " 2 Hu . j1frtb .SHb.S «ffc*3ss§£ft§ -fefe SSg , "SrtrtS^'S.'S'S- *S.5.5 8 « 8 3 3 8 S'S'S S ..£.5.5 833 833 8 52 - rt2 - rt2 ~ *2 - S2 103 - -vo - - in . ,m - - -r - - -ft • -m - - <N - - C N - - H .H ri *4 .HI ,4 H r-t —« O vo VD — mm — mm — ^  — «# ^  •— i~i cn — n n - n f i - N N — H H — H b U i * — — CO — — 10 J J CO — —'UI i ; CO — — CO J J — — W) CO J J —-— to — — CO J J O O X H Hb.XHb.X - H Hb.XHb.X - H H b . X H b . X - H Hb.XHb.X - H H fa. X H b. X - H <N CN U fi M H U W M U C b M C J M U U C M k U h h U e M w U M w U C W M U M M U C O o * - H to to <o to to « H to to a to to « H to to « to to <e H M H « to n M - H ti n 4 n n O - H A A A A X! A A A A A A A X A A A A A A A X A A A A A A A JS A A A A A A A ' X! A A A A A A A X! 11 n u n u - n n 11 11 1 11 n 0 — n n u o n n a y — H B n o n n a u - n n 1 n D n 1 u —- B B » it « H M O J J u J J J J * J J J H b. O J J '*> 5 M H h. O *> *" 5 M H b. O J J *« S H H fa. O J J * S§ M H fa. O J-> « 5§ M H L> O *> J J J J X - H H O X X J J J J X - H H b < X J J J J X - H H b. X J J J J X H H fa. X J J J J X H H b. X J J J J X H 3 3 U C " H C C U 3 3 U C - - H C C U 3 3 0 C " H C C C J 3 3 U C " H C C U 3 3 U C " H C C U 3 3 U C OOM-H C £ - H - H « J O O « - H CC-H-H400M-H « H H < 0 O O « H O S H H M O O M H « - H - H « 0 0 « - H vo o — m o ^ O 1*1 o ( N O H — Hfr — HDi — HO. — r-tO. — HO. — H H H H H H H to to n to 10 to - XI . ..H - <N r t . „ , - , <N - • H fa. H H . . - H ( i b , H * - H - C N «0 C B - - G H f a C h t x C X l X l C H fa. C a - - c H H IN H H M H b . H U [ N N H r i n H U H H M CN IN M Jj - 'NHk.HU - - fa. - - U JJ - « U. H H X H M X H - H .H X H X ,M *4 JC *4 ~i JC H fa. X N IN X H H fa. X H fa. X H H fa. X c c u c c o c c c o c c o c c c o c c o c a a y c c u c H M u H r-< u c r* i! H H 0 M M «J H H H « M M « H M H H H H O -H N N O H H <-4 fa, fa. « C J O « H fa. fa. « A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A — n t t t i f i f f U H « i 1 1 1 1 1 1 — 1 n 1 1 • > 1 ~ B i i « a « t t i i — • M n n a « • * - « H B £ J 2 X XI X! x: 0 0. ua. y a . 00. oa. u a « 3§ ' wHb.OJJ * 2 M H fa. O JJ « 2 H H fa. O * J «J 5 H H b i O J J , H h f a Q j J «X_ H H H b . X j J j J X H H H b > X J J J J X H ^ H H b . X J J J J X H H H b . X j J j J X H H H b. X J J J J X H H H fa. X 0 H C C U 3 3 0 C C H C C U 3 3 0 C C H C C O 3 3 O C « H C C U 3 3 U e « H C C U 3 3 0 C « H C C O CCHHCOOOMH 0 C H H « O O < H C C H H « 0 0 « H K-H-HBOOO-H O u H H S O O V H D C H H M ..g „ ..g „ ..g _ ..g „ ..g ~ ..g 01 « t » vn vo . 1-H H H H H H 104 A A A A A A A A A A A A A A A A A A A A A A A A A A A A A _ A A A A A A A A A ii xi — ti I» II II n u II J 3 - . I I i i n i u i JS — i o i i B • i X ! — n n i i u u i i D xt — H 11 « B « ti n X ! — n n u o o . o o u J J CU j j OI uo> * J Cu J J M h l k O u " 5 H ^ b O U H h h O u * 5 rt fr* b. O J J * 3§ , # M H U. O * J rt a H h > ; i j u j c - H a H l b X H D ^ - H a fr. h, JC J J J J J C - H « H u. J C J J J J JC rt « fr. b. JC « J J J JC rt n fr* b. C H C C U 3 3 U C f C C U 3 3 U C fr*CC033UG frjCCUSSUC f - C C 0 3 3 0 C £ j - C rt - K - H - H « O O « - H - - C C r t r t f l O O O r t • • C C r t r t B O O O r t " ( C r t r t * 3 0 0 * 3 r t . . « r t r t » 3 0 0 f l r t •- CC rt rt o o o o • o o — m a — *» a. — M O . — fN a. — . - to . — o o . rt rt rt rt rt rt (Q CQ U (0 *B f) A A A A A A A X ! A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A - II II II I D P It U ~ B B B B B M B i i | | i g i I J= — D H n H U U H £ " « « H P I I II £ - II I « II " « JJ V U V u P> «o. J J a. J J a J J o. J J e* X W H U . O J J « X HI H b. O J J rt X H H bu O JJ rt X M fH U. O J J rt 2 rt f- U. O J J rt X . , M fr* b. Q H f r - J C J J j J J C r t H b u J C J J J J J i r t « * fr* b. JC JJ J J i r t O H h . J < J J J J J C r t « fr* b. JC J J J J jc rt « fr* b. JC J J J J JC fr*CCO330C - f r * C C W 3 3 0 C fr*CCU33UC H C C U 3 P O C fcccy23yc H C C O 3 P O c c r t r t a o o a r t c C r t r t « o o « - H ' - c c r t r t d o o o r t • • c C r t r t « o o « r t ••cCrtrt#3oo«rt - - c C r t r t c o o e 2 ~ 22 ~ en 2 — co £ -> r- 2 — «2 rt rt rt rt rt to a a to to 105 S B * - O O M - -fr* t* fr* W M M ca ca ca c M M o C fr* fr* w •H M w ca — ca ea nz z 5 — 0 rt rt o fr* fr* M rt rt CQ CQ CO z z 5 rt w O fr* fr* — W W * J CQ CQ w w fr* fr* fr* w fr* fr* • rt w [ - c a ca» o o rt w rt O fr* fr* — O •• fr* O fr* fr* — fr* fr* ;* fr* — HHfr*rtfr*fr*MrtMWfr* W W fr* fr*fr*M j c a c a r t j j w w c a * J C Q C Q w co « M w ea a CQ «j CQ CQ n ca — m c co io *-O O W J J W W O J J O O W O O O W fr* fr* rt rt CQ CQ z z w o — O O W rt w rt t-T) n 8 H 01 k - fr* b. Jc -. rt rt O C Q. Cw « i rt Q.U 4 « O J J * U fr* fa. Cw C E t * a & J C o -i Cw O O O O i-* cw cw « t j e fr* fa. ; o o o HJ*-**-t t u o O C I J i o -(N J J I. u c -t JC o M O O tN • M Ji U >, w fr* b, >, 3 fr* b. O B fr* b. W fifr*fa.U)Mfr*fa.O w E B U m fr* fa. O O JC 3 r t r t J C 3 O O J C « r t r t J C # 3 r t r t J C 0 U ) M «N <N U W JC JC U W J i J C o o > > o o > > . o o . n WJ « rt cc u JJ JC « rt o > c O T J C9 W fr* fa. rt J J JC O O JC rt y c c o e •9 W W #3 rt I I 1 I I w fr* fa. o *J JC JJ JJ JC rt o 3 3 o a « O O « r t fr*b.Cfr*fa.Cfr*fa.C rt flaHCRHQCH - -fa. O O J C r t r t J C(Nr4JCfr * b . J C C C O C C O C C O r t r t O A A A A -< C C C rt * X fr* fa. rt fr* h. w fr* fa. w O j o o J C r t r t X M r * J C f r * b . J C H C C O C C O C C O rtrtO -2 . - © « -rt - »<N fr*h.Cfr*fa.efr*b.C XI XI w X) Xt W X) XI »-• - - u. O O J C r t r t J C N ( N J C f r * b . J C e e o e c o c c u N r t o W rt flrtrt Crtr t *3 fa. fa. «3 A A A i A A i < C C C M * X fr* b. M fr* b. rt fr* h. w O J O O J C ^ r t J C < N ( N J C f r * b . J J fr*ccoecoceo(N<Nu 106 M a M a " --S--2SS I w m iii J i i « i l i l i l J IS J i i i i i 8 l l I 1,111111 | I s ! ' 3 - S B * l l 5 5 5 5 1 5 3 1 1 " i 5 5 l "^ s l ! s | B Wnlli 116«» I i 5 s i s s l s 107 (SI . . M - - N - . O H k O H h O H b. P. * wo . x t .QQ. N N A ! N ( S J ; M ( N J « o o o o o o o o o a . a t < s a * o < « o . o . « A A A . A A I M 0> O < C «"* M *M £ M o o H l u J t H U i J c H h i J i •• H G C U H M U <N fN O ttH-HCOOOflOOM X o . , O H b. M o o to - J-I y y X to - H TJ M u y M c TJ a ca <o > > A A A A A A ' H 0 D It P H 0 X H b. «fl 4 * j J J x u -• H 3 3 U * I CC o O « TJ -JC Jt Jf-fi C O C a a « -j i — n n n n h l u J i * • H C C O ( H b. O - - Je -H « OOiHtuV) - -< <H t* AC r* Oi M b* b. Ji O O U J C X U H M U o . a . « c a c o a « < a e A A A A i A A . ' I i I ii n u : o. o H J J 'SSHb,l5HU.MHU . cB OOJCMMJCJJJJJC • H c c o c c y j g o CC-H-H « J ^ ^ H | « o O cfl - -2 - .a H h. 6^  - -ton Hb.jlHb.JCCNCNJCHb.JC'? (N CN O m m y >, > y M M U >, a « « x t x i duo « w w « o co X < to 2 Jtf Jc Jf H O H H b. U H b. O H b, O H U. UO MC£ « « < a J 3 X t < 9 U O«taD ) « u a o •o cw - O H b. C h. CL M M — M JC JC JC o y c c y O. K CO CO <0 & S o ' « . .a'i.'ku - - B H V S ^"y^Ss'sy as2e%2s%S a'siasaSo" ! SSSKCjlcS^sllls 33SSSS33S SSSSCSSBS SS8SS83S i S S i i o - J » { 5 S S 5 J » i ! t 5 { J 5 ^ - J i t S S S S S S ^ - S i i S S S S S S ^ - i J S i S S S S 1 . . J P i a H H J H J - L S H J H J ^ L S , J H J - L L J H . 108 fa. Ji! H fa. rt rt U O J { N U C « « « #3 « rt A A A A A A U II H U U It H H I x O U b. J C J J *j J C rt C W 3 3 U C rt a O O * rt rt M f> rt . - 2 « - 2 J J H* fa* H b. (J* J J H tb Cw - -. cu J J f- fa- O*1 H 6u <j H f a . S H f a . 2 r t «H «—t J C o i <N J C - H m ro * H fa. JC rt ? ^ •* T* •* ja xi « xi J J « rt o u »s o u « rt cw cw « cw cw «•** o u * o O c A A A A A' A A ' H D H n U N I I A A A A A A A • H R D H tl B II . x: JQ. u cw J £ rt H fa. o J J « 3§ rt H fa. o J J 4 H fa. J C J J J J J C rt rt H fa. M J J J J J C rt S H C C U 3 S U C C H C C U 3 3 0 C f X r t r t C O O C r t CC rt rt «3 O O «rt . O •• O 0. — Cw A A A A A A A — fltiuHdnn X! u cu •J £ w H fa. O JJ rt H b > ^ J J J J J C r t B H C C 0 3 3 0 C CC rtrtCOO«rt .. o cw JZ — u J J CM •3 H fa. C _ M JCrt rt JC rt > >, u > > y c O U « U CJ Art A A A A A A A  l i n U D H D P t/) CO B W l f l « rt A A A A A A A — u i i u p n u n cw X M H fa. O JJ rt£ w H fa. O JJ H b . J C J J j J J C r t « H f a . J C J J j J J C r t H C C U 3 3 U B H C C U 3 3 U C e C r t r t f l O O A r t '-CCrtrtfUOOArt O O 0. — rt 0. B JQ m rt IN rtfS . « » r t rt » " O l ^ - > - - O . - O . . J C - - J C rt I N H fa. >i > • >» . H & . 0 - - 0 fa, 6 H fa. P . H fa, P« J J H f a . c n H b . C 0 J J - - Xj - •• X) J J B 6 (J H fa. G J J X l X I C W H b . f i . J J £jZ rt rt JC r j fN J i rt rtrtJCMINJCrt H f a . 2 H b . 2 r t rt rt JC rt T-H JC rt . « <N JC 1-J 1-J JC rt H o o o o o o c J C J C O J C J C O C H H U I N I S U C >> y >,> o c 5 £ 2.5 -t> #a cw cw « cw cw «3 rt (fltoctotoart xi xi * Xi Xi « rt OO uOO « - H cw cw « cw cw * rt a A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A II U — H f l P P U P P — H P H H U H H — I II 0 H II U I — B B P B O P P — B B B B B B B -""~B X! X! X! X! JZ JZ u cw u cw CJ cw u cw ua. o cw C J M jS rt H fa. O J J «3§ M H b- O J J < 1 § M H b. O J J ifl 3 § M H fa. Q J J * * , « . M . t * t , , 9 * > fa. JC rtHhiJCJJjJjcrt rt H fa. JC * J J J JC rt rt H b . J C * J J j S r t rt H fa. Jc J J J J 5 rt rtHfcJCjJxJJCrt rt H 88 • B - S - g S g g S - S " S r t r t S o g S ^ "£-5.5 8 g g 8-5 - S ^ - S S § g * S 5 ^ 8 g g 8 5 " £ . 5 ^ -8 ^ "2 ^ -2 ~ "2 - "2 ~ "2 . 109 1 -A »! « M 3 J J u 2 J J U O no t j J J H fa. X -rt N M U C CJ ( J « -rt cn a* 3d H u H fa. JC -rt H C E U G C * CC -rt -rt « - H u o j c a. o o JC W J S S?o"J w cn a * u 5 X M l H fa. J C -H E C U f JC « - . CO O J C a. O O -rt -— — P . - X J H b . X « -H -d §2$ « J J H u. x t n - r tT j > > O « B TJ nd, Cyi c< X • • C H b . IO X X - 4 B B Ck J J CO tO X - 4 - H - H U C CM Ch «J > -rt > A A A A A A u n U H H U H fa. a J J J J J J JC J J -rt a o u a > - H > O A A A A A A k — B « U W U « tn a " SHU. M J J fi J J J J JC J J -rt OJ for Pi a Cb Ot <0 -rt X A A A A C — H B H U tn bi ** X M J J H b . X -rt 3 3 O * C 0) O O * T J - r t h • H H 3 3 0 « B 0 £ t g O O « TJ-r t w U Oi — u Sinks H C C O C -rt CK - » -rt «J -rt Q. O x a. c i = 6« - fa. X -rt H > U B J CJ « -rt s§ w J J H b . X -rt •rt H B C O C H fa. O O u u a n 3 3 o oc o o o. o v a. H H -M M H CQ CO M H H -M M H CO CQ W J — CQ J J H H 58883 H H M — M M CO C A CO H H M M I - (0 CO ( .&.. .-rt H I <0 M I CQ B : o z M CO CO M M M gg H H E M M r ( D O G z z s C D Z Z 2 •rt O M M M X - X J U k U l a o * * H fa. 10 o o x X X o co to a & >, & H fa. > 3 S5S5XJ3HH^S H b . f i to tOJ CO CP I CC CC I 4 O T J tO : u •o n 82 S G « « -rt ^ ^ — C 82 I X X U B « t o fa. «U fa. b . b . O O —t CJ J J H fa. X - » 4 H rH O C ( J CJ A -rt - H b* X -rt H E B O C 4 06-rt-rt C3 -rt *2 : CO CO W CO CO w 111 — — o - - © - «O - »rt — • — > < o o M O O J t H H > O O U O -— — W 6— — J J J H U . D J . I J -S h, JC H U . JC H b. U O ) « JC rt TJ m 2 o > i > , u > . > . « J « « u cp n — I U O C U O CfJ w 0 t, A A , A A A A A H u n n u H M H n K K « r t > > A A A A A H b. rt rt cw cw W CW C H U. JC J r t r t U a cw cw « H H a — — O IN IN H Ck O. 4rt(NfMt>*JC<HrtJCr P. &J< H U . X H U . J C H U . J C H U . J C H U . J C H U, J( H h. JC H O O U rt rt UrH<H U <N IN O IN IN U JC JC U JC JC O > >i O > cw cw 0 u u « o o 0 o u • o u 0 w w 0 cn « • s o u 0 u — >-rt -rt o — JC H U U. U m « > #3 0) fl C rt TJ W J CO n 8 rt > > J C > H b. > 0 H U. U I H Ck 0 8 E 6 H U. K JJ _ O O J C r t r t J C r t r t J C n 0> J C rt TJ I J C J C U > I > , U >i>ua>»o cp ( JJ H rt CC ja o 01 cw u, - J J J C m rt T ) U H C O * > - H 5 J C J J - H a U A c 0 0 TJ rt H U - fa. W J o u. M JC I CW Q u cw . u. a J J J J J jc J J * H a J 3 u 0 c • ) O 0 TJrt M U U I x U U JC m n u W W II 5w H U . WO J J J J J C a n 3 s u o cc o o 0 %2 « rt TJ « C TJ > rt > 0 JJ JJ rt 0. 0 C 0 •Ort U H U . oi O O u. U U J C m oi O m rt i 0 C l > rt ; • H B » 0 D a » • f—I . - O — —• — - -rt - «© - -rt - - O - -rt — — — — — — O O fj, ^ . ^ - — — — — — — — — — — — — — HH-HOO*l O r t r t r t O O r t r t r t l N O O W r t r t J C — — a. — — cw HCwcw u (j o ( j - _ — LO H U . J C H U . J C a ajc H U . J C H U . J C H U . J C H U . J C H U . J C rt rt (Jrtrt U O 0 UrMrM V UfNIN U(N(M UJCJC U a c w 0 C w c w 0 C w c w 0 ( j ( j 0 U ( j 0 C j < j ( u u f l v i v i c A A A A A A A A A A A A A A A A A A A A A A A A ' H O P D B K n H U I i n n U I I I I * l l « H D t l R I I I I X H 3 3 U i > CC 0 0 0 7 ;2 .. < rt rt O rt rt r i CJ X C w H b . C W H U . C w H b . U H U . U H U . U H U . O H O H U . J C E G J C Q , U S rtrtJC 0 0 J C r t r t JC O O J i r t 4J |-i rt rt U -ri ~ri U O O V '-i r-* V r-l r-i O N IM U <N (N UJC •HCCCWCW 0 Cw CW 0 Cu CW 0 CJ U 0 U U 0 U U 0 U U 0 H rt 52 JC U — *S 2 112 — > m ro a U A I A U * in W D U O « u u ri(M«»J<nn>i*. - , _ — u w tn 6 X H b . i t 4 ' " * i bu U to to JC-H TJ to • < > < « C D a > U C T J t O CC CC « > > . A A A A A U U H H U n U U H H U O D . A A A M A A A A A A • II n II • I (N JC X >H b. >i CD b U r i k l f l H I u l A H k U S fi O H b. CC 4J _ OJC-H-HJC O OJtf-4-HJC-rtHJC to W JC H T) 10 (N O JC JC U X J i U > > I O > > I U O « U CO ID H bu JC H I 4J —I ~ l U -H --H Oi Cu 0 Cu I XI CQ A A A A . K — H 11 H II • H pS h C Xt o - b. O . 5 G JC H * H U u Cu eg h b f i . H l i . U r ' b i U H k U H k U H I i . i a H l u V l r ' h . „ a d JC -H -H JC O OJC-rtHJC O OJC-H-HJC O O JC -H -H JC -H O O U H H U H H UCNCNUCNCNOJCJC U JC JC U >, > U > o. p. a u u I I L I U o u u a u u «</)« « « « « u u « o JC to > U CO C J « cc b. CC CO JC 9 C J ' CC « — — a. ~ ~ a. H bu JC H tu JC -H -rt U -H U a. a. o o> a. « A A i I N - I 2 2 & M « H fJnHpinnricioinnjJN r - u . * a a j c f-•  -H U O O U »H . .  o. o. a o A A A A A A A bu JC H CJ « u A A A h b i J CN I N i C J C J i H b . ' CN CN ; u cj - . < N - -m - -> f N r (NCNJCnrl > I N C N O yj (j J( H {i Hb-JtHbuJCHb. O to I JCJC U >>, U >i >. K 9 ( w w « 0 0 « O o cc c ( • H TJ 0) J C T J to O H > > I A A A A A A A A A A A A I H b . J -H -H I Oi Oi I . H b . O . t a ax ) o o u ICQ. e CJ CJ (0 CJ CJ d I N CN ( u u < u ( J H b D J C - H -1 U JI J 3 O JC -H H JC H b . >» E G U H - H J C ca H TJ •» C T J W H > > „ . ^ . . co —^ —^ ~ - . ^ . - m - -— — — — m m U —- — — — o. — o . H u. a . c j u— — o — H b . J C H b . J C Q, O.JC H b . J C H b . J C H b . J C H •W -H CJ -H H U O O U H M Uf-IM UCNCN UCN o . o . a O i O . « o . o > « t J U « c j t j n c j C j a c j A A A A A A A A A A A A A . A A A A A a . 6 a H o H • - H - H O M H CN X O, H b . O . H b . a . H b . O H b . C J H b . C J H 1 H b u J C f l B J C a Q.JC H H J C O O J C H - H J C O JH-H-rf U - H ' H l> O O O H H U r t H O N N UCN - - c a o . « o . o . « j o . c u « c j u « C J C J * c j o « c j 113 V> (0 rt CJ H fa. JC O C J 0 A A A ~ > v o p - i - r 4 W 3 * o t N t — r - J C » o v D J c r - r - > r «> *o u — U o W w — — 6 JC H H fa. JC H b. JC ' * " * - * - ' ' ' ' • — <N I N ve+— •• O o « u « b . J C H f e J C H b , J C H h . J C H h . U to 4(M U JC JC U J C J C U > > > U > i > i « 3 0 ; u f l n u i < u w < C u < u u cc rt T I « e T J o • H > > A A A A A A i H D II II 11 H II A A - . A A A A A A 11 n I ii ii i n n i a i i ii B N H II B fl e- fa. u o OJC f-irA U CJ CJ 0 I N <N JC JC bj > O H b . O H b . t r j H h . t i i H b . 0 B B G H JC O O JC rt rt JC O O J C r t r t J C - H r t J C to H b. rt rt , CN CN _ . . . . _ _ _ _ rt T J tO C T J to rt > > - r - t- c- u * r t H fa. t - J C r- r- J C eo o M M JC H fa. JC U M J C r t r t J C H b . J C r t r t J C H b . J C r t r t J C H b . J C H f o . J C E -rt rt U rt -rt U D) 10 U rt rt V rH r-i U CN CN U CN CN U J C J C U J C J C U > | > U ) p. Cb fjCBi 0 »M «M t U U A U U fl U U fl U O fl W W fl W W n u O D C A A A - A A A i A A A A A A A A A A A A A A A A A A , n n n i i H n n i i H n i i H i i i i a i i i i n rt 0 rt rt I N I N J C bO.Hb.b.Hb.CjHb'tJHb.UHb.UHb.WHb. g J C a & J C -n -n x o ojertrtjc o ojertrtje o o H U O O U rt rt O rt rt U CN CN U CN CN U J C J C U J C J C 1 . 0 0 . 0 . « u u « u u < u u < u u c n n « n n w H fa. JC rt rt u > > « Go a 1 JC rt ' 8 & - m rt T J n C T J w • H > > rt T J M § . -to . - m m m u - »w> - - tn - -<o - - m - .*© - - m - -w> -_ — — — — u — — — ~~ — — > m m to w t o r t i n m r t H h . t o t o w a r t i n i n r t v s w n t n i n r i i o t o j c i n i n j c t o t o >iin in O — — 0 -— — O. — — 0 . U Ufa. O CJ O U W W U JC H fa. CC JJ -H b . J C H b . J C U M J C H b . J C H b . J f H b . J C H b . J C H b . J C H h . J C H b . J C H b . U U HJCrtTJ to j u-rtrt u ra « u -< ortrt U C N I N U C N C N U J C J C U J C J C u > >i o >, > « c u o u C T J ra 4 e . o . 0 C w e w « w w 0 u O 0 U O 0 O O « u o * w w * w w « O o * O O os cc 0 •*< > > 9 A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A I I A A A A A A 9 — M I I I 11 • n 1 P n « 11 a 1 1 1 • 1 D « 1 D 1 1 0 it 11 n • D B i B 0. H Q - H O r t O r t O r t r t 0 . <t ~4 5 0 rt rt CN CN J C J C > , H f a . > i 0 1 H fa. J C E B J C ft ftJC -rt rt J C 0 O J C r t r t J C O O J C r t r t J C 0 O J C r t r t J C r t r t J C to to J C rt TJ O J C r t r t U r t r t U O O U rt rt O r t r t U CN I N U CN CN U J C JC U J C J C U » U » l ) 0 0 U C TJ to 4 C C 0 - O . 0 0 . 0 . A a. a. 0 u < J D U U « U U 0 U ( J « i a u ) c u i f l « u O 0 0 0 0 cc cc 0 - M > > is. - - r- - - I O V 3 V 3 U • M — r ^ r > r t i o w } r t H h . « r» — — 0. Ch U Ufa. — H b . J C H b . J C 14 h* JC H rt rt U rt rt U tO CO U rt 0. Cb 0 a. Q. 0 <M «M 0 C J A A A A A A A A A A " B B B B B B B B B B  b. 5c rt U fj 0 A A \D H b. JC E £ JC ft ft JC rt -Ut*~r*-4 -A O 0 O U rt » -H cc 0. cw 0 O . f i . « O . D . « U ( 114 T J « T J to > > TJ to TJ to > > • - U H U . U H b . t J H b . X <t) « X XI XI X H P ! U H H U H H U u u e u u <ouu • A A A A A A A A A — I 1 I I I » I H I X u o. o< c H i u g M o o H b . J C H b . X H b . J C • • H C G U H M O C N C N U K - H H A O O C O O t X o <U O. « - - « . . «3 - .HHb.HHb.fH H fc. u « a u j a x i u < a « x e « x « « x M M U H H U H H U u u e u u o o u a > A A , , A A X DC O * O. n n o u n o n H U. X H U . X H U , X C C U H H U C N C N U H H a o o a o o * ) a - • a n b. H -. - t o H b . t > i e « U i J -H b . X M ti) X « «0 X H to T J a a o a a u H H u c to T J H M a t s 1 N ( 0 U U * 3 H > > X H b . H -- tfl £i J3 U u -V A A A A A A O — H U B B U B to H O. o cc t to O H a . i A A A A A H h» Cfl & o " S L „ . . . _ . . i o t / ) < t o t n « u U 0 H > > A A A A A A A A A A A A - B n n n a B B B B O D t i O H H b . X H b . X H b . X H CO TJ H - 4 U O O U H H U C « TJ O CC D. (W a (A 1 0 «J U U « H > > to o H O . H U H X m u u * X H u u - H b . XI H H M H ca ca z z « TJ n t n x H b> X o a a OH N N C U u. u o x H O u a H b . U <u O O X H NN U B U U « H T J CO 1 ? -5 82 . . . H H H - H H - H M M M H M M H 4 M C Q C Q C 0 M C Q C 0 M Q CQ CO CQ H H H H H E Z D D 3 Z D D Z H M O O O M O O H C H CN M O O - U . X H b . X H U . X i C O H H U M M O H H « 0 0 « 0 0 « U U XI 10 x -H a . U U N • H a t s x x U CJ o o X - X «J «0 u u. u « «J «J . . 0 b . b . -H -xi n b . U b . H 0, H NUN U - O U U U U N ggsgg H b. « - - a *J J H b. N -to tn X n to X H - U - - U i U . X H U . X -H U CN CN O I U fl u u « -A A A A A A A A A A i < H h. a a H H X u U j N H b . U H t o t O X H b . X O O X O O X - . H U CN CN U I u a u u « -1 1 6 o o o O O O -a. o cn J J rt (j j j u m o !X J J 3 0 5 J J B TJ n rt 0 </> H m o a n h H H z z z z n n S M rt M rt z z z 0, a n >* — O O ft 0 J J _ H cw co N . J rt TJ oi M H G TJ w H CC rt > > 5 2 : : : : cc cc ggg u u u - V . g c c c c p c c c c p c c c c p O O P O O H O O H H H M H H M H H M H H M M M H H H H H H O H H O H H O H H O O I Q H H H H OQOQ B Q O CQ 03 CD CQ CQOQCQCQ z z 5 z z £ z z 5 z z 5 £ 5 z z z z M M O M M O M M O M M O O O M M M M O O Q . H b. 0 0 - H Ch Cw H fa. CO N J J J J 4 H b. CC 4J & Q.JC ft ftJC H b. JC n 9i jc n w JC rt T) » O U O O U f t f t U 0 0 U 0 0 U C T I m : cc cw cw 0 t f l i n 0 N M C r t J « c c e C 0 r t > > : 3 5 J 8 2 t" M H H M CQ CO M CQ CQ 2 S S 2 rt O O rt Z — H fa. JJ 2 JC U JJ rt H U 3 3 C • Z CC 0 O O rt -H - -O H h Z CC o o CJ cw JC H <J c 0 rt fa. rt CJ c c -rt-< ~ Q ggg-b u o cc -I I I O CQ H H H W CQ 0 ft ft M tl O O 0 « 2 CW CO CC CJ jc 2 2 ft 0 U O U N 0 « 0 JC • U b< . - - 0 JJ Cu U. U. Id ft a m - 0 O O » U. J CW CO CC ft N -. . . H Ht-f- - JJ J J J g g CJ CJ O O CJ rt rt rt M rt CO to to CO ( 0 U . . 0 - - r t fN JC - * 0 • O H fa. CW H fa. O - - O - - 10 H b. CC JJ -rt ft ftJC X l X l J C H b . J C H b . J C U cu 2 rt TJ B Xt O O U r t r t U ( N r N U J C J C U 0 0 U C T } n U C W b 0 U C J 0 ( J U 0 C t j C O 0 C C C C 0 r t > > , A A A A A AA A A.A A A i A A A A u n a n D u > < O rt Ct JC o ( i H U . U H b . O H b . O H b . W H b . C C J J r , n w - . - . ^ _ . _ . j ^ r t r t j C 0 m 2 r t i O aftJCrtrtJCrtrtJCrtrtJCWeiJSrt'gw O H O O U r t r t U t N t N t J J C J C U O O U C T J B rtCCCWCW0OO0OO0CnCO0CCCC0rt>> • P 9 117 fa. tn u O.X. - H O U C W (0 H J J J C -4 3 o n O «9 -4 m n OJ — — O a ax-H o o u c tn i n « H A A A A £ H fa. J J m J J J J J C H an a a o c o et o o * H tn o o o> m b. o« J J ew o* «j - H h — It H II u u Ch '" S H fa. JJ O JJ JJ JC H an 3 3 o c o cc o o a - H a. o U Ch f> fa. CM J J &&1S-S Ch a. * - H " SS H fa. J J r-l JJ JJ JC H at* 3 3 u c O CC O O «J * H 0. o U Ch H fa. Ch J J a ajc H o o o c Ch o. 1 - H c O A A A A b - ii ll I ii to Ch " 3S H u. J J <N J J J j J C - 4 an 3 3 u c o cc o o « -< Ch O O Ch o H fa. 0. J J Ch Ch « H A A A A C l H 3 3 U B O CC O O «J -4 Ch O U f a O O 01 Cp H fa. CC J J to ta J C H CD » O B CC CC 1 -A SS M JJ O H fa, JC H m h C C U C f- fa. CC JJ (0 tO JC -4 v e o c cc cc * - H H H fa. JC -A to H G C O B 0) CC - H - H « H CC O JC Ch H fa. O JJ JJ j J to to -oo a — — tsl JJ H fa. JC - 4 a a u c A A A A «-< i—i a N JJ H fa. JC - H a a o E N tsl * -*4 M I N a — — N JJ e* fa. J C -4 a a u B H fa. a a M JJ JC-4 U B a - H t- fa. tn J J a ajc-4 o o o G tn to A A A A H fa, tn J J a ajc-H o o u c w w « - H A A A A S H fa. *> JJ JJ JC - H to H 3 3 O C B K O O O - H o 2 10 Ch g t- fa. J J ' J J J J JC -4 O r* 3 3 O C act o o e-4 e s • I H b . *J JJ JJ JC H I N H 3 3 O C ace o o *-4 U 2 ace ( e s J j i - H 3 O G 3 B-H 5 H fa. jJ O JJ JJ JC -4 an s 3 o G o cc o o n -H w p O th ' " 3§ H fa. JJ <-4 JJ JJ JC -A at- 3 3 O c O K O O « H w p O th -o « o "52 118 •3 - - a -J t-i U. CC JJ -x u n jc rt T J to o tv i> u C *0 w a cc K a r t > > A A A A A A A .-J. H fa. OS J J jc w tn jc rt T) n O « a> y c TJ W « K K a r t > > CN CN I H fa. e H — fl fl U D I f- ti. J 0 {- E E I 0) CC rt rt l 52 H — H tt II II m E-< l 0 CC •* 32 rt J-> fa. J C rt B U B 4 ha CC 4 o tn 2 -4 - i i n n CO H I CD DC f 32 •n in H cZ S i * n H B i tn H c O B -32 rt J J It J C rt s u c WO VO CO (0 VI J C rt © c u e cc cc a r t aS H «j t£> H b. J C rt 10 CH B B U C e cc rt rt a r t 32 : !%33 I 0 U B "3 to H C 0 CC rt 32 rt J J b. J C rt c u e H b. a H b. cn cwo. a co tn a N N a J <-3 A A A A A i A A A A A P< o o a n b. X H b. O. H b. CO N t) W & Q>JC a a j C H b . j c m u H o o u o o u a a u a a •• os cw a. a co w a N N a ,o 2 119 •0 * Jj 0) s — I N c i a CN E a> *J 3 b c — o U. X 4 O J J n xi * rt c o rt o> J J e tn o i l rt C C O) « V) CD JJ JJ E m » 0 rtrt O G JC J J -M 0 ) O to i a a : o o I u H n <u <u SSrr <M J J J J rt 3 3 J J J J O O O JJ < < o o o JJ r i C C 5. t C JJ rt 9 ; J J J J M M 8 5 5 0 X) to 4 u M jc 3 «J I M <M U U rt 3 0 0 I O O I I - . M 01 JJ «u O U 0 J O O 0 * rt ) 0 > Ot 0 > 0 > -O 9 9 9 9 B B B B B 3 3 C C C C 1 0 B| to to to to — > rt « ™ O JJ rt XI « rt 0 4 1 rt * J JJ * M (0 rt O M CO JJ X) u JJ JJ rt X) » to «w I 0 J J « J J to j rt a o r t CO « rt U rt JJ 0 4 0 rt J J JC a> u to I 3- IM rt O JJ «4 a> JJ rt «3 JJ JJ rt (SO rt (J — CO U X c o T J r t rt JJ o a > N -O JJ c to a> rt c o a a o c to to > > e o a> c* at o» o fN CN JJ JJ o o e s « o o e « M « o < rt J J J CO J J 0 0 rt r> x : to J J J rt rt H 0 rt <M 0 M J J JJ to 1 8 8 8 ° i ' U U I M 0 ' i *u J J <w — CXI XI £ oi n ; CO 0 1 CO rt -rt « j j - r g x i (9 JJ JJ * J 3 3 O O M JJ *M JJ o> o> • • - 0 XJ XI t I IU iJ 1*4 JC JC I O O O U U K ' i 0 xi J5 0 0 O J H a ot o OI OI u u o 0 o 0 § § rt rt c c o i W ~ 0 0 JJ E < rt U tJ 0 11111 = c c c c c n to 0 co to O O n fi -u « <• Q> 9 ) at <N (N CN CN JJ JJ JJ JJ n o o 0 o J J J J J J u o c rt rt rt rt (N CN JJ JJ O O JJ JJ t2 fna from t from t from t from t Jj JJ fi e II O O M Vt O <M <M Lt : cf tl is st is sf is ct is cf :2 fnam is ot is of c u . . . . 3 J J J J J J J J <M 3 3 3 3 rt 0 O 0 O O 0 JJ "JJ JJ UJ C JJ M W U O O 0 o> o> o> o> rt • • • • mal unit )t of tl t '"gtoufi 1 "gfout•) O 0 9 0 9 0 «« 0 c c c c Eunctic (fname' (fname' 9 Jj' * -0 0 •O W 0 0 J J — — TJ 9 c m 0 JJ 9 *». rt 120 -v. rt O 0 JJ JJ rt JJ O. XI JJ E c o O 0 M JJ JJ I M U TJ Ort 9 Q. JC 9 E O C rt 0 JJ JJ « - O rt c c O — TJ 9 • M rt «J 0 JC 3 ) 9 > -II — — f TJ J3 < C * 9 ' m i JJ JC c Pi C w 0 rt — H 0 —• 9 U •• JS O O JJ t*J JJ rt e e M *w JJ O O * J M M rt 0 I M I M 9 JC C G V 0 JJHJ O 0 TJ M M TJ 0 rt CO tO 0 rt JC GO ~ rt 0 0 . . • rt »M JJ «M 9 JC 4 U tt Ot C U JJ 0 9 O 0 0 JJ h M TJ 0 > TJ M • • • • < < < < JJ rt 9 0 0 0 3-S I § 11 rt C c c c 9 0 0 0 0 0 C* JJ — — e o w o o 0 3 O 9 0 M C O w U — C 9 0 § 4 rt 0 JC 0 . o 9 4 JC JJ C 9 rt 0 — — I N J J I N CN CN J J It J J J J o J J o 9 O O J J C rt rt J J Cl J J J J E CN e e £ 8 J J O O <n u M M *M rt * M I M 0 J J J J 9 J J »w 4 C 0 0 1 0>TJ O 0 J J J J 0 • TJ 3 3 J J 0 O o 0 c • M J J «M TJ O O O O ) 0>TJ 3 rj i § 1 § O U G G G G to 0 0 0 U 0 0 J J — — — — J J 0 4 0 J J 4 rt » TJ J J rt — a> J J x : • CO JJ J J 0 9 3 >i J J C O rt 0 9 J J rt TJ rt Ot 4 • u c i < . rt O 0 J J U rt B 4 «TJ 3 S I C J J J J CO J J 0 0 — 3 0 rt — 10 J u 01 3 « 6 a in a « «AXt O d CM X ! • C « H Q 5 JC to u CJ *M o u i 3 « « « TJ TJ CD H O l l v> O O e CN » « o u C B C H H g cp — A J J < B « © u a 3 3 U J J « CO M 5 3? to to J J fl O J J J J (fl c , 1 5 fl • O M J J X ! «•* H H >, a H J C a H h J J H l i 3 O XI cp u J J J J co » X S O J J 01 TJ - H C C H " c o u-O I •3 u ; J I H O O •n « a xi a a J J J J c O H H H J J H XI T J H W H T J » A > 0) 6 O f l - H h C > o a a £ CO J J > > T J X ! XI TJ fl b. C0-H 3t > l- * > O ai e o o a u * J -01 j J CO > CJ J3 C V* « J J H B A X i -O Um J J «i u »M * J a B V U U H H C H W -H a 10 - H X i wx: X i H ~ -o co cp a , ~ * J J to J J u u — • e * cp o • o > , J J a 5 u o J C J J CD M Q , O H U C H X i 3 H X I M CO • T J J C CN I T J A H . -< to T J 9 oo e -© to T J H a B X i « — • C r « O an — -H U 1 • M l/ o o B CN J J J J « J J CN E « S •o e — J J H T J CN 2 S E JJ « JJ Tj CN — oo — TJ J J S U U r> M A 3 UJ. U J CN J J — iH tO b. J J J J H h b i H ^ j J k S to co J J bu >iZ H H b> r-t O — bu bu J J bu b. bu tic: G CO fl < 1 J J >iJ3 C O CO CP O U JZ > H J J CD © > > J3 B oi O H 01-H X -^N.-."^ >^s.-v"V^ . CP CP O to c B H a X ! J J H H 3 to jj fl J J U J m j c § C CO CO toe t> O <U S M - H T J j J ^ C C T J B I t O 3 VJ CP O O «J H O f ttl J J J J O U J U C O C P J J C O C O C C - H J S X ! U, r-i r-i - H a T J J J J J »J co X ! I to CP J C o c TJ TJ U J J 1. C T J O « T « fl «M M ( A b b . X ! U CO X ! x: o o O JJ TJ TJ O O • • jj fl TJ E JJ JJ • • H fi fl A A < < 3 « J < W I U H H CD CD - I I I fl A ~ " « e • — J C o < H U U CP X ! o UJ e — TJ 10 TJ H CN H O J J Jm H U H X I H a J J 0>b. bu o b. JC H JZ c o JC co b. o © § .SSI CO H H J J J= J J b. b. b. UJZJZJZ o o o o U J J J J J J J A A A «M fl C H III-U CN CN H CO J J J J 6 O H H H H J J J J O z CD bu bu w J J bu b. b. u jz x; x: o o o o H J J J J J J J •3 a « • H H H J J 4 *0 •3 I I t | H - I I « _ _ _) J J J J J J I » CP CP O CO CO I cn co co a to to -i i n e ; J J J J A J I to co r I t o - ^ Si 5$ u o a - .3 fl J J a *M CO 121 - J S rt — • rt J C CP M * I w Ot CO 4 G U i art rt u I J J I M tP O r t J J I J J #3 CP M > J 5 - H I r> J J pt rt b i <D I CP M I J J c u I « « 3 J J I T J *u l ot cp O rt n t C jq « J S ) rt Cb CQ CP 1. J J o g rt J J O O a ; a J J js c i j n J J s > T J CN I rt CP Ut C CN C » #3 CP rt J J rt ) C C O I i & C w rt .—« rt CP * CP J J J O U 3 • -J CP rt rt J J CN 1 « J S fa. a CO 3 • j J J > a c «w 1 O 3t rtrt* j J j T ) O fa. t • C r t rt J J - • J T » " 0 r t ^ U C O » 4 rt • S C ^ r t t U r t ^ j 3 - C - J 3 : o w o c - r t * J i J S tp J J C - O (J • i CO > — M O I D rt W W Z - I : vo o H CM o c J J t r t IM M C O 0 B I H CP #3 H J J O J O J S J S CP ItN CO-. o J J J J o n > i u c : -t J J rt J J T J rt M-l I j « . a a rt O C * CP J J J J s to tp 6 T J J J tp * 3 C r t j 3 O C t 0 r t r t -rt *e > y * O JJ c a • M - • J C «3 • rt o C E - c n •ri O » r~t • m CN to o JC u c • U Ui i « J C i y c : M rt •do u u c fi T> J J J J S 2 *3 — a a — T J *•* rtrt T J — CP N CN JS CN tq J J — J J c M l O U m J C J S J J • J J § w «— JJ «3 m *3 O rt ^ C tP 10 N O *3 CP c» — •i—s t CO M I — J C CO • tN n c "w In I J J fi T ) T J - _H a a —. C N B f l H "9 rt B O C T J •9 U — rt TJ * 4 rt TJ — * U Ot rt 10 10 C • CP • • rt ^* M tO — . " J J " - . * " ft jc « j n tn B - o "M rt rt • B rt J S tn co to oo 1 rt w ffl . CP rt B b. J J J J J J z u h. rt b. e-S J J CN — C N rt O J J J J rt CN J J rt H „ _ rt fa. & rt J J fai fa. fa. fa. CJ Z J J fa. fa. fa. fa. — H JS JS JS fa. rt b . u h . u u j s j s j s JC fa. J J j j j j y u u j c c M r t r t « J 9 J J J J J J H r t U B - i n H H s a e o n h E t o < u « » a r t r t r t i M M t o I I t I I « a « I I I rt rt rt rt rt ( I I rt rt rt A J A J J J J J A J J J J J J J J J J J J J c p t p t p o t p t p t p c p t p t p c p c o a c o c o t o t o t o t o t n t o t o rt fl e~ rt C TJ cp < — O C N I o to to JC c U CP «J I M ^ J J ri rt u a y rt a — fi ft > » J J rt T J 10 B B J J *3 •32 f JS| 8 to I w T J y J J cp I tP C tO rt -> M O O B ~ i to to a • — J r t r t C J C • ft ft B rt J C ' § J C " J J < «J J J CP CP - B B J J a a 2II S <o a l l J J CN CN J — — to J J J J fa. CN CN J C fMw-i J J J J O J J J J rt O O r t r t rt W M J J J J J S O O J J , tn to to c t* fa. a rt rt o >,>>.:* o oT J T J T J T J rt * J a a a a l I CP CP tp CP J J J J 4J J J J J J J CP CP cn to to tn, to to J-l fa. a — >1JJ O. J J c j tn M fa. J J — a o. to Ot U - C JC C H rt C rt CP O. rt M > — r t 10 u to **J y O CP O rt J J T J >i * J e T J M tO C rt a IM J J Ct) a to T ) **• CP U rt rt «M 1 O tP CP — T J JJ JJ — a « — — Jj JJ — ca tn — o tp ^ VO i J > 0>rt to B w C Cj c a J J a * — CP rt J J JTJ E J S o J J J J CO C £ | C N JJ TJ I W - J J J C J, — U Oi C CP T J T J O * J S C rt rt CO *. J J a 3 J J J J M o w rt < C V J S a J •• a to fi tn i CP O tP J Jj CO cp to a r t T J js o JJ CD C JJ rt to rt a rt M C CP «w a O r t c O U ft o a o to VI ft JJ JJ JJ tp rt to rt T J J J A a Xi tp a to rt JJ J j tl m * M « E O CO J S ts Co J J a C Q J S J S J C — H H i 3. rt >, j d u M c J T J C art c c ,<3 38" - a o o o y ^ • » » & & c c — « n" • i IM to to to 01 JC JC c c to to TJ O tO a TJ — 0 CSI v» -— fi • rt rt >, In & o O H M _ J 3 O « CO M CO 01 « n — J C J C to • • J J O O rt c c „ • • a T J T J J J O ) t 0 f i < < J J — J J I M S oi tp oi rt 5 s i J J e T J a 3 r - tp tp — T J • a t » -— J J J J J J • J J JJ f r iH O) co to 0) fa. fa. n . H fa. fa< Cx H «*t m r> fa. fa. . r t r t H H U.rtrtrtfa.jCJCfa. — tP CP CP — C C t l . fa. — — M-ri O u to M u y J J J J J J J J J J H H t Q t - l H ^-H^i^i-H I I I 01, 10, O O O O O t p e p e p c p e D T J T J T J T J T J n t o t o t o o i to TJ rt rt ft tp O r t tp 9 > § O CO — r t C rt I rA r-H rt b J J V) * " > • • _ o i t p t n v i o . rt c JS . JC J C r t ^ 9 JJ JJ C « " • — JS to — CO o 1 ) < M • . — ft O JJ B S C tp Xi to rtUOOB R tn B «M c m J S 5 . t p t p r t u t o t o j s e T J S f t J J J C J C U C t C IM JJ 1 j r t o a -I to to u rt a a o a o j j j j j j j j j TJ JJ O (D CP tp ( O C Oi r^ r-t r-i rH -O M J S — CN Tj U • rt — T J J J cn • to a e rt • — jc — rt • < W C . 9 J C rt CN e < B w to J J 2 fl) S o i s i " j i s — CN T J a CN AJ Tf — H J J CN « J J rt — CN fa. rt J J J J J J rt CN fa* J J I M J J rt fa. to J J fa. H rt fa. JJ JJ fa. fa. fa. to J S C u r t J S u J S js J C y J J O U J C C J J a J J J J U-ri-ri rt a a o to » tO rt rt <M M 0] I a a I I I rt I trAr-t rt J J • 1 to o t » :& I . ~ H ~ . ( N — CN CP J J c « J J i rt rt a fi a ja a rt c O — CD C J J E o J J rt Xi o rt Q> ft— * -to — • — o < CO M rt < a W  CM ft* Cj CN 10 J J • J J rt . < CN rt tt J J • CP J J J J C rt & J J * M rt J J 3 rt «M rt to CP O JC CO § g « l J J CN TJ — J J TJ J J 0, to ftTJ* W 5 cp J J y J J tp J J J to to • n • to a. rt rtrt ft H u ft c J J ~ ~ ! J C • M M > , J J C — - T J rt in » J S a XI ft a? I it a J J o — E J J J J to TJ rt n JC O H TJ TJ C U T ) rt rt TJ O ^ fl ft A 41 *v fa. rt in J J tp A J J J fa. N rt rt H rt J J J J H rt 0 O r t a 01 a J C b . rt •ri-ri G J J ft ftrt O rt I 10 M C J J > , M CO rt rt TJ | | J3 a rt rt o I tp J J J J J J O J J 9 9 TJ CO CO CO tP "g 122 o o o o O. CO a a o o a. CO • — Ui tn u LJ H S o o a u. o t- u. o a a o o i-> o 6 W I N O I h J J fi«M - H O C U H a a o o P . co E-2 — CN -IS it iH o> ot H E E id u ^ O O v b, b, b.*bT bTcJ U." b." ! l u w I CO J J J J h a * * -H - aw . o a— •H a- a B N » » 0 H a a - a £ N • H O u o a u a o c to N a c l N Di II -H - D 3 >. « O & - H CD fl) « -Si H n ex c : i to 0 X X J J I e c « o 1 « to « T J i i 0 o o 1 TJ TJ a cc — t» bl to —. La o ' o B TJ U 0 «*J W J J C to •H -H > c c • • 1=3 to to -1 *J : J J J J • uutouiintonn x aaaaaaaa Soooooooo ^ C C C C C C C C o....... • u 8 o " o « o ' o ' & & & & 5& . o . o . f a W t n c o t o « J J O O O O O O O O J J J J J J J J J J J J J J J J oououut^oo O X l X t J Q j 3 2 2 j 3 j 3 I Q f l A A f l A f l f l f l D h M M h h H M M - . . a fl A 4 IB a a n fl .—.—. > > > > > > > > Hb.b.b.b.Hb.b. j? ~ ^  H h h h h h MMfchkjhbhlh U B H H B 0 H P jt I H • • I HB H OrtNMOHdrl aaaaaaaa SOHNrlOHNr) O O O O O O O O uaaaaaaaa o. o. o. o. w to w to ooooooooo J 2 ft ft O. ft 1 0 W to tO J J J J J J J J J J J J J J J J f_, g p ( p ( p ( p ( p ( p ( p Q J J J J J J J J J J J J J J J J iHHr-lpHp-IHHH - — u m — — •• a —x O ll ' H > > T J a — a a a N N M a X X X see a 9 w © J J J J a a cp cp £ N H H C O -tJ iH J J a e 123 H H «N O C Z tt> X u •ri O t4 — §5! O O 01 o c « M - O crv u u & A m ex A U A O I CO I A fa. JC fa, fa, -U fa. c « - C - H 3 fa] -H O § 13 Ofi H Dl H JJ H _ - O • 3 •w JJ JC jJ O 3 U 3 —• O * O -H Ol JJ 3 10 Q 3 « hi S D Z 3 A fa. CO I O J C CO rt. 3 U O b . > M jO • 10 >*-85 O H O fi fa. CJ Jc H u o o . « <0 JC fa) u a < tX - A t * H CO 2 JC U - (J < fa. «J t> O cxb. H 3 j a m b. to c o < ^ ' ) Z » f a . 6 fa. « Dl < H « t> * - H 9 H O O < C9 D - H H -I 3 H Q B O H z H fa. C < CJ -H O — : fa, o § — o o H fa. I m — z * 3 n o c c c JC JC JC u u u « e « C fal -H •H CO J CS H « 3 o •• o fa. H .as H fa) c o C CO H fa, •H J CJ O fa. pi CC fa. o H O • CC CJ C JJ O JC *H 3 U 0 H « — H O 8 -*H — — Q S '8 = J C > — 0 c e u •H J C c to I O C *> I > et> o — JJ to •© to to o to <9 > s JJ > 1 2 4 A O 1/1 i X J 0> «< o T J h> X C > « X ta J J OJ « T J • • Q c 0»'H X 0) - . "O fN CN C « X •H 4J 01 « T ) -Q C —• OiH O H M gs g sa «J T J o c .- t>-H Jj o © a a X C Q w 01 u u o> * T J ; U H Q C r ta < » H c o u x tn •83 c u. I X -0) w > T J 3 < c * XTJ -01 C U TJ -H S I X D 0) DC 3 TJ H O T J a Z C CC •H H H a> . X T J -0) c u o* 5 Z T J tn 3 x . . J o d bu bu TJ < bu TJ D> C bu Dl C tn 3 x a o 3 < bu TJ bu Dl C H X O 0> ZTJ - W 3 ~ . - , . J O < fa. < bu bu DICN bu 0><N 3 J J Z - J J J J 2 - J J J J Z - J J J J - H - J J J J H - . 0 3 J J « 3 J J « 3 J J « 3 J J * 3 J J « 3 fa. O Q 3 Q 0 P 3 O 0 Q 3 Q 0 Q 3 C t 0 P 3 C i 0 O H Z O O H Z O 0»H Z O O H Z O D>H 2 O o>3u. t><- - ' ~ ' ~ ' » H J J 0C m Q CC m 3 O X Z O X S OiH t»H CC ro O CC ro Q K n Z O X Z O X Z O X _ _ _ « 0) cp H X TJ -XTJ -XTJ -XTJ -XTJ -XTJ b u c - o o c - H O C - C N O C u c • o c ' H J j a f l - H j j a c - H j J A a - H j j a « * H J J «j <s H 3 J J — 3 J J — 3 J J — 3 J J — 3 J J — H O * H O * H O * H O * H O * -X - JJ • id U n -1 - 3 JJ * * X JJ » O 3 JJ — 01 3 JJ O a TJ O A » H O H C H Q H b» W O H U» 0>JJ cp n Z TJ OI CC fiu -X o C U u H " * §> o» c cc u •H O It — H H " C » H H H 01 X O MO - - - - - 5 C H * : cd o>z v O I H a < u a x M u x « o J J x; o u « J J « J J J J H t 3 3 (J t - O O n n C C C C X X j U U 0 * * 5 ~* bu U H ( U < W mM D J O cc 2 < H fa. D» U hi fa, ; fai „ W D D O J a et o> 2 A H A H bu I I -H - j j bu J J bu O bi 3 « 3 J 3 O WO O J X -X - n - H D H n X - hi o •• o •• o inz z * •« kJ u u J < p JJ p JJ . S bu Z UI Z w CO a * s * x —j — S o 5 Q 3 < U U Z O Z U X u. * u. << << < y « 0>J3 t» CJi Dl « et -et - ~ - -ObuObufa>fa)h'h>bu as o z So'~6'~ Z J J H t>H O co O O * Z Z O* H S H S H O « 0>J3 Q JJ '8 ZZ ZZ* X V V U Z V V O M •-tu tj —Q 3 < O — — — — O fal D tn oi o -bu JJ A D> 3 A O JJ Dl 3 ffl H H •I *H <<TJ -H X H JJ O O 3 a Z o 3 In n fa 125 

Cite

Citation Scheme:

        

Citations by CSL (citeproc-js)

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>
                        
                    
IIIF logo 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-0051420/manifest

Comment

Related Items