ST TO FL TRANSLATIONFORHARDWARE DESIGN VERIFICATIONByLee, Wing SangB. C. Sc. University of Manitoba, 1991A THESIS SUBMITTED IN PARTIAL FULFILLMENT OFTHE REQUIREMENTS FOR THE DEGREE OFMASTER OF SCIENCEinTHE FACULTY OF GRADUATE STUDIESDEPARTMENT OF COMPUTER SCIENCEWe accept this thesis as conformingto the required standardTHE UNIVERSITY OF BRITISH COLUMBIAApril, 1994© Lee, Wing Sang, 1994In presenting this thesis in partial fulfilment of the requirements for an advanceddegree at the University of British Columbia, I agree that the Library shall make itfreely available for reference and study. I further agree that permission for extensivecopying of this thesis for scholarly purposes may be granted by the head of mydepartment or by his or her representatives. It is understood that copying orpublication of this thesis for financial gain shall not be allowed without my writtenpermission.(Signature)________________Department of pset JThe University of British ColumbiaVancouver, CanadaDate / 2 &‘DE.6 (2)88)AbstractDue to the rapid advances of VLSI technology in the past two decades, complicatedhardware designs are now practical and common. Such designs are difficult to verify.Traditionally, design validation had relied on simulation, but exhaustive simulation isimpractical, and as designs get larger, simulation becomes more and more inadequate.In my research, I have developed rigorous, formal methods to verify hardware describedin ST — a simple, intuitive hardware description language. This goal is achieved bytranslating hardware modeled in ST to an equivalent representation in FL — a generalpurpose functional language. With its built-in support for Ordered Binary DecisionDiagrams (OBDDs), Boolean expressions can be easily and efficiently manipulated byFL programs.My research is mostly concentrated on safety property verification. Such propertiesassert that bad things don’t happen to the hardware designs. By using the weakest invariant calculation algorithm designed, which is based primarily on Boolean manipulations,we are able to verify safety properties of ST programs efficiently. Moreover, a refinementrule is also defined. This refinement rule produces a safety property of an implementationdescription; it guarantees that all safety properties of its design specification also holdfor the implementation. Consequently, we are able to verify a specification, and to verifythat all subsequent refinements of the specification are suitable related.iiTable of ContentsAbstract iiTable of Contents iiiList of Tables viList of Figures viiAcknowledgement viii1 Introduction 12 STandFL 42.1 Synchronized Transitions 42.2 FL 83 Translation 143.1 State transition relations 143.2 Representation of ST programs in FL 163.2.1 Representation of variables 173.2.2 Representation of expressions 203.2.3 Representation of transitions 223.2.4 Representation of programs 254 Safety properties 281114.1 Verifying safety properties 284.1.1 Invariants 284.1.2 Deriving invariants 324.1.3 Disproving safety properties 374.1.4 Approaching safety properties 404.2 Generating safety properties 434.2.1 Generic safety properties 434.2.2 Speed-independence 455 Refinement 475.1 Definition of refinement 475.2 Transition matching 505.3 Refinement as a safety property 546 Examples 566.1 An elevator controller 566.2 A transition arbite 627 Conclusion 687.1 Related work 687.2 Goals accomplished 707.3 Future work 72Bibliography 74Appendices 76A Elevator controller 76ivB Transition Arbiter 87C Arbiter incorrect version 94VList of Tables3.1 ST reduction set identities 213.2 ST transition identities 256.3 Elevator car movement controls of the elevator controller specification . . 576.4 Seven floor elevator controller verification performance comparison . 616.5 Status of the transition arbiter implementation 636.6 Transition arbiter verification performance comparison 646.7 Transition trace of the incorrect transition arbiter 67viList of Figures2.1 OBDD of (a A b) V (c A d) with ordering a, b, c and d 122.2 OBDD of (a A b) V (c A d) with ordering a, c, b and d 134.3 The two sets Sq and SQ+ 304.4 The invariant I 324.5 Counter example path 395.6 State transition matching. 536.7 Transition arbiter implementation 626.8 Transition arbiter ST specification 646.9 Incorrect transition arbiter implementation 65viiAcknowledgementSpecial thanks should be credited to the following people: I should thank Dr. MarkGreenstreet for suggesting to me the verification strategies mentioned in this thesis; hissupervision has been a strong helping hand in leading me to the finish of this thesis. Inaddition, he had guided me into modification of his ST-to-C compiler, which allowed meto develop the ST2FL translator rapidly. I also have to thank Dr. Carl Seger for hisvaluable comments on the implementation of the verification techniques in FL. His Vosssystem has been a great tool for experimenting with the verification techniques presentedin this thesis. Finally, I also owe thanks to my fellow students who have tried out theverification tool, and given me insights on improving the tool to make it more usable.viiiChapter 1IntroductionDue to the rapid advances of VLSI technology in the past two decades, complicatedhardware designs are now practical and common. Such designs are difficult to verify.In particular, it can be very hard to ensure the correctness of asynchronous designs.Traditionally, design validation has relied on simulation, but exhaustive simulation isimpractical, and as designs get larger, simulation becomes more and more inadequate. Inpractice, simulation can only reveal the presence of errors, not the absence of flaws. Manyresearchers have proposed formal, mathematical methods to allow rigorous correctnessverification. However, formal methods tend to be too abstract and tedious to be widelyaccepted. In this thesis, the hardware description language ST is used to write simple,intuitive descriptions of hardware that can be verified using rigorous, formal methods.In particular, ST is well suited for describing asynchronous designs.The theme of this thesis is automatic verification of safety properties. These properties can be formulated as Boolean expressions over the state transition relation of thehardware model. When the hardware design is modeled using ST, the state transitionrelation is naturally partitioned into a set of next state functions. This partitioningworks particularly well when the design is asynchronous. Since functions are more easilymanipulated than relations, safety properties of the ST model can be efficiently verified.This verification is performed using the functional language FL, which provides efficientsupport of Boolean operations using Ordered Binary Decision Diagrams. By translatingST programs to FL, efficient verification techniques can be prototyped easily.1Chapter 1. Introduction 2This approach to hardware verification is demonstrated by verification tools for twoclasses of properties — safety properties and refinement. A safety property is an assertionabout the states that can be reached when executing a ST program. Refinement describesthe state transitions that can be performed. When translating a ST program to FL,refinement requirements are translated into corresponding safety properties; thus, thecornerstone of this work is the efficient verification of safety properties.Safety properties assert that “bad things don’t happen.” An example of safety property can be drawn from a traffic light controlling two roads: both green lights shouldnot be turned on at the same time. More precisely, a safety property is defined to bea property that holds in all states reachable in any execution of the program. Accordingly, direct verification of such properties requires reachability analysis of the finite statemachine the hardware model represents. Instead of performing reachability analysis, weuse invariants to verify safety properties. An invariant is an assertion that, if it holdsin one state of the program, it holds in all successor states, and by induction holds inall future states. Invariants can be verified by considering individual state transitions.In general, this is easier than reachability analysis. However, invariants are often muchmore complicated than the safety properties they ensure because invariants often implicitly characterize the set of reachable states. We address this problem by automaticallyderiving the weakest invariant that guarantees a desired safety property.Top down design starts with an abstract, high level specification and leads to a detailed implementation. To ensure the correctness of the implementation, we need toshow that the implementation corresponds to the specification in a certain way. In ourapproach, we impose this correspondence by making sure that the implementation is arefinement of the specification. More precisely, an implementation is a refinement of aspecification if and only if for every state transition of the implementation, there is a corresponding transition (an “explanation”) allowed by the specification. This requirementChapter 1. Introduction 3ensures that all the safety properties of specification are inherited by the implementation.We show how to formulate refinement as a safety property of the implementation. Checking this one property guarantees that the implementation inherits all safety properties ofthe specification.Having highlighted the contents of the thesis, the actual presentation is now presented.Chapter 2 gives an overview of the ST and the FL languages that we use throughout thisdissertation. Then, in Chapter 3, the ST2FL program that translates ST programs intothe FL language is described. Safety properties and refinement are presented in Chapter 4and Chapter 5 respectively. Their definitions and the verification techniques employedare explained in detail in these two chapters. Moreover, in Chapter 6, two examplesare presented, one for each of these two classes. For safety properties, the example is adesign of an elevator controller; for refinement, the example is an implementation of atransition arbiter. They are designed to illustrate the “what” to verify, instead of the“how” to verify as explained in the preceding two chapters.Chapter 2ST and FLAs mentioned in the introduction, we translate ST programs to FL for verification ofsafety properties and refinement. The reason for this translation is that FL is a generalpurpose programming language that supports manipulation of Boolean expressions usingOBDDs. This chapter describes the features of ST and FL that are used in this thesis.2.1 Synchronized TransitionsSynchronized Transitions, ST, is a hardware description language that was designed tofacilitate formal verification of designs. In this thesis, we derive a state transition relationfrom circuit descriptions written in ST. The syntactic structure of ST programs providesa basis for partitioning a program into a set of next state functions. This partitioningleads to efficient verification of safety and refinement properties.ST can be used to describe high level designs and low level implementations as well.For high level specifications, four primitive types, Boolean, integer, floating point andcharacter are incorporated to increase the expressive power of the language. To describelow level implementations, Boolean variables and operators model signals, latches andcombinational logic. In this thesis, we restrict our attention to programs where all statevariables are of Boolean or integer subrange types.Because there is no dynamic allocation in ST, ST programs describe Finite StateMachines (FSMs). The state variables declared in the ST program define the state spaceof the FSM. When different values are assigned to the program’s state variables, the FSM4Chapter2. ST and FL 5is said to be in different states. Mathematically, the state space Sp of the ST programP is defined by the cross product of the variable domains.Sp : dom(vi) x dom(v2)where {v1,v2.. .} is the set of state variables declared in the ST program F,and dom(v) denotes the domain of the state variable v.The state transition relation is represented by the relation Rp.‘RpCSpxSpLike most other programming languages, ST supports data structuring constructs likeinteger subranges, records, and arrays constructed from the primitive types — Boolean,integer, floating point and character. Although we restrict our attention to the twoprimitive types, Boolean and integer, and data structures constructed from them, we cannonetheless verify significant properties of interesting programs. States are defined bystate variables; state transitions are defined by primitive transitions.In ST, a primitive transition T consists of two parts, a precondition G, and an actionM.The precondition G, called the guard, controls when the action can be taken. The actionM is a multi-assignment that assigns new values to the state variables as a single, atomicaction.A multi-assignment can be viewed as a function that determines the next state giventhe current state; thus, a primitive transition T denotes a partial next state functionFT:Sp—*Spsuchthat5’= FT(s) iff G(s) A (s’ = M(s))Chapter 2. ST and FL 6and the corresponding next state relation RT is{(,s’) =For example, with guard G being a V b, and multi-assignment M being {a— b, b —transition T is written as<<a V b —* a, b := b, -‘a>>reading “if a V b holds, then a gets the value of b, and b gets the value of -‘a.” The nextstate function for this transition FT isFT(01) = 11FT(10) = 00FT(11) = 10where 01 means that a is FALSE and b is TRUE, etc.To describe complete designs, three operators to combine primitives transitions areprovided. The asynchronous operator is the fundamental one of these three and is described here. The other two operators are presented in Chapter 3.Asynchronously combining primitive transitions (or simply transitions) has the effectof allowing any one of the transitions to make the state move. In any one step, asingle transition is selected arbitrarily from those enabled (precondition satisfied), thenthe multi-assignment is performed to complete the state move. As a result, the statetransition relation of the program is the union of the next state relations of the primitivetransitions. Mathematically, if the ST program P isT,then the state transition relation Rp is the unionj1 7?TChapter2. ST and FL 7As an example of a complete ST program, a program that describes a modulo-ncounter is shown below:STATIC counter: CELL(STATIC n: INTEGER)STATE cnt: INTEGER;INITIALLY cnt = 0;ALWAYS (cnt >= 0) AND (cnt < n);BEGIN<<cnt<n-1—-*cnt:=cnt+1>><< cnt n - 1 — cnt := 0 >>END;The modulo-n counter is specified by the cell counter. Cells are a structuring mechanismin ST similar to functions in other languages. The counter cell has one parameter n —the modulus of the counter. The local state variable cnt keeps track of the countervalue. If its value is less than n— 1, the counter is allowed to increment; otherwise, ifthe value is equal to n— 1, the counter will be reset to 0. This description is the exactoperation of a modulo-n counter with each step incrementing the counter. Notice thatin the specification, the two annotations INITIALLY and ALWAYS state properties of thecounter— cnt falls in the range [0, n—1] given that cnt is initially 0 — which we canverify using the techniques presented in Chapter 4.In this chapter, ST has been presented as a natural way to describe hardware andto decompose the state transition relation of a hardware model, into a set of next statefunctions; this allows verification to be performed efficiently and easily. For a morecomplete description of ST, the interested reader is referred to the ST language manual[16].Chapter 2. ST and FL 82.2 FLFL [4] is a functional language that, like ML and other well known functional languages,is strongly typed with a polymorphic type inference system. FL is unusual because ituses a fully lazy evaluation semantics and supports Ordered Binary Decision Diagrams(OBDDs) as first class objects. This incorporation of OBDDs facilitates manipulation ofBoolean expression. Because our verification techniques require efficient Boolean representations, FL is chosen as the host language for the prototyping.Every statement in FL is an expression, a function definition or a type definition. Forexample, a statement can simply be an expression that evaluates to a value.1 + 2;is an expression that evaluates to 3. Or it can be a function definition.let sum a b = a + b;defines sum as a function of two parameters that computes their sum; thereforesum 1 2;evaluates to 3. Function definition can be recursive as well. In this case, the keywordletrec is used instead of let. For example, the following defines fact as a function thatevaluates n factorial:letrec fact n=(n = 0) => 1 * (fact (n - 1));If n = 0 holds, this function returns 1; otherwise, n * (fact (n— 1)) is returned.Three of the primitive types that FL supports interest us; they are Boolean, integerand string. More complicated data structures can be defined using the pair and listconstructs: A pair is like a record with two fields, and is created using the “,“ operator.For exampleChapter2. ST and FL 9let agerec = (“Peter”, 25);defines a pair associating the name “Peter” with the age 25. There are two built-infunctions accompany pair structures:• Function fst. This function returns the first element of the association pair.fst agerec;returns “Peter”.• Function snd. This function returns the second element of the association pair.snd agerec;returns 25.A list is represented by enclosing the list elements with square brackets. For example1, 2, 3, 4, 5 j;is a list with the elements 1 to 5 in ascending order. Another method to create a list isby using the “:“ operator.1:2:3:4:5: [j;is equivalent to the above list— where [1 represents the empty list. An illustration oflist structure would be the function accumlist.letrec accumlist base = base:(accumlist (base + 1));The function simply creates the list[base, base + 1, base + 2, base + 3 ...]Chapter 2. ST arid FL 10This list is infinite —accumlist 10;evaluates to an infinite list, and therefore never returns- however the definition ofthe function is legal since FL has a lazy evaluation semantics. There are two built-infunctions for list structures:• Function hd. This function returns the head (first element) of the list.hd (accumlist 10);evaluates to 10.• Function ti. This function returns the “tail” of the list (the list without the firstelement).let is = ti (accumlist 10);defines is as the list [ 11, 12, 13 ...].Additionally, FL supports construction of new type based on the types already defined. For example, a new record type RECORD can be defined as:lettype RECORD = REC mt bool (mt list);It defines RECORD as a new type that contains three pieces of data, an integer, a Booleanand an integer list. REC is the constructor of this record; it accepts an integer, a Booleanand an integer list, and returns the created record. Thereforelet rec_var = REC 2 TRUE [5, 8];assigns to the variable rec_var the record of type RECORD having the fields, 2, TRUEand [5, 8]. Another example is a union in other programming languages:Chapter 2. ST and FL 11lettype INTORBOOL = INT mt BOOL bool;It defines INT_OR_BOOL as a union type that either is an integer or a Boolean. INT andBDDL are the two constructors of this union; INT accepts an integer; BOOL accepts aBoolean. As a result, many interesting data structures can be created easily. In the nextchapter, these features of FL are used to represent the various entities of ST.The preceding description of FL has concentrated on the syntax. However, it isactually the internal representation of Boolean expression that is most important to thework described in this dissertation. The rest of this section introduces the key featuresof this internal representation— OBDDs.In general, Boolean expression manipulation is very difficult. For example, comparing whether two Boolean expressions are equivalent is complete for co-NP. Nevertheless,OBDDs [19] provide a Boolean representation that often makes Boolean manipulationsefficient. In particular, comparison of Boolean expressions requires constant time. Thereason for easy comparison is that OBDDs represent Boolean expressions in their canonical forms — if two Boolean expressions are equivalent, they have the same OBDDstructure.OBDDs represent Boolean expressions as directed acyclic graphs. Internal nodes ofsuch a graph correspond to variables, and leaves are labeled either TRUE or FALSE.When evaluating an expression, the graph is traversed from the root to one of the leavesas follows: when visiting an internal node, a branch is selected to proceed according tothe value of the corresponding variables; when a leaf node is reached, the final decisionis drawn from the leave’s attribute. Figure 2.1 shows an OBDD. In the example, theTRUE branches are indicated by solid lines, and the FALSE branches by dotted lines.Each edge is directed from the upper node to the lower one.As suggested by the name, OBDDs have an ordering along the paths from the root.Chapter2. ST and FL 12Figure 2.1: OBDD of (a A b) V (c A d) with ordering a, b, c and dIn particular, a fixed order is chosen for the variables and every path from the root to aleaf encounters the variables in this order. For a fixed variable ordering, every equivalentBoolean expression has the same OBDD structure. For example, if the variable orderingis a, b, c and d, the Boolean expression(aA b)V(cAd)has the OBDD structure as in figure 2.1. We can observe the effect of different variableorderings by reordering the variables as a, c, b and d; in this case, the OBDD structurelooks different, and is shown in figure 2.2. As these examples show, the variable orderinggreatly affects the size of the OBDD structure, and thus the efficiency of Boolean manipulations. Nevertheless, with careful selection of the variable ordering, OBDDs oftenprovide an efficient Boolean representation.Our verification techniques, which make extensive use of Boolean manipulation benefitfrom OBDDs. In fact, FL is chosen for prototyping our verification algorithms primarilybecause of this feature; on the other hand, verification techniques can be prototyped easilybecause FL is a general programming language. Together with the partitioning of statetransition relations provided by ST, we have the basis to experiment with new verificationEChapter2. ST and FL 13Figure 2.2: OBDD of (a A b) V (c A d) with ordering a, c, b and dapproaches. In the next chapter, the translation of ST programs into FL is explained.The following chapters describe the new verification techniques we implemented.Chapter 3TranslationA ST program denotes a FSM (Finite State Machine). ST2FL produces a representationof this FSM in FL. With this model, properties of the ST program can be formally verifiedautomatically. In this chapter, the translation is described in detail.3.1 State transition relationsAsynchronous hardware designs are usually specified as FSMs with state transition relations. In the preceding chapter, ST was introduced as a formalism that describes andpartitions this state transition relation into a set of next state functions. Therefore, ouraim in translating ST program to FL is that these next state functions should be represented effectively using OBDDs. In return, algorithms can be prototyped easily, andverification can be performed efficiently.A ST program is composed of a set of transitions combined asynchronously. Eachof these transitions consists of two parts, the precondition and the multi-assignment.The precondition is a Boolean expression. Furthermore, the multi-assignment can alsobe considered as a set of Boolean expressions since each assignment is identified byan association of a Boolean expression with a state variable. Consequently, both theprecondition part and the multi-assignment part of a transition can be convenientlyrepresented using OBDDs.Practically, a transition describes a next state function that could be used to determine the next state if the precondition is satisfied. Since transitions are combined14Chapter 3. Translation 15asynchronously to form a program, the state transition relation can be partitioned intoa set of next state functions. This decomposition is advantageous because (1) handlingfunctions is easier than handling relations, (2) the complete state transition needs notbe explicitly created, and (3) the large problem of verifying the whole program is broken down into smaller problems of verifying the individual transitions— this is the wellknown approach DIVIDE-AND-CONQUER. The rest of this section illustrates ourapproach to verification.Consider a general scenario: Given a model of a FSM, it is often desirable to be ableto argue what will happen from state to state over the state transitions. This can beaccomplished easily with Boolean algebra. To illustrate this point, assume that R.1smis the state transition relation of the FSM, and RT’s are the next state relations of thetransitions T’s. As mentioned in Chapter 2, 7?fsm = Rr. Therefore, if the propertyover the state transition p: $ x $ —* BOOL must be maintained for all state transitionof the program, we need to verify thatV(si,s2)E ‘R.fsm :p(sl,s2)VT.V(si,s2)E T :p(sl,s2)VT.Vs E 5: GT(s) = p(s, MT(s))V.s ES: (GT(s) p(s,MT(s)))By embodying p within, we define p’p’: (S — BOOL) x (S —* S) — (S — BOOL)such that p’ accepts a transition — a precondition and a multi-assignment— and returnsthe function that evaluates to the truth value of p with respect to the state transition;i.e.= )G.AMis.G(s) p(s, M(s))Chapter 3. Translation 16The proof becomesVs ES: Ap’(GT,MT)(s)AP’(GT,MT)TRUEIn the next chapter, we show that we can implement invariant verification in the functionp’, and this invariant verification technique is based primarily on Boolean algebra.This example illustrates our approach to verification and suggests that it is practical.In the next two chapters, the actual verification techniques are described in detail. Inthe remainder of this chapter, the translation process is documented.3.2 Representation of ST programs in FLTo unambiguously represent ST programs in FL, we employ a one-to-one translationfrom each ST entity to corresponding FL functions. Thus, the translation provides anapparent meaning for the translated FL program based on the semantics of ST, andmakes the verification more trustworthy. This section presents this translation process.To start with, a general framework for ST programs is introduced: Particularly, a STprogram is composed of a tree structure of cells. Each cell declares types, variables,functions, cells and transitions. All of these entities are explicitly represented in FL.Their representations are simple and are described in the following subsections.Note that ST provides a powerful set of constructs that facilities ST program development; however only a subset of these constructs are handled by the ST2FL translator.The following descriptions do not reflect the complete ST language, but only the subset that is accepted by the ST2FL translator. See [16] for a detailed description of thelanguage.Chapter 3. Translation 173.2.1 Representation of variablesState variables are translated to records of attributes. The idea is to allow them tobe mapped to their OBDDs, which are the basis of our verification technique. In thissubsection, the mapping is explained in detail.ST2FL supports two primitive variable types, Boolean and integer. Booleans areobviously the most natural to represent hardware signaling; whereas integers are mostlyused in higher level descriptions of the hardware. Representations of Boolean expressionis straightforward; however integers cannot be directly represented as OBDDs becauseplain OBDDs do not handle domains with more than two elements. Instead, integersare represented as bit vectors. An immediate consequence of this representation is thatintegers no longer have an infinite domain, but one restricted by their size1.In ST, three data structuring constructs are provided. They are subranges, arraysand records. Subrange variables are no different than integers except range restrictionsare imposed on the values they can assume; therefore they are treated the same asinteger variables. Arrays and records are collections of variables; they are representedwith sets of primitives extracted according to their contents. Thus, all state variablesare represented by sets of primitive variables— Boolean variables are represented usingOBDDs “as-is;” integer variables by bit vectors of OBDDs— which are referenced tousing data structure qualification operators (e.g. array subscripts). In other words, theultimate representation of the set of state variables is a set of properly named OBDDnodes. Accordingly, creation of or reference to a variable involves only generating theproper set of names of the OBDD nodes that makes up the variable.To generate these sets of OBDD node names, each variable is tagged with an encoding1The integer size is specified by the user. This integer size should be large enough so that integeroverfiow/underfiow is not possible.Chapter 3. Translation 18of its type. BOOLEAN and INTEGER are the two primitive types; they are tagged “asis.”• SUBRANGE variables are tagged with1. lo Lower limit2. up — Upper limit• ARRAY variables are tagged with1. type — Base type2. lo — Lower index range limit3. up — Upper index range limit• RECORD variables are tagged with a list fields whose elements define1. type — Field type2. name — Field nameBecause a type in ST can be parameterized and the actual parameters can be referredto, the formal-actual parameter pairs must also be encoded in addition to the aboveinformation. Note that these tags do not introduce additional OBDD nodes. They areused to generate the names of OBDD variables and to provide values of constants thatappear in ST expressions. For example, if arr is declared asTYPEarr_type(lo, up: INTEGER) = ARRAY(lo. .up) OF INTEGER;STATEarr: arr_type(1, 3);Chapter 3. Translation 19then it is translated to the record of attributes below:• Base type: INTEGER• Lower index range limit: 1• Upper index range limit: 3• Parameters: [(“lo”, 1), (“up”, 3)]The mapping from variable to OBDD nodes is defined recursively by the functionNodes shown below:Nodes(rzarne, type){name} if type is BOOLEAN{narne©bit 0 < bit < SIZE— 1} if type is INTEGER{narne© bit 0 < bit < SIZE — 1} if type is SUBRANGE{n e Node.s(narne©idx,type.type) Itype.lo < idx <type.up} if type is ARRAY{ ri E Nodes(narne©fld.name, fld.type) Ifid e type.fields} if type is RECORDwhere © denotes the name concatenation operation for the various types. Continuing thepreceding example, the integer arr[1] is represented as a bit vector with OBDD nodenames “arr[1]:0”, “arr[1]:1”, “arr[1]:2” ... because according to the above definition ofNodes, the variable arr is represented by the sets of OBDDs with names:“arr[1]:0”, “arr[1]:1”, “arr[1]:2” .“arr[2]:0”, “arr[2]:1”, “arr[2]:2” .“arr[3] :0”, “arr[3] :1”, “arr[3] :2” .Chapter 3. Translation 20In addition to the operators that refer to fields of data structures, other operatorsmanipulate expressions of the built-in types of ST. They are described in the next subsection.3.2.2 Representation of expressionsST provides operators for forming expressions of integers and Booleans. A Booleanexpression is one that evaluates to a Boolean value, and is therefore represented with anOBDD. For example, the expression crit = 0 evaluates to(cnt:O = FALSE) A (cnt:1 = FALSE) Acnt:O A cnt:1 AOn the other hand, an integer expression evaluates to a bit vector of OBDDs. Other thanthe usual operators to form Boolean and integer expression, ST also provides a specialkilld of operations set reduction operations.In ST, a set is a list of “guarded” elements with an operator associated with it. Allelements with satisfied preconditions are elements of the set. The operator associatedwith the set reduces the set to a single value. For example, the reduction set{ + con1?val,co2.. .con?va4}reduces to the value(if con then val else 0)In general, the element of the reduction set{op con1?val,co2...con?val}is denoted by SetElemval if conSetElem =op.ident otherwiseChapter 3. Translation 21operation identity+ 0x 1A TRUEV FALSEFALSETable 3.1: ST reduction set identitieswhere op.idertt is the identity (table 3.1) of the operation op; and the reduction set istherefore rewritten asJp SetElemi=1In practice, each set element SetElem is encoded with the precondition cong, the valueval and the operator op. They can then be evaluated the same way as other expressionsare combined.A special set reduction operator, ONE, expresses exclusive selection of a single valuefrom a set. Its value is only defined for singleton set. (In Chapter 4, we describe how thisrequirement can be automatically checked.) It resembles the CASE statement in otherprogramming languages. A ONE reduction set is stored as a list of precondition-valuepairs. Assuming that exactly one precondition is satisfied at any one time, then the resultof the Boolean ONE reduction set{ ONEI cl?vl,c2?v2...c?v}would be V’ (c A v1). If the ONE reduction set is of integer type, the same techniquecan be applied to each individual bits of the set elements.Chapter 3. Translation 223.2.3 Representation of transitionsAs mentioned previously, a ST transition << G — M >> consists of two parts, theprecondition G and the multi-assignment M. In FL, a transition is represented as thepair (C, M). Representation of G is easy since it is a Boolean expression. Notice thatthe multi-assignment M is a set of associations of state variables with expressions; forexample, the multi-assignment{v1 .‘ e1,v2.‘ e2,.can be represented by the list[(v1, ei), (v2,e2),...]Therefore, we represent M as a list of variable-expression pairs. For example, the transition<<aEb—’a,b:=aVb,aAb>>is represented by(ab,[(a,aV b),(b,aAb)])Likewise, the transitionof the module-n counter specification (page 7) is represented as(cnt = n — 1, [(ent, 0)])Although we have been assuming that transitions are combined asynchronously, transitions can be combined using other combinators as well. ST provides three differentcombinators for transitions:Chapter 3. Translation 23The asynchronous combinator.Two transitions combined using are said to beasynchronous because at any one time, either one is taken atomically.The synchronous combinator +. Two transitions combined using + are said tobe synchronous because both of them are taken simultaneously. More precisely,both transitions are examined at the same time; if either precondition is satisfied,the corresponding multi-assignment is performed. If both preconditions are satisfied, both multi-assignments are performed as if they are merged into a singlemulti-assignment— in FL, the two lists that represent the two multi-assignmentsconcatenated. Note that the semantics of ST requires freedom of write conflict(Chapter 4).• The product combinator *. If two transitions are combined using *, for examplethe result is a sillgle transition with precondition being C1 A G2, and action beingthe merger of M1 and M2.Any program can be rewritten as one that only uses the asynchronous combinator bythe following rewrite rules:• el 0 e2 e2 Q el• (elQe2)0e3=elQ(e20e3)•• e * (ci e2)=(e * ci) (e * e2)• ei + e2 (ci * e2) 1 (e1 * e2) (ci * e2) 1 (ei * e2)where-(B<<Gi----Mi>>)=<<-i(YG)>>Chapter 3. Translation 24Where e’s are transition expressions (combinations of transitions), and 0 stands for anyone of the three combinators.Because the verification techniques presented in this thesis requires all transitions becombined asynchronously, ST2FL rewrites ST programs into asynchronous ones. Thisconversion can be performed automatically because the rewriting rules can be implemented easily in FL. However, rewriting could result in exponential increase in programsize. To avoid this, we designed a set of optimization rules. When translating a STprogram, we attempt to keep the FL program size small by looking for special patternand rewriting accordingly.• Unsatisfiable precondition. A transition with a unsatisfiable guard can usually bediscarded; exceptin which case the whole combination result should be discarded.This pattern occurs most often when rewriting synchronously composed transitions.They should be eliminated as soon as possible to prevent exponential growth in thenumber of transitions when generating the FL representation.• <<G1 —* v1 := e1 >> + << G2 —÷ v2 := e2 >>=<< TRUE— v1,v2 := (if G1 then e1 else vi), (if G2 then e2 else v2) >>ifv174v2.Many programs, such as UNITY [5] programs, have the pattern of several synchronous subsystems working together asynchronously. If the sets of transitions ofthe subsystems satisfy the requirement of this optimization, the size of the converted program is linear in the size of the program.• <<G1 —* v1 := e1 >> <<C2 —* v2 := e2 >=Chapter 3. Translation 25operation identityII <<FALSE>>+ <<TRUE>>* <<TRUE>>Table 3.2: ST transition identities<< C1 V C2 —* v1, V2 := (if C1 then e1 else vi), (if C2 then e2 else v2) >>if (1) C1 A C2 is anti-tautology, and (2) v1 v2. Note that if the two transitionsare combined with +, the same optimization still applies.However, experience suggests that this pattern is quite rare, unless the program iswritten with this optimization in mind.A final note concerning transitions is that the set reduction constructs are also defined for them. The ONE set reduction operation is the obvious; whereas the other setreduction operators are, +, and * with identities defined2 in table 3.2.3.2.4 Representation of programsIn ST, cells are considered as units of transitions that are grouped for readability andreusability. Unlike functions, cells last forever, and do not “return.” Cells are instantiated; they are the building blocks of ST programs. As depicted by the framework givenin the beginning of this chapter, a ST program defines a tree structure of cells. Each celldeclares locally the variables it uses, and the transitions that it instantiates. Instantiation of a cell (called cell-instance) is treated like a regular transition; the placement of itrepresents expansion of the cell at that very place. Nevertheless, several characteristicsdistinguish a cell-instance from a transition:2The “identity” for synchronous transition combinator + is not a true identity element, as no suchelement exists. The choice was made for convenience.Chapter 3. Translation 261. Local transitions.2. Local annotations. Annotations state properties of the program. For example,we employ INITIALLY annotations to state the initial conditions of the program,and the ALWAYS annotations to state what conditions should always be satisfiedduring execution of the program. They together specifies what properties shouldbe verified to ensure correctness of the design. In practice, annotations can bedefined specifically with respect to a cell.3. Local variables. When a cell is instantiated, its local variables come into existence.Because these variables are specific only to that instantiation, we need to tag thevariables appropriately so as to differentiate them from the rest. The strategy isto pass a unique identifier to each instantiation, and prefix the variables with theinstance identifier.We represent a cell-instance as an attributed list of transitions; it is a list of transitionsbecause its content is a set of transitions; it is attributed because it has a unique copyof local declarations.For example, the attributed list of the cell counter of the modulo-n counter specification (page 7) consists of the information shown below:• Local transitions. These are represented by a list of (G, M) pairs.[(cnt < n— 1, [(cnt, cnt + 1)]), (cnt = n — 1, [(cnt, 0)])]• Local annotations. They are represented by a pair with the first element being theINITIALLY annotation, and the second element begin the ALWAYS annotation.(cnt = 0,0 cnt < n)Chapter 3. Translation 27• Local variables. They are represented by a list of pairs— the first element beingthe name of the variable, and the second element being its type.[(“cnt”, INTEGER)]Because transitions and cell-instances are very similar, we extend the representationof a transition to allow a common representation for both. The result is representationof a ST transition like a cell, as a unattributed singleton list of FL transitions. Thisstrategy allows combination of transitions and cell-instances be expanded conveniently.The expansion is simply accomplished by merging the attribute lists of the transitionsand/or the cell-instances. To merge two attributed lists of transitions, the attributes areconcatenated, and the transitions are combined as described in the preceding subsection.As a result, we only need to pay attention to the attributed list of transitions the rootcell defines since the root cell of a ST program encodes all information for the program.In conclusion, with proper tuning of the translation methodology, most ST constructscan be directly translated to FL, producing a FL representation that is convenient forverifying properties of the ST program.Chapter 4Safety propertiesCorrectness properties for programs, and therefore hardware designs, can be divided intotwo general categories, namely safety properties and liveness properties. In particular,a safety property states that something bad never happens during the execution of thehardware. In this chapter, verification of safety properties with ST2FL is explained indetail.4.1 Verifying safety propertiesConceptually, safety properties are given by predicates that must be constantly satisfied.With safety properties specified as such predicates, ST2FL verifies that the predicatesalways hold using weakest invariant calculations.4.1.1 InvariantsIn [14], an invariant is defined to be a predicate that, if it holds in the current state, italso holds in every possible next state.Definition 4.1.1:Predicate Q is an invariant of a program P iffV(s,s’) lp : Q(s) = Q(s’)where Rp is the state transition relation of P.28Chapter 4. Safety properties 29Showing that Q is an invariant can be viewed as the induction step in proving thatQ always holds. To complete the proof, we need to show that the initial condition Qologically implies Q. In other words, a proof of Q being a safety property of a ST programP can consist of two steps: (1) prove that Q is an invariant, and (2) prove that the initialcondition Qo logically implies Q. Step 2 is straightforward when both predicates are givenas Boolean expressions represented by OBDDs; however, step 1 is not practical in generalbecause it requires verifying Q(s) = Q(s’) for all state transitions (s, s’). Nevertheless,when the circuit is described by a ST program, we can usually check large groups of statetransitions at a time.The composition of a predicate Q with a multi-assignment M is denoted by thepredicate Q o M. We derive the predicate Q o M with the function substitute(M, Q),which replaces all variables in Q according to the multi-assignment M. For example,.substitute(a i— a + 1, a < b) produces the predicate (a + 1) <b.Accordingly, we formulate the following theorem which provides a way of verifyingan invariant with respect to a single transition:Theorem 4.1.1:Let T <<G —* M>> be a transition.Predicate Q is an invariant with respect to the transition T if(GAQ)zQoMis a tautology.For convenience, we use as a short-hand for Q o M, and write invariarit(T, Q) todenote (G A Q)Chapter 4. Safety properties 30Figure 4.3: The two sets SQ and Sq+Proof sketch: Notice that Q is an invariant with respect to the transition T if and onlyifV(s, s’) E Q(s) = Q(s’)To justify the theorem, we define the two sets S and SQ+ (figure 4.3) asSQ = {s s’.(s, s’) E 7T A Q(s)}SQ+ = {s I s’.(s, s’) E ‘RT A Q(s’)}By the definition of 7T, G(s) (s’.(s,s’) € R). This implies that GA Q describesthe set S. Additionally, by the definition of Q+, Q+(s) holds if and only if there existsa state s’ such that (s, s’) e 7T and Q(s’). This implies that G A Q describes the setSQ+. ConsequentlyV(3, s’) E : Q(s)SQcSQ+(GAQ)=(GAQ)(GAQ)=Q0For example, consider the transition<<TRUE-c:=1—c>>Chapter 4. Safety properties 31with the initial state predicate Qo (c = 0). Let Q be 0 c 1. Then it follows thatQ = 0<c<1Q+ = 01—c1G =TRUETherefore, the proof of Q being an invariant is(TRUEA (0 < c< 1)) (0 1—c 1)TRUEWe can easily see that Qo logically implies Q. Hence the proof of Q being a safetyproperty follows given the initial condition Qo.In Chapter 3, it was shown that if all transitions of a program are composed asynchronously, then verifying that a predicate holds for every element of the program’s statetransition relation can be done by verifying the predicate for each primitive transitions.Verifying that a predicate is an invariant is just a special case of this. This leads directlyto the following theorem.Theorem 4.1.2:Let P T1 T2•..T,, be a ST program.Predicate Q is an invariant with respect to the ST program P ifX invariant(T, Q)is a tautology.Using this theorem, we can prove that Q is a safety property of P by showing(Qo = Q) A (} imvariant(T, Q))This computation can be implemented in FL easily and efficiently.Chapter 4. Safety properties 324.1.2 Deriving invariantsAlthough it is possible for us to verify safety properties using invariants, as described inthe preceding subsection, the algorithm does not always give a definite verdict becausea predicate Q can be a safety property even though it is not an invariant. On the otherhaild, the existence of any invariant I such that(Q0=I)A(I=Q)is sufficient to establish Q as a safety property given the initial condition Qo. Figure 4.4pictorially shows the relationship between the predicates Qo, I, and Q. In this section,we derive the weakest invariant of Q as such invariant I.Definition 4.1.2:With respect to the ST program F, the weakest invariant W of some predicateQ is defined to be the weakest predicate such thatinvariant(P, W) A (W= Q)Predicate W is said to be the weakest predicate implying Q ifFigure 4.4: The invariant IVI.(invariant(P,I) A (I= Q)) = (I =‘ W)Chapter 4. Safety properties 33We shall denote the win of Q with respect to P by win(P, Q).Accordingly, we can show Q to be a safety property of P by proving thatQo = win(P,Q)is a tautology because win(P, Q) is an invariant that logically implies Q. However,deriving win manually is often difficult. In the remainder of this subsection, a simplerecursive algorithm for deriving win is introduced.Consider the predicate Q and the transition << G —> M >>. If Q is satisfied in thecurrent state .s, it is easily shown that Q continues to hold in the next state (after onestep) if and only ifQ(s) A (—iG(s) V (Q o M)(s))(QA(-’GvQoM))(s)Notice thatQA(-’GVQoM)QA(GAQ=QoM)Consequently, by defining Qt to be G A Q = Q o M, we know that Q is satisfied in bothstate s and the next state if and only if (Q A Qt)(s).Having defined Q, we can state a recursive formulation of win with the followingtheorem:Theorem 4.1.3:Let the transition T be <<G —i M >>, and Q be a predicate.IQ ifQTRUEwin(T,Q) =( win(T, Q A Qt) otherwisewhere Qtis GAQQoM.Chapter 4. Safety properties 34Proof sketch: We prove the base case and the recursive case separately: Recall thatQt is defined to be G A Q = Q o M, and hence Q is an invariant if and only if Qt is atautology. Therefore, in the simple case when Qt TRUE, Q is an invariant and thewin of Q is Q itself.Otherwise, in the recursive case, the win of Q is the win of Q A Qt as shown below:• win(F, Q A Qt) = win(P, Q) as shown below:QAQt=Qwin(P,QAQt)=Q= win(P, Q A Qt) = win(P, Q)• win(P, Q) = win(P, Q A Q). We shall show this by contradiction.Assume thatwin(P, Q) win(P, Q A Qt)Therefores.win(P, Q)(s) A -‘win(F, Q A Qt)(s)= s.win(P, Q)(s) A ‘(Q A Qt)(8)This is a contradiction becausewin(P, Q)(s) = Q(s) A (Q o M)(s)howeverQ(s) A-‘(Q A Qt)(s) = -‘(Q o M)(s)In conclusion, win(P, Q) ‘ win(P, Q A Qt). If Qt TRUE, then there exists at leastone state .s such that (Q A _iQt)(s). Thus, each successive approximation of win(P, Q)is a predicate satisfied in fewer states than the previous approximations. The modelingChapter 4. Safety properties 35of P as a FSM implies that eventually Qt TRUE; therefore the recursive algorithmterminates. 0In order to illustrate that the above algorithm can be implemented easily in FL, thefunction, win, that derives the win of Q with respect to a single transition (G, 14) (seeChapter 3 for details on its representation) is listed below:letrec win (G, M) Q =let Qdag (G AND Q) IMPLIES (substitute 14 Q) in(Qdag == T) > Q I win (G, N) (Q AND Qdag);Note that substitute is a built-in function of FL.As a concrete example of win derivation, we consider a single transition that continuously swaps the values of the two Boolean variable a and b.<<TRUE—*a,b:=b,a>>Given the initial condition Qo a A b, we would like to know whether the safety propertyQ b is always satisfied or not. Intuitively, the answer is YES. The derivation of win isshown below:In the first iteration of deriving the winQ —zbQt b=zi-a-‘bVaIn the second iterationQ bA(—ibVa)bAaQt (bAa)(aAb)TRUEChapter 4. Safety properties 36Hence, according to the above theorem, win(b) = b A a. Thereforewin(b)(aAb)=(bAa)TRUEconfirms that b TRUE is a safety property with respect to the transition.The above example illustrates how win, with respect to a single transition, is derived.For a program with multiple transitions, win is the fixed point such thatwin(Ti, = win(T2,Qj,) = = win(T,because Qj,,, must be an invariant for all transitions.Theorem 4.1.4:Let P T1 B T2 T, be a ST program.IQ ifQQwin(P,Q) =win(P, Q) otherwisewhere Q is defined to beX win(T, Q)This completes our approach to verifying safety properties: To verify safety propertyQ of the ST program P given the initial condition Qo, prove thatQo = win(P, Q)is a tautology.Chapter 4. Safety properties 374.1.3 Disproving safety propertiesThe verification technique we have been discussing so far oniy yields the answer YESor NO. To many people, the answer YES is attractive; however the answer NO is oftenunhelpful. In fact, a counter-example is a much better way to say NO because it is helpfulin uncovering design flaws.Although the algorithm stated above could be used to generate counter-example, thecounter-example thus produced can be much longer than the shortest possible one, and isharder to understand; moreover, the algorithm to produce the counter-example would becomplicated and inefficient. The theorem below gives a derivation of win that producesenough information to efficiently yield a shortest counter-example.Theorem 4.1.5:Let P be the ST programM>and Q be a predicate.Define the function next asnext(Q,<<G-* M>)=G=QoMand Q* asQ A Q next(Q, << G —* M >>))AccordinglyIQ jfQ_Q*wzn(P,Q) =L win(P, Q*) otherwiseChapter 4. Safety properties 38Intuitively, next says that if the precondition is satisfied, the transition leads to astate where Q is satisfied. Hence, if Q* is satisfied, then (1) Q is satisfied currently, and(2) all enabled transitions lead to states Q continues to be satisfied. Therefore from astate .s where (Q A _,Q*)(), exactly one step later Q could be violated; i.e. there existsat least one enabled transition which leads from s to a violating state.Following this observation, we write down the Q*s of the above recursive algorithmasrQ* * * * * *0’ fl 2’ k—2’ k—i’ kwhere Q*0 Q, and Q*k is the first predicate in the list that satisfies Qo Ø Q*k. Forexample, consider the transition<<aVb—* a,b:= b,-’a>>with Qo a A b and Q a, we derive thataQ* aA(aVb=b)aAb(aAb)A(aVbbA-’a)FALSEHence the list of Q*s for this example is [a, a A b, FALSEI.According to the above Q*s, the list[,Q* A Qo, ,Q* A Q*k2, Q*k2 A Q*k_3 _Q*1 A Q*0 .,Q]“encodes” all the shortest paths which lead from the initial state to a state that Q is notsatisfied. For convenience, we rename this list as (figure 4.5)[C0,C1,C2 . .. Ck_i, Ck]If we define the states s ‘S according to the following two rules:Chapter 4. Safety properties 391. Go(so). The state would be the start of the counter-example. It satisfies Qosince Co ,Q* A Qo.2. For 1 <i k, s is a state that satisfiesj.C(s) A (s = M(s)) A G(s_1)The state transition (s_, s) would be a step of the counter-example. Such atransition can be found because there exists an enabled transition such that (1)before taking it, C_1 is satisfied, and (2) after taking it, C is satisfied. Moreover,the final step would lead to a state 8k that satisfies Ck, which is equivalent to —iQ.Then a counter-example to shown that Q is not a safety property is simplySi . . . Sk—1,Sk]Notice that given Sj, we are guaranteed existence of a transition that leads to :.Therefore, by first fixing S according to rule 1, we can easily find s1, 2, and so onCkFigure 4.5: Counter example pathChapter 4. Safety properties 40according to rule 2. Continuing the previous example, we haveC0 —-‘FALSEA(aAb)aAbC1 ..,Q* A Q*-‘(a A b) A a-‘bAa—‘aHence the list [a A b, -b A a, —‘a] “encodes” the shortest counter-example that leads toviolating state. By first fixing the initial state, we can easily derive a counter-example;for examplestep a b0 TRUE TRUE1 TRUE FALSE2 FALSE FALSE4.1.4 Approaching safety propertiesComplicated hardware may need a startup procedure to initialize it to some workingcondition. In this case, there may be properties that must hold as safety properties afterinitialization is completed, but transient violation of the property during initializationmay be considered acceptable. However, this reasonable scenario does not satisfy theverification criteria presented previously. In fact, the question we need to ask about suchdesigns is: “Is the hardware eventually safe?”Notice that the win of some safety property Q is a predicate that describes the setof all states from which Q is always satisfied throughout the execution of the hardware.Chapter 4. Safety properties 41If we can show that the hardware eventually gets to one such state, we can definitelyanswer the above question. Since we model hardware designs with FSMs, the time toget to such state would be finite, and therefore the answer would be meaningful. Moreprecisely, our approach is1. Compute the win of Q.2. Make sure that this win of Q is eventually satisfied.We have already designed an algorithm to derive win, but we need a new algorithm toprove that some condition is eventually satisfied. In fact, if we impose a very weak fairnessconstraint on the hardware, the definition of ultima below gives the exact algorithm wewant.To precisely state the fairness constraint, we first define when a transition is active:A transition is active if (1) its precondition is satisfied, and (2) performing the multi-assignment changes the state. We define the function Act asAct(<< G —* M >>) = As.G(.s) A (s M(s))to capture the definition of “active.” Accordingly, the fairness constraint is: If there isat least one active transition, some active transition is eventually executed.Definition 4.1.3:Let F << G ‘ M >> be a ST program.Define Q asQv((Act(<<G —M>>))Aj1(Act(<<G —M >>) =QoM)))Chapter 4. Safety properties 42The ultima of a predicate Q is defined recursively byjfQ=Q#ultzrn(P, Q) =ultim(P, Q#) otherwiseIf s is a state that satisfies Q#, then either (1) Q is satisfied in s, or (2) at least onetransition is active, and all those active transitions lead to states that Q is satisfied. Thus,the fairness constraint guarantees that from a state in which ultim(P, Q) is satisfied, Feventually reaches a state that satisfies Q.For example, the state transition relationa b a’ b’FALSE FALSE FALSE TRUEFALSE TRUE TRUE TRUETRUE FALSE FALSE TRUETRUE TRUE TRUE TRUEcorresponds to the ST program<<TRUE—*a,b:=b,TRUE>>From the state transition relation, we can observe that from any initial state, the programwould reach the state in which a A b is satisfied. To verify our intuition, we derive theultima of a A b. The Act condition is(ab)V(b TRUE)-‘aV-’bTherefore, in the first iterationQ aAbQ# (a A b) V ((-‘a V b) A ((-‘a V b) = (b A TRUE)))Chapter 4. Safety properties 43and in the second iterationQ =—bbV((-iaV-b)A((-aV-b) TRUE))TRUEBecause Q# of the second iteration is a tautology, ultim(a A b) TRUE. Therefore,from any initial state a A b is eventually satisfied.As the consequence of the introduction of ultima, we are able to verify safety propertieswhile allowing initialization: Given the initial condition Qo, we can prove that a designeventually satisfies some safety property Q by showing thatQo = ultim(win(Q))is a tautology.4.2 Generating safety propertiesOther than the safety properties ST program are designed with, there are many implicitsafety properties. For example, “ONE reduction set always contains exactly one element”is a safety property dictated by ST semantics. Although, such safety properties areusually tedious to generate manually, they can be automatically generated easily. In thissection, some of these general properties are introduced first. Then a special propertydesirable specifically for asynchronous designs, namely speed-independence, is described.4.2.1 Generic safety propertiesAny design described using the description language ST must follow the set of restrictionsdictated by the semantics. Failure to follow these rules are considered design flaws, andshould be eliminated. Because for a particular program, these restrictions are usuallyChapter 4. Safety properties 44manifested by some implicit safety properties of the program, our idea is to automaticallygenerate such safety properties from the program text; and with the use of the verificationtechnique presented in this chapter, we are then able to guarantee fulfillment of thosesemantics rules.The following is a list of semantics related safety properties automatically generatedby ST2FL:• Freedom of integer overfiow/underfiow. Because we model integers as fix-sized bitvectors, integer overfiow/underfiow is possible. To ensure that this undesirablesituation is never reached, a safety property can be automatically generated. Forexample, with both a and b being positive integers, the negative result of a + bsignals integer overflow.• Subrange value within range. In ST, two kinds of values have imposed value ranges,namely array subscripts and integer subranges. To ensure the correctness of theprogram, it should be verified that none of these values get out of their prescribedranges.• Single-elemented ONE reduction set. The ONE reduction set is a special constructprovided by ST for the ease of specifying selection. The semantics is that at anytime, exactly one element is selectable from the set. Basically, if cone denotes theguard of the th element of the th ONE reduction set specified in the ST program,then the propertyVi: : con A ( A -‘conk)k.k3should be maintained by the program.• Freedom of write conflicts. According to the semantics of ST, any two synchronoustransitions cannot modify the same variable if they are both enabled at the sameChapter 4. Safety properties 45time. This is to avoid programs which assign conflicting values to the same variablesynchronously. A few strategies are usually employed to guarantees this property,with the simplest being to ensure that no two synchronously combined transitionswrite to the same variable. However, this simple strategy can be too restrictivebecause it fails to examine if both transitions are enabled together. In practice, therequirement can be relaxed toVi,j : Vk,l: G AG3 = (v vii) V (e2k = eii)where vk— ek is the ktI assignment of the ih transition.4.2.2 Speed-independenceA speed-independent design functions correctly regardless of the speeds of its individualcomponents. Basically, any one component if excited to change its output, should remainexcited until the change is completed. To capture the essence of speed-independence, firstconsider when two asynchronous transitions are speed-independent:Two transitions T1 and T2 are speed-independent at state .s ifAct(Ti, s) A Act(T2,.s) =(Wr(T1)fl Rd(T2)= q)A(Wr(T2)fl Rd(T1)= q)A(Wr(Ti) fl Wr(T2)=where• Act(T, .s) is defined in the preceding section. It ensures that (1) the precondition ofT is satisfied in state s, and (2) taking the transition from s makes a state change.• Wr(T) is defined to be the set of variables that are written by the multi-assignmentof T.Chapter 4. Safety properties 46• Rd(T) is defined to be the set of variables that are read to evaluate the precondition,or to perform the multi-assignment.This gives the safety property that guarantees speed-independence between two transitions:(G1 A (y v1 ei)) A (G2 A (V v2.i e2)) =(Wr(Ti) fl RcZ(T2)= q)A(Wr(T2)fl Rd(T1)= qS)A(Wr(Ti) fl Wr(T2)= q)where vj — ejj is the j assignment of T:. We shall denote this safety properties assi(Ti, T2).Having defined si, verification of speed-independence follows easily: To verify thatthe program is speed-independent, show thatA si(T,T)iJis a safety property of the program.Chapter 5RefinementTop-down hardware design starts with an abstract specification, followed by iterativesteps of refining the design until a concrete implementation is reached. It must beverified that each refinement corresponds to the specification in an acceptable way. Inthis chapter, a simple rule is introduced for when an implementation is a refinement ofthe specification. This rule ensures that the implementation inherits all safety propertiesof the specification. After defining refinement, a verification strategy is presented; thestrategy involves generating the corresponding safety property and verifying it by meansof the win calculation.5.1 Definition of refinementIntuitively, if a concrete implementation is a refinement of an abstract specification,there must exist a correspondence between them. We impose this correspondence by therefinement rule which requires that every action of the implementation be “explicable”by the specification. The refinement rule guarantees that the concrete implementationcannot reach a situation that the abstract specification could not.Before a precise definition of the refinement rule can be given, the concept of equivalence between abstract and concrete states must be clarified. In order to state preciselywhen a concrete state is equivalent to an abstract state, a relation between values of theabstract state variables and those of the concrete state variables is needed. This relationis called an abstraction mapping.47Chapter 5. Refinement 48Definition 5.1.1:An abstraction mapping, map, is a function1 that maps a concrete state toan abstract state:map: SC—‘where 5a and S are the abstract and the concrete state spaces respectively.We say that the concrete state 3c is equivalent to the abstract state 5a if and only if= map(sc)(Notice that many concrete states can map to the same abstract state since the functionmap is not required to be one-to-one; however, every concrete state maps to a singleabstract state.) Accordingly, we define the refinement rule with the following definition:Definition 5.1.2:A concrete implementation Fc with initial condition Qc0, is a refinement ofan abstract specification Pa, with initial condition Qa, under the abstractionmapping map if (1)‘V/Sc Sc : Qc0(c) =‘ Qao(map(sc))where Sc is the state space of Pc, and (2)V(c, s) E(map(sc) = map(s)) V ((map(sc),map(s)) E ?a)where ‘1c and 7?a are the state transition relations of P and Pa respectively.‘In a more general framework, an abstraction mapping could be a relation; however, we do notconsider such mappings in this thesis.Chapter 5. Refinement 49Intuitively, the first criterion of the definition ensures that the concrete program startsoff from a state that is equivalent to an initial state of the abstract program; whereas thesecond criterion captures the two situations below:• The concrete state transition does not affect the abstract state. This situation ismost common when the concrete state transition only changes the values of internalstate variables of the implementation, which have no direct relationship to abstractstate variables.• There exists an equivalent abstract state transition. In this case, an abstract transition can be found to change the values of the abstract state variables in the waythat matches the concrete state transition.The refinement rule ensures that safety properties of the specification are preserved bythe implementation. To justify this claim, we must first give a precise definition of“preserve.”We say that P preserves the safety property Q of Pa if all states P reaches whenmapped back to their equivalent abstract states satisfy Q; i.e. if s is a state that Preaches, then Q(map(s)) holds. Mathematically, )sc.Q(map(sc)) is the safety propertyof P that corresponds to the safety property Q of Pa. We can rigorously prove that anysafety property Q is preserved, by showing that the invariant property WQ W(Pa, Q)is preserved:1. Vs, S : Q0(s) = I’VQ(map(sc)) — WQ is satisfied initially.According to the first criterion of the refinement ruleVs E S : Qcü(Sc) Qao(map(.sc))Notice that Q0(map(s)) = Wqfrniap(s)) since Q is a safety property of Pcj.Chapter 5. Refinement 50ThereforeVs : Q(s) = WQ(map(s))2. ‘v’(s,s’) E 7?: WQ(map(s)) = WQfrnap(s’)) — WQ is satisfied thereafter.If we let that Sa = rnap(sc) and s = map(s’), then according to the second criterionof the refinement ruleV(s,s) e : (a = V ((3a,3) E fla)Note that (1) (a = s) A WQ(Sa) implies that WQ(.s) holds, and (2) ((Sa,Sj) Efla) A WQ(Sa) implies that WQ(S’) holds because WQ is an invariant. ThereforeV(s,s) e : WQ(map(s)) = WQ(map(s’))This shows that for every state that P reaches, W is satisfied in the equivalent abstractstate. Because WQ Q, the safety property i\s.Q(map(s)) is satisfied by P.5.2 Transition matchingIn this section, the technique that we use to check refinement is presented. We call thistechnique transition matching, matching of concrete transitions with abstract transitions.Basically, it checks to see if every concrete transition is “explicable” by the abstractprogram.Definition 5.2.1:Let P be a concrete program consisting of a single transitionT=<<G-M>>and Pa be an abstract program:Pa << Gai “ Mai >>Chapter 5. Refinement 51T is matched against Pa under the abstraction mapping map ifVs S : G(s)(map(sc) = map(M(s))) V(i : Gaj(map(sc)) A (map(Mc(sc)) = Ma1(map(sc))))where S is the state space of P.To simplify the definition, we implicitly add to the abstract program Pa the identitytransition << TRUE>>, to match concrete state transitions (se, s) satisfying map(sc) =map(M(s)). The resulting simplified definition isVs E Sc : Gc(Sc) ‘(Gaj o map)(sc) A ((map o Mc)(c) = (Mai o map) (Se))and we define the corresponding predicate match asmatch(Tc, Fa nap) = G =7 (Gai o map A (map o M Maj o map))where Ga0 TRUE and Ma0 . Accordingly, T is matched against Pa under theabstraction mapping map if and only if raatch(Tc, Fa map) is a tautology.Theorem 5.2.1:Let Pa be an abstract program with initial condition Qa0, andP EEW Tbe a concrete program with initial condition Q0.P is a refinement of Pa under the abstraction mapping map if(Qc0 Qaü o map) A ( match(Tcj, Pa map))is a tautology.Chapter 5. Refinement 52Q0 Qao o map ensures that P and Pa start off from equivalent states, andmatch(T, Pa map) ensures that all transitions of P are “explicable” by Pa. Hence,this theorem gives a sufficient condition for refinement; however, weaker conditions arepossible. Such a condition is presented in the next section.To illustrate how the theorem is employed to test refinement using OBDDs, a simpleexample is shown below:The abstract program Pa declares an integer variable cnt, and has a singletransition<<GaMa>><<.cnt<2—*cnt:=cnt+1>>The concrete program P, declares two Boolean variables h and 1, and has asingle transitionThe two Boolean variables h and 1 of P are supposed to be the two bitsrepresenting the integer cnt of Pa. Therefore, the abstraction mapping mapis defined ascrit = (if h then 2 else 0) + (if 1 then 1 else 0)As shown pictorially by figure 5.6, the concrete state transitions are matched with concrete state transitions. (Notice that Pa has state transitions not matched with Ps’s statetransitions; this situation is allowed by the refinement rule.) The following shows thesteps for performing transition matching using OBDDs to check if P is a refinement ofF:Chapter 5. Refinement 53Abstract FSMFigure 5.6: State transition matchingThe composition operator o is familiar to us. Recall that we compute Q o M, thecomposition of a predicate Q with multi-assignment M, by substitution of the variablescomprising Q according to M. The computation of Ga o map is handled in a similarfashion, by substituting the variables comprising Ga according to map. ThereforeGa o map(ent < 2) o (cnt = (h?2 : 0) + (l?1 : 0))(h?2: 0) + (l?1 : 0) 2-(hAl)By the same token, we compute Ma o map by substituting the variables comprisingthe right hand sides of Ma according to map.Ma o map(cnt — cnt + 1) o (cnt = (h?2 : 0) + (l?1 : 0))cnt f— ((h?2 : 0) + (1?1 : 0)) + 1It tells what value, in terms of concrete state variables, crit should be after performingthe abstract transition. Similarly, we compute map o M by rewriting the right handConcrete FSMChapter 5. Refinement 54sides of map according to M.map o(cnt = (h?2 : 0) + (l?1 : 0)) o (h — 1, 1 i— -‘1)crit = (l?2 : 0) + (—l?1 : 0)It tells what the equivalent value of crit is after taking the concrete transitions. Therefore,the comparisonmap o M = Maj o mapis performed by pair-wise equating the right hand sides of the two composition results.If the integer representation of cnt is two-bit unsignedmap o M = Maj o map(172 : 0) + (—‘171 : 0) = ((h?2 : 0) + (l?1 : 0)) + 1It then directly follows that Pt-, is matched against Pa:G (Ga o map A (map o M = Maj o map))(-(h A 1) A -‘h)TRUEThus, if the two programs start off from equivalent states, then P is a refinement of Pa.5.3 Refinement as a safety propertyThe transition matching technique presented in the preceding section ensures that everyconcrete transition is “explicable” by the abstract program, and hence guarantees fulfillment of the refinement rule. However, this formulation is not the most general. Instead,Chapter 5. Refinement 55a weaker condition requires that every reachable concrete state transition be “explicable”by the abstract program. This leads to our refinement verification strategy.Our strategy is based on the concept of transition matching. However, instead ofrequiring that transitions be matched, a safety property of the concrete program, derivedfrom the match formulation and defined below is used to guarantee refinement.Theorem 5.3.1:Let Pa be an abstract program, andBbe a concrete program.Letrefine(P, Fa map)=match(T, Fa map)If refine(P, Pa map) is a safety property of P, then P is a refinement of Pa.The proof follows directly from the definition of the refinement rule, and the details areomitted.We verify refinement using the safety property refine as follows: Given the concreteprogram P with initial condition Q, and the abstract program Pa with initial conditionQaü, P is a refinement of Pa if(Q0 Qa0 a map)A (Q0 = wiri(P, refine(Pc,Pa,map)))is a tautology. This condition is necessary and sufficient for refinement. Sufficiency followsfrom the above theorem. Necessity can be shown by considering a counter-example ifrefine(P, Pa, map) is not a safety property. Any such counter-example is also a violationof the refinement rule.Chapter 6ExamplesIn order to illustrate how the verification tool described in this thesis helps us to developsafe hardware, two simple examples are presented in this chapter. The first example isa specification of a single-car elevator controller; it illustrates “what” properties can beverified to gain confidence in the design. The second example is an implementation of atransition arbiter; it illustrates refinement verification.6.1 An elevator controllerThis section presents a simple single-car elevator controller specification. In additionalto the controller, the elevator car is also modeled to allow thorough verification. Thecontroller itself is divided into two parts:1. The “control.” This part handles signals from control buttons involved in controlling the elevator, and responds to these signals by sending appropriate commandsto the elevator car motor controller. For example, call buttons, door open/closebuttons, etc. are handled by this part.2. The elevator car motor controller. This part receives elevator car motor commandsfrom the “control,” and only forwards to the car motor those that would not putthe elevator in an unsafe situation.One expects that the design of the “control” part could be complicated and prone toerrors. Therefore, the motor controller is introduced as an intermediate component to56Chapter 6. Examples 57up down actionFALSE FALSE StopFALSE TRUE Go downTRUE FALSE Go upTRUE TRUE undefinedTable 6.3: Elevator car movement controls of the elevator controller specificationreduce the complexity of the whole design, and thus to make the design more reliable.Since we make the elevator car motor controller solely responsible for safety, we concentrate on the specification of its design. As for the design of the “control,” it is specified tosend arbitrary signals to the motor controller for the sake of verification. See appendix Afor the ST specification of this design.In the specification, we used three modules to describe the design: (1) the “control,”called tester, (2) the elevator car motor controller, called motor, and (3) the elevator car,called car, which models the behaviors of the elevator car in response to the signals frommotor. Two sets of control signals are defined to interface between the three modules:1. Elevator car motor control signals. These signals consist of the ones that controlthe movement of the elevator car, up, down and park, and the signal open whichinstructs the elevator car to open its door. The signal park instructs the elevatorcar to stop at the coming floor. The movement of the elevator car is controlledby the two signals up and down as described in table 6.3. In reality, signal up andsignal down should not both be set on; however, if this should happen, the programspecifies that the elevator car goes down. There are two variables of this recordtype: carMove, which is for the movement signals sent from tester to motor, andcCarMove, which is for the movement signals sent from motor to car.Chapter 6. Examples 582. Elevator car status signals. These signals consist of the ones that reflect the status ofthe relative position of the elevator car, top, bottom and near, the ones that reflectthe status of the elevator car door, opened, closed and blocked, and stoppedwhich signals when the elevator car is stopped. The signal blocked signals thatthe elevator car door is blocked by some obstacle. (It is generated by the celltester to emulate possible car door blocking.) In reality, it is not supposed to beturned on when the elevator car door is closed; however, if this should happen, theprogram specifies that the elevator car stops. The variable of this record type iscarSt ate.Several variables are used internally by the module car:• Integer curFir. This integer variable is used to keep track of the floor number ofthe elevator. The value of this variable should range from 1 to numOfFloor.• Integer drPos. This integer variable is used to keep track of the elevator car doorposition. If drPos is 0, the door is considered closed; if drPos is DRPOSMAX, thedoor is considered opened.• Integer carPos. This integer variable is used to keep track of how far the elevatorcar is above a particular floor. If carPos is 0, the car is at a floor; if carPos is 0,1 or CARPOSMAX, the car is considered near a floor.Given this specification, we have several safety properties to verify to assure thesafeness of the controller.• Either the elevator car is stopped, or the car door is closed.carState . stopped OR carState . closedChapter 6. Examples 59• Door closed signalThis ensures that the elevator car does not move when the car door is opened toload/unload people.• Either the elevator car is near a floor, or the car door is closed.carState.near OR carState.closedThis ensures that the elevator car does not stop between two floors then open thecar door.Additionally, there are some properties can be verified to gain confidence in the elevatorcar model:• Door opened signal carState.opened(drPos = DRPOSMAX) = carState.openedcarState . closed(drPos = 0) carState.closed• Car near floor signal carState.near((1 < carPos) AND (carPos < CARPOSMAX)) XOR carState.near• Car at top floor signal carState.top((curFir = numOfFloors) AND (carPos = 0)) = carState.top• Car at bottom floor signal carState.bottoiu((curFir 1) AND (carPos = 0)) = carState.bottomChapter 6. Examples 60The properties stated above are safety properties. They assert that certain bad thingsdon’t happen. In particular, they are satisfied by a program that does nothing (e.g. <<FALSE >>). To increase our confidence that the program can reach states correspondingto typical scenario for a real elevator, we check for the existence of a path from theinitial state to a state satisfying some property Q. We can easily verify this propertywith —‘win(--iQ): If we can show that -iwin(--iQ) is satisfied initially, we are guaranteedexistence of a path from the initial state to a state that satisfies Q. Moreover, we couldfind out one such path by tracing a counter-example that disproves-‘Q being a safetyproperty.The predicate —iwin(--iQ) represents the set of states from which the condition Q isreachable. Hence, if the elevator controller is always in an invariant subset of this set(i.e. —iwiri(-’Q) is a safety property), the condition Q is always reachable by the elevatorcontroller. Accordingly, we can more rigorously test the elevator car model by showingthat win(—iwin(—iQ)) is satisfied initially. Some properties Q’s to test for interestingpaths of the elevator model are stated below:1. Because the elevator car door is initially closed, our first step is to check if the doorcan ever be opened. The predicate Q in this case iscarState. opened2. The next step is a large leap. We check if the elevator car can ever reach the topfloor, and can open its door when it is there. The predicate Q iscarState.top AND carState.opened3. Finally, we check if the elevator car can come down from the top floor. To do thiswe need some minor modifications to the ST program:Chapter 6. Examples 61partitioning YES ] NOFSM size 139 BDD nodes } 7127 BDD nodesproof timecarState.stopped OR carState.closed 0.2 seconds 17.0 secondscarState.near OR carState.closed 1.7 seconds 71.1 seconds(drPos = DRPOSMAX) = carState.opened 0.1 seconds 18.8 seconds(drPos = 0) = carState.closed 2.1 seconds 67.6 secnodsTable 6.4: Seven floor elevator controller verification performance comparison(a) Add an auxiliary Boolean variable reached, which should initially be FALSE.(b) Add the transition<< carState.top AND carState.opened —÷ reached : TRUE >>to the root cell.Now, the predicate Qreached AND carState.bottom AND carState.openeddepicts the situation: the elevator car reaches the top floor, opens its door, closesit again, comes down to the bottom floor, and finally opens the door again.In order to contrast the performance of ST2FL with traditional symbolic model checking algorithms (state transition relation not partitioned), we have embedded a traditionalsymbolic model checker in ST2FL. By running ST2FL on a SPARC 10-512mp with 64Mbytes of memory, and verifying some of the properties described above, we have collectedthe performance data list in table 6.4.Chapter 6. Examples 626.2 A transition arbiterIn this section, an implementation of a transition arbiter (figure 6.7) described in STis presented: The arbiter has two clients, each of which communicates with the arbiterusing three signals r for request, g for grant, and d for done. Transition signalingis employed; for example, if a client wants to request the privilege, and its signal r iscurrently low (respectively high), the client makes the request by toggling the requestsignal to high (respectively low). Each client can be in one of the the four states describedin table 6.5. When a client is in the “idle” state, it may request the privilege by togglingthe request signal r to enter the “requesting” state. The arbiter grants a pending requestby toggling the grant signal g, bringing the interface to the “privileged” state. Then,the client can release the privilege by toggling the done signal d, returning the interfaceto the “idle” state. (From the “idle” state, the client can make another request.) AfterChapter 6. Examples 63state description state namer—g=d idle-‘r = g = d requesting-‘r = -‘g d privilegedr = = d pending-doneTable 6.5: Status of the transition arbiter implementationthe arbiter grants the privilege, the client can toggle d and r to release the privilege,and then request it again. Because the protocol is designed to be delay-insensitive, theseevents may appear at the arbiter in either order. If a new request appears before thedone signal from the previous cycle, the arbiter sees the interface in the “pending-done”state.The arbiter has two clients. A correct implementation should guarantee that bothclients cannot be in the “privileged” state at the same time. We could verify this requirement as a safety property. Instead, we give an abstract specification and verifymutual exclusion for this simple program. Then, we verify that the implementation isa refinement of the specification. Figure 6.8 shows the ST code for the specificationwhere cl.r, cl.g and cl.d are the request, grant, and done signals for the first client ci,c2 is the signals for the second client, and privileged is as defined in table 6.5. In appendix B, an implementation is described in ST. We embedded the arbiter specificationin the ST program as the cell abstract, and declared that the program is a refinementof abstract with the REFINE annotation. Note that the abstraction mapping is specified by the Boolean constant TRUE which implicitly maps all concrete variables to theabstract variables having the same names. Data is collected to show the performance ofST2FL in verifying refinement of this transition arbiter implementation; additionally, itsperformance is contrasted with the performance of a traditional symbolic model checkerChapter 6. Examples 64ALWAYS NOT(privileged(cl) AND privileged(c2));BEGIN(* internal arbiter *)<< NOT privileged(c2) —* cl.g : cl.r >><< NOT privileged(cl) — c2.g : c2.r >>(* client 1 *)<< cl.r := NOT cl.g >><< cl.d : cl.g >>(* client 2 *)<< c2.r : NOT c2.g >><< c2.d : c2.g >>END;Figure 6.8: Transition arbiter ST specificationpartitioning YES NOFSM size 28 BDD nodes 5276 BDD nodesproof time 23.8 seconds 186.2 secondsTable 6.6: Transition arbiter verification performance comparison(state transition relation not partitioned). The data collected is list in the table 6.6.It is worth mentioning that the above implementation of the transition arbiter isour second attempt; our first attempt is shown in figure 6.9, and the ST description isin appendix C. When we designed the first circuit, we simulated it for 500,000 statetransitions by compiling its ST program to C [16], and then compiling and executingthe C program. Mutual exclusion was maintained throughout the simulation. We thenattempted to verify mutual exclusion as a safety property using ST2FL. Within oneminute, ST2FL reported that the weakest invariant for mutual exclusion was FALSE;i.e. from any state, a state could be reached that violate mutual exclusion. Furthermore, ST2FL gave a shortest sequence of transitions that starts in a state satisfying theChapter 6. Examples 65Figure 6.9: Incorrect transition arbiter implementationChapter 6. Examples 66INITIALLY predicate, but leads to a state that violates the ALWAYS predicate. The trace(table 6.7) consisted of 38 state transitions. After uncovering the flaw with ST2FL, wefurther simulated the arbiter in order to see how well simulation does in revealing designflaw. However, after simulating more than 2,000,000 state transitions the error remainedundetected. We believe that this example demonstrates that simulation can be an inadequate verification technique, even for a relatively simple design, and that it demonstratesthe value of the automatic tools described in this thesis.Chapter 6. Examplesci.r ci.g ci.d c2.r c2.g c2.d si ti ui vi wi xi yi zi s2 t2 u2 v2 w2 x2 y2 z2 T#678384878889ioii81213814is816817818192082122823248258268278282983083132833834835836837838F F F F F F FFFTFFTFFFFTFFTFI F F F F FFFFTFFTFFFFTFFTFT F F F F F IFFTFFTFFFFTFFTFT F F F F F T%FTFFTFFFFTFFTFT F F F F F TTITFFTFFFFTFFTFT F F F F F TTTFFFTFFFFTFFTFT F F F F F TTTFTFTFFFFTFFTFT F F F F F TTTFTTTFFFFTFFTFT F F F F F TTTFTTEFFFFTFFTFT F F F F F TTTFTTFIFFFTFFTFTI F F F FTTTFTTFTFFFTFFTFT T F F F FTETFTTFTFFFTFFTF£ T F F F F TFTFTTFTFFFTFFTFF T I F F F TFTFTTFTFFFTFFTFF T T F F F TFTFTTFFFFFTFFTFF T T F F F TFTFTTIFFFFTFFTFF T T F F F TFFFTTTFFFFTFFTFFT T F F FTFFITTTFFFFTFFTFFT T F F FTFFTFTTFFFFTFFTFF T T F F F EFFTFTTFFFFTFFTFF T T F F F FIFTFTTFFFFTFFTFF T T F F F FTITFTTFFFFTFFTFF T T F F F FTTFFTTFFFFTFFTFF T T F F F FTTFITTFFFFTFFTFF T T F F F FTTFTETFFFFTFFTFF £ T F F F FTTFTFTFFFFTFFTFF F T F F F FETFTFTFFFFTFFTFF F T F F F FFFFTFTFFFFTFFTFF F T F F F FFFTTFTFFFFTFFTFF F T I F F FFFTTFTFFFFTFFTFF F T T F F FFFTTFTFIFFTFFTFF F T T F F FFFTTFTFTTFTFFTFF F T T F F FFFTTFTFTTITFFTFF F T T F F FFFTTFTFTTTFFFTFF FT T F FFFFTTFTFTTTFIFTFF F .T T F F FFFTTFTFTTTFTITFF F T T F F FFFTTFTFTTTFTTFFF F T T F F FFFTTFTFTTTFTTFIF F T T I F FFFTTFTFTTTFTTFT19567128910116192010971256712811671211213143415161718Table 6.7: Transition trace of the incorrect transition arbiterChapter 7Conclusion7.1 Related workSince traditional simulation is seldom exhaustive, and therefore is often inadequate inhardware correctness verification, formal approaches are developed to overcome thisweakness. Two common formal verification approaches are theorem proving and modelchecking.Theorem proving involves formally describing the specification and the implementation of some hardware design, and proving that the specification and the implementationare suitably related. Although the proof can be mechanically checked, the derivation ofit tends to be very tedious. Nevertheless, theorem-provers usually help to reduce thistedium by deriving most of the proof steps automatically; however, full automation is notyet possible. (Although the lowest level proof steps can be performed automatically, theproof process remains much more tedious than that of an informal (unreliable) manualproof.) Usually, the components of the implementation are verified against the components of the specification to ensure that the two levels of the hardware design are suitablyrelated; thus theorem proving is structural rather than behavioral. An example of sucha theorem-prover is the HOL system [15] developed at Cambridge University. HOL isan interactive theorem proving environment for classical higher order logic. The primaryinterface to HOL is the functional language ML (Meta Language). With a specificationand implementation modeled in ML, the user applies ML functions, representing rules of68Chapter 7. Conclusion 69inference, axioms, or previously proven theorems to prove the correspondence betweenthem; the sequence of such application is the formal proof. Not only can HOL be usedas a stand-alone system, it can be embedded as the theorem proving engine in someverification application system as well. For example, a verification tool has been builtfor the Z specification language based on HOL (see [15]).Model checking is behavioral as opposed to the structural approach of most theoremprovers. Given a model of the behaviour of some hardware design, and some propertiescapturing the correctness of it, the model is automatically checked to determine if thebehaviour satisfies the properties. Even though the properties can be precisely and conveniently specified using various forms of temporal logic (e.g. Computational Tree Logic),it can be difficult to determine that the properties completely characterize the correctness of the hardware. A further problem with model checking is the “state explosionproblem” since traditionally, the state transition relation of the FSM is not partitioned.An example of model checker is the SMV system [13] developed at Carnegie-Mellon University. It incorporates its own description language that can be used to describe bothsynchronous and asynchronous circuits. Since it is intended to model circuits as FSMs,the only data types supported are Booleans, scalars and fixed arrays. With properties toverify specified in CTL, SMV uses an OBDD-based symbolic model checking algorithmto determine whether or not they are satisfied.The verification tool ST2FL presented in this thesis is a specialized form of modelchecking. ST2FL models hardware symbolically using a set of next state functions tohandle the “state explosion problem;” moreover, this decomposition of the state transitionrelation makes new verification algorithms possible. We not only check properties ofhardware models, if given a specification, we verify refinement— correspondence betweenan implementation and the specification — as well. Thus, our approach addresses bothproblems associated with traditional model checking and theorem proving. (FurtherChapter 7. Conclusion 70application of ST2FL is necessary before the success of this approach can be thoroughlyevaluated.) Although we emphasized safety properties, as mentioned later in this chapter,we expect verification of liveness properties to be incorporated into future versions ofST2FL.The “backward traversal” approach that ST2FL uses to derive the set of states fromwhich a safety property Q always holds is also employed by the Ever system [1]. Theyclaim that the “back images” are more easily evaluated given that the state transitionrelation is described in Ever [3j (using high-level data structures, imperative semantics,and non-determinism); the experimental results they gave in the paper are encouraging.Moreover, they suggested that, in contrast with verifying a set of safety properties as asingle big BDD, keeping a list of BDDs implicitly conjoined during the execution of thealgorithm would be a better approach. The ground is that simplification to the BDDscan be performed in run time: Given the two BDDs Qi and Q2, Q can be replaced witha possibly smaller BDD i as long as = Qi whenever Q2 is true; essentially, theyview-‘Q2 as a “don’t-care” to simplify Qi. We plan to incorporate this scheme into afuture version of ST2FL.It is worth mentioning that a ST-to-C compiler, which compiles ST programs intosimulators in C, was developed by Dr. Mark Greenstreet of the University of BritishColumbia. Because ST2FL is developed based on the ST syntax recognizable by theST-to-C compiler, hardware, described in ST can be verified as well as simulated.7.2 Goals accomplishedIn Chapters 4 and 5, techniques for safety property verification and refinement verificationwere presented. As shown by the examples in Chapter 6, verification of these properties isfully automatic, and helpful in verifying the correctness of hardware designs. The elevatorChapter 7. Conclusion 71controller example has illustrated “what” properties can be verified to assure correctnessof designs. Moreover, with the transition arbiter example, refinement verification wasillustrated; it ensures inheritance of safety properties from specifications.The safety property verification technique was described in Chapter 4. The technique is based on the concept of an invariant, which ensures that if some predicate issatisfied in the current state, it is also satisfied in all possible next states. Additionally,a technique for deriving the weakest invariant (win) that implies a desired safety property was designed since invariance is a sufficient but not necessary condition for provingsafety properties; in contrast, win is both necessary and sufficient for establishing a safetyproperty. Furthermore, the win derivation provides a shortest counter-example if someproperty does not hold as a safety property; this capability is very helpful in diagnosingdesign flaws.In Chapter 5, a refinement rule was introduced as a basis for claiming that an implementation refines a specification. This rule requires that state transitions of the implementation be “explicable” by the specification; this guarantees that safety properties ofthe specification hold in the implementation as well. We verify refinement by generatinga safety property according to the refinement rule and using the win derivation to provethat the refinement rule is fulfilled by the implementation. Because both generationand verification of this safety property are automatic, verification of implementations iseasier than deriving and verifying all safety properties that should be inherited from thespecification.FL, the host language of the verification tool, has enabled the quick prototypingof ST2FL because it is a general programming language. Moreover, it allowed us toincorporate new verification algorithms easily; for example, we have experimented withseveral variations of win derivation to observe the performance of different algorithms.Nevertheless, it is FL’s Boolean representation using OBDDs that is most helpful becauseChapter 7. Conclusion 72our verification strategies are based on Boolean manipulations. Additionally, ST providesa natural way to decompose ST programs into next state functions that makes ourverification strategies possible. The result is the new verification tool presented in thisdissertation — ST2FL.7.3 Future workA high priority for us is to evaluate whether or not the verification approach as suggestedin this thesis have better performance than the traditional symbolic model checkingapproach. The approach could be to implement a symbolic model checker, like the onedescribed in [11], in the way we implemented the algorithms presented in this thesis.This should be straightforward since FL is a general purpose functional language. Afterincorporation of the symbolic checker, we then can compare the two difference approaches.In Chapter 4, a win derivation algorithm is presented. This algorithm is by no meansthe best. In fact, different variations of the algorithm may serve different purposes.For example, we have designed a variation of the win derivation algorithm that “keepstrack” of the necessary information to allow counter-examples be generated. However,the version that produces counter-example is slower than a version that only gives a “yes”or “no” answer. In general, if we view a predicate, say Q, as the set of states in whichQ is satisfied, then the basic difference between various implementations is in the waythe “set” Q shrinks step by step until the “set” win(Q) is reached. Some variations ofthe win derivation algorithm converges to the “set” win(Q) faster than others. Althoughwe have tried several variations of the win derivation algorithm, including the ones thatconsider the order the transitions are applied, we believe that the best is still yet to bedesigned.We would like to extend ST2FL with algorithms that verify liveness properties. In [8],Chapter 7. Conclusion 73CTL (Computation Tree Logic) is introduced as a formalism to specify liveness properties.With liveness properties specified in CTL, hardware models can be model checked todetermine if the CTL formulas are satisfied. We believe that all CTL formulas can beverified, by simple extensions to the techniques described in this thesis. For example,our strategy for verifying safety properties with the win derivation algorithm presentedin Chapter 4 is equivalent to model checking the CTL formula AG. Additionally, theultima formulation presented in the same chapter could be viewed as equivalent to AF inCTL with the same fairness constraint imposed. We speculate that other CTL formulas,such as AX and AU, can be verified using some similar formulations as ultima. Forcompleteness, incorporation of fairness constraints is required. To handle fairness in ageneral setting, for example in programs with mixed constraints, is a topic worthy ofanother thesis.Bibliography[1] Alan J. Ru and David L. Dill “Efficient Verification with BDDs using Implicitly conjoined Invariants.” 5th International Conference, CAV ‘93. Lecture Notes in Computer Science 697. Springer-Verlag. 1993.[2] Alan J. Ru and David L. Dill “Reducing BDD Size by Exploiting Functional Dependencies.” 30th ACM/IEEE Design Automation Conference. 1993.[3] Alan Nu, David Dill, Andreas Drexler and Rang Yang. “Higher-Level Specificationand Verification with BDDs.” Fourth International Workshop, CAV ‘92. LectureNotes in Computer Science 663. Springer-Verlag. 1992.[4] C-J. Seger. “Voss— A Formal Hardware Verification System, User’s Guide.” February 1993.[5] Chandy, K. Mani. “Parallel Program Design: A Foundation.” Addison-Wesley Publishing Company, Inc. 1988.[6] David Harel, Hagi Lachover, Amnon Naamad, Amir Pnueli, Michal Politi, Rivi Sherman, Aharon Shtull-Trauring, and Mark Trakhtenbrot. “STATEMATE: A WorkingEnvironment for the Development of Complex Reactive Systems.” IEEE Transactions on Software Engineering. Vol. 16, No. 4. April 1990[7] David L. Parnas, A. John van Schouwen, and Shu Po Kwan. “Evaluation of Safety-Critical Software.” Communications of the ACM. Vol. 33, No. 6. June 1990.[8] E. M. Clarke, E. A. Emerson, and A. P. Sistla. “Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications.” ACM Transactionson Programming Languages and Systems. Vol. 8, No. 2. April 1986.[9] Fumihiro Maruyamma, and Masahiro Fujita. “Hardware Verification.” Computer.February 1985.[10] H. J. Touati, H. Savoj, B. Lin, R. K. Brayton, and A. Sangiovanni-Vincentelli.“Implicit State Enumeration of Finite State Machines using BDD’s.” ICCAD. 1990.[11] J. R. Burych, E. M. Clarke, K. L. McMillan, and K. L. McMillian. “SequentialCircuit Verification Using Symbolic Model Checking.” 27 ACM/IEEE Design Automation Conference. 1990.74Bibliography 75[12] K. L. McMillian. “The SMV system DRAFT.” February 2, 1992.[13] Kenneth L. McMillan. “Symbolic Model Checking: An approach to the state explosion problem.” Carnegie Mellon University. CMU-CS-92-131. May 1992.[14] Leslie Lamport. “win and sin: Predicate Transformers for Concurrency.” DEC Systems Research Center. Technical Report 17. May 1, 1987.[15] M. J. C. Gordon and T. F. Meiham. “Introduction to HOL: A theorem provingenvironment for higher order logic.” Cambridge University Press. 1993.[16] Mark R. Greenstreet. “Synchronized Transitions: pre-draft of a language manual.”March 11, 1993.[17] Michael C. Browne, Edmund M. Clarke, David L. Dill and Bud Mishra. “AutomaticVerification of Sequential Circuits Using Temporal Logic.” IEEE Transactions onComputer. Vol. C-35, No. 12. December 1986.[18] Nancy G. Leveson. “Software Safety: Why, What, and How.” Computing Surveys.Vol. 18, No. 2. June 1986.[19] Randal E. Bryant. “Symbolic Boolean Manipulation with Ordered Binary DecisionDiagrams.” Carnegie Mellon University. CMU-CS-92-160. July 1992.[20] Randal E. Bryant. “A Methodology for Hardware Verification Based on Logic Simulation.” Journal of the Association for Computing Machinery. Vol. 38, No. 2. April1991.[21] Randal E. Bryant. “Graph-Based Algorithms for Boolean Function Manipulation.”IEEE Transactions on Computers. Vol. C-35, No. 8. August 1986.Appendix AElevator controllerIn Chapter 6, a design of an elevator controller was described. The ST specification islisted here. It is followed by a FL session that verifies the properties mentioned in thechapter.The specification (top level cell elevator) accepts one parameter— the number offloors numOfFloors. It declares three cells, tester, motor and car, and three datarecords, carMove, cCarMove and catState:The data record carMove is the record of movement signals, representing the elevator movement commands, sent from the cell tester to the cell motor. The datarecord cCarMove is the record of movement signals, representing the “safe” movementcommands, forwarded from the cell motor to the cell car. The data record carStaterepresents the sensors signals sensed by the cell car (except the status signal block whichis arbitrarily generated by the cell tester). These sensors signals are readible by bothcells tester and motor.The cell tester generates commands to instruct the movement of the elevator. Inreality, the commands should reflect the control buttons pushed by the users. However,in the specification, arbitrary commands are generated in order to verify that the elevatorwill not get into unsafe situation regardless of the movement commands. (For this reason,the signal blocked is also generated by this cell.)The cell motor is an intermediate component between the “control” (the cell tester)that sends movement commands and the elevator car. It is supposed to examine the76Appendix A. Elevator controller 77commands sent by the “control” and forward those commands that would not put theelevator into unsafe situation to the elevator car model (the cell car).The cell car models the physical movement of the elevator door and the elevatorcar. The movement of the elevator door is modeled by the subcell door. It representsthe status of the door by the variable drPos which is the elevator door position rangingfrom 0 (closed) to DRPDSMAX (opened). The movement of the elevator car is modeled bythe subcell floor. It represents the status of the elevator by the two variables carPosand curFlr. The variable carPos reflects the elevator door position above a floor. It istreated as a “wrap-around” counter ranging from 0 to CARPOSMAX. When its value is 0,1 or CARPOSMAX, the elevator car is near a floor level; when the value is 0, the elevatorcar is at a floor level. The variable curFlr is the floor number the elevator is at. It isincrement when the elevator car is going up and carPos is equal to INCCP, which is aposition somewhere in the middle between two floors; it is decremented when the elevatorcar is going down and carPos is equal to DECCP, which is 1 greater then INCCP.The following is the ST specification of the elevator controller:(** * * * * ***** ****** * )(* DEFINITION MODULE *)(*********************)DEFINITION MODULE elevator;EXPORT elevator;TYPE ELEVATOR = CELL(STATIC numOf Floors: INTEGER);STATIC elevator: ELEVATOR;END.(*************************)Appendix A. Elevator controller 78(* IMPLEMENTATION MODULE *)(*************************)IMPLEMENTATION MODULE elevator;FROM useful IMPORT CellO, BoolFnO;TYPEFLRRNG(n: INTEGER) = INTEGER SUBRANGE 1. .n;CARMOVE = RECORD up, down, park, open: BOOLEAN END;CARSTATE =RECORDtop, bottom, near, stopped, closed, opened, blocked: BOOLEANEND;CAR = CELL(carMove: CARMOVE; carState: CARSTATE);MOTOR = CELL(carMove: CARMOVE; carState: CARSTATE; cCarMove: CARMOVE);TESTER = CELL(carState: CARSTATE; carMove: CARNOVE);(******************)(* CELL: elevator *)( ** * * * * * * * * * * ****** )STATIC elevator: ELEVATOR =STATIC(* maximum of door position *)DRPOSMAX: INTEGER = 4;(* maximum of car position *)CARPOSMAX: INTEGER = 5;Appendix A. Elevator controller 79( ** * * * * * * * * * * * )(* CELL: car(*************)STATIC car: CAR =STATE(* up/down counter of the floor number *)curFlr: FLRRNG(numofFloors);(* up/down counter of the door position *)drPos: INDEX(DRPOSMAX + 1);(* modulo-(CARPOSMAX+1) counter of the car position *)carPos: INDEX(CARPOSMAX + 1);C ******* * * **** )(* CELL door *)STATIC door: CellO =STATIC(* open the door? *)openDr: BoolFnO =BEGIN carMove.open AND (drPos < DRPOSMAX) END;(* close the door? *)closeDr: BoolFnO =BEGIN (NOT carMove.open) AND (drPos > 0) END;INITIALLY mit: BOOLEAN =(drPos = 0) AND(carState.closed = TRUE) AND(carState.opened = FALSE) ANDAppendix A. Elevator controller 80(carState.blocked = FALSE) AND(carMove.open = FALSE);BEGIN (* car.door *)<< openDr() —* drPos : drPos + 1 >> *<< carState.closed : FALSE >> *<< carState.opened : drPos = (DRPOSMAX - 1) >><< closeDr() —* drPos : drPos - 1 >> *<< carState.opened : FALSE >> *<< carState.closed := drPos = 1 >>END; (* car.door *)(***************)(* CELL: floor *)( **** ** ****** * * * )STATIC floor: CellO =STATIC(* ‘‘carPos’’ wrap value *)CPWRAP: INTEGER = CARPOSMAX + 1;(* ‘‘carPos’’ at which to increment ‘‘curFlr’’ *)INCCP: INTEGER = CARPOSMAX DIV 2;(* ‘‘carPos’’ at which to decrement ‘‘curFir’’ *)DECCP: INTEGER = INCCP + 1;INITIALLY mit: BIJOLEAN =(curFlr = 1) AND (carPos = 0) AND(carState.top = FALSE) AND(carState.bottom = TRUE) AND(carState.near = TRUE) ANDAppendix A. Elevator controller 81(carState.stopped = TRUE) AND(carMove.up = FALSE) AND(carMove.down = FALSE) AND(carMove.park = FALSE);STATIC(* at top floor? *)atTop: BoolFnO =BEGIN (carPos = 0) AND (curFlr = numOfFloors) END;(* at bottom floor? *)atBottom: BoolFnO =BEGIN (carPos = 0) AND (curFlr = 1) END;(* park the car? *)parkCar: BoolFnO =BEGIN carMove.park AND (carPos = 0) END;(* raise the car? *)upCar: BoolFnO =BEGIN(NOT (atTopO OR parkCarO)) AND carMove.upEND;(* lower the car? *)downCar: BoolFnO =BEGIN(NOT (atBottom() OR parkCarO)) AND carMove.downEND;BEGIN (* cär.floor *)<< upCarO —* carPos : (carPos + 1) MOD CPWRAP >> * C<< carState.near :=Appendix A. Elevator controller 82(CarPos < 1) OR (carPos >= (CARPOSMAX- 1)) >> +<< carState.top(curFlr = numOf Floors) AND (carPos = CARPOSMAX) >> +<< carState.bottom : FALSE >> +<< carState.stopped : FALSE >> +<< carPos = INCCP —÷ curFir : curFlr + 1 >> )<< downCar() —* carPos : (carPos- 1) MOD CPWRAP >> * C<< carState.near : carPos <= 2 >> +<< carState.bottom : (curFlr = 1) AND (carPos = 1) >> +<< carState.top : FALSE > +<< carState.stopped : FALSE >> +<< carPos = DECCP —* curFlr : curFir - 1 >> )<< (NOT upCarQ) AND (NOT downCarO) —÷carState.stopped : TRUE >>car.floor *)** ** * * ******** )(* CELL: motor*)(* ** ********** * * )STATIC motor: MOTOR =(* open the door? *)STATIC openDr: BoolFnO =BEGIN carMove.open OR carState.blocked END;(* can the car be moved? *)END; (*BEGIN (* cardoor() floor()END; (* carAppendix A. Elevator controller 83STATIC canMove: BoolFnO =BEGIN carState.closed AND (NOT openDrO) END;BEGIN (* motor *)<< cCarMove.open :openDr() AND carState.stopped AND carState.near >>* << cCarMove.down :canMove() AND carMove.down AND (NOT carState.bottom) >>* << cCarMove.upcanMove() AND carMove.up AND(NOT carMove.down) AND (NOT carState.top) >>END; (* motor *)C ** * * ** * ** * * ***** )(* CELL: tester *)C * ************** *STATIC tester: TESTER =BEGIN (* tester *)<< carMove.up : NOT carMove.up >>II << carMove.down := NOT carMove.down >><< carMove.park := NOT carMove.park >>II << carMove.open : NOT carMove.open >>II << carState.blocked := NOT carState.blocked >>END; (* tester *)STATEcCarMove, carMove: CARMOVE;carState: CARSTATE;Appendix A. Elevator controller 84ALWAYS safe: BOOLEAN = carState.stopped OR carState.closed;BEGIN (* elevator *)car(cCarMove, carState)II motor(carMove, carState cCarMove)II tester(carState, carMove)END; (* elevator *)END.The following is a verification session of the elevator controller::1/ safety: carState.stopped OR carState.closed (stated in the ST code):prove safe;“Bingo --- PROVEN!!”:1/ safety: carState.near OR carState.closedprove (carState:-”near” or carState:—”closed”);“Bingo --- PROVEN!!”:1/ safety: (drPos = DRPOSMAX) = (carState.opened):prove ((drPos equ DRPOSMAX) is (carState:—”opened”));“Bingo --- PROVEN!!”:1/ safety: (drPos = 0) (carState.closed):prove ((drPos equ ##0) is carState:—”closed”);Appendix A. Elevator controller 85“Bingo --- PROVEN!!”:1/ safety: ((1 < carPos) AND (carPos < CARPOSMAX)) XOR carState.near:prove (((##1 les carPos) and (carPos les CARPOSMAX)) xor carState:-”near”);“Bingo --- PROVEN!!”:11 safety: ((curFir = numOfFloors) AND (carPos = 0)) = carState.top:prove (((curFir equ numOfFloors) and (carPos equ ##0)) is carState:-”top”);“Bingo --- PROVEN!!”:1/ safety: ((curFir = 1) AND (carPos = 0)) = carState.bottom:prove (((curFir equ ##1) and (carPos equ ##0)) is carState:-”bottom”);“Bingo --- PROVEN!!”:1/ Note: AG Q win(Q) and EF Q —iwin(-iQ):11 path: carState.opened:ctlverify (AG (EF (ctl (carState:—”opened”))));“CTL VERIFIED!”:1/ path: carState.top AND carState.opened:ctlverify (AG (EF (ctl (carState:—”top” and carState:—”opened”))));“CTL VERIFIED!”:11 Note: the auxiliary transition is already added:1/ path: reached AND carState.bottom AND carState.opened:ctlverify (EF (ctl (reached and carState:-”bottom” and carState:-”opened”)));Appendix A. Elevator controller 86“CTL VERIFIED!”Appendix BTransition ArbiterIn Chapter 6, an implementation of a transition arbiter was described. The ST descriptionof this implementation is listed here. The top level cell, arbiter, has no parameters. Itdeclares three cells, abstract, client and arb, and two data records, ci and c2 whichare the interfaces between the clients (two instances of the cell client) and the arbiter(the cell arb).The cell abstract is the specification of the transition arbiter similar to the onelisted in Chapter 6. The cell client represents a client. It is the circuitry descriptionof “client 1”/”client 2” in figure 6.7. The cell arb is the circuitry description of the“transition arbiter” in figure 6.7. It declares two subcells, intern and signal. Thesubcell intern is the implementation of the internal arbiter (the circuitry description of“internal arbiter”). The subcell signal is the circuitry connecting the “internal arbiter”and “client 1”/”client 2” in figure 6.7.The client circuitry is simple, and it work as follows: If currently it is in the “idle”state (r = g d), then it can toggle r to make a request by taking transition c.1. Now,it is in the “requesting” state (—ir = g = d). As the privilege comes and brings it tothe “privileged” state (-ir = -‘g = d), it can either toggle d to release the privilege andget to the “idle” state by taking transition c.2 state, or it can toggle r to get to the“pending-done” state by taking transition c. 1. From the “pending done” state, d can betoggled to reach the “request” state again.The internal arbiter is level sensitive. If both vi and v2 are low, it keeps the grant87Appendix B. Transition Arbiter 88by setting both xl and x2 low. If any one of the vi and v2 are high, say vi, it grants bysetting xi high leaving x2 low. If both vi and v2 are high at the same time, an arbitrarychoice of one of xi and x2 will be set high. Assume that both vi and v2 are initially high;then both wi and w2 will be settle in high level, and both xi and x2 in low level. Now,if vi becomes high to make request, wi can be changed to low by taking transition i.1,disallowing w2 to be changed to low as long as vi keeps high. Then xi can be changedto high by taking transition i.2 to signal that the grant is given.The circuitry connecting the “internal arbiter” and “client i” / “client 2” is a bridgebetween a client and the internal arbiter. Basically, this bridge converts the transitionsignaling from a client to level signal to the internal arbiter, and vice versa. The transitionsignaling from a client is converted by three transitions, s.2, s.3 and s4, and the levelsignaling is convert back to the client by two transition s.1 and s.5. For example, assumethat the client is in the “idle” state initially, when r, g and d are low. If the client makesa request by changing r to high, then s will change to high too because x is low (grantnot given). Note that, g cannot be set to high because transition s.5 is disabled. Now, bytaking transitions s.. and s.3, both t and u change high. Because both t and u are high,transition s4 is enabled. By taking it, a request is made to the internal arbiter. Whenthe internal arbiter gives grant by changing x to high, the level of s can be propagatedsetting g high by taking transition s.5; and at the same time, transition s.1 is disabledto disallow si to reflect any change to r, until the grant is returned by a transition ofthe d signal.The following is the ST description of the transition arbiter implementation:** * * * * * * **** * *** * )(* DEFINITION MODULE *)C ** * * * * * * * * * * * ******** )Appendix B. Transition Arbiter 89DEFINITION MODULE arbiter;EXPORT arbiter; TYPE C = CELLO;STATIC arbiter: C;END.(* IMPLEMENTATION MODULE *)IMPLEMENTATION• MODULE arbiter;TYPE ArbiterClient =RECORDr, g, d: BOOLEANEND;TYPE P = FUNCTION(c: ArbiterClient): BOOLEAN;(* Function that tells if a client is privilege *)STATIC privileged: P = BEGIN (c.g = c.r) AND (c.d <> c.r) END;TYPE Arbiter = CELL(cl: ArbiterClient; c2: ArbiterClient);TYPE Client = CELL(c: ArbiterClient);** * * ****** * )(* CELL: client *)* * * * **** *** * )STATIC client: Client =Appendix B. Transition Arbiter 90BEGIN (* client *)<< c.r : NOT c.g >> c.1<< c.d : c.g >> c.2END; (* client *)** * * *** *** ** * )(* CELL abstract *)(*****************)STATIC abstract: C =(************)(* CELL arb *)(************)STATIC arb: Arbiter =BEGIN (* abstract.arb *)<< NOT privileged(c2) —* ci.g : ci.r >><< NOT privileged(cl) —÷ c2.g : c2.r >>END; (* abstract.arb *)STATE ci, c2: ArbiterClient;ALWAYS me: BOOLEAN = NOT (privileged(ci) AND (privileged(c2)));INITIALLY mit: BOOLEAN = me;BEGIN (* abstract *)arb(ci, c2)II client(ci)II client(c2)END; (* abstract *)(** ** ** * * * * * ***** )Appendix B. Transition Arbiter 91(* CELL arbiter *)C * * * * * *** ** ** *STATIC arbiter: C =(* *** ** * * * **(* CELL arb *)(************)STATIC arb: Arbiter =TYPE Inter = CELL(xi: BOOLEAN; vi: BOOLEAN;x2: BOOLEAN; v2: BOOLEAN);TYPE Signal = CELL(x: BOOLEAN; v: BOOLEAN; C: ArbiterClient);(* CELL: intern *)(***************)STATIC intern: Inter =STATE wi, w2: BOOLEAN;INITIALLY mit: BOOLEAN = wi AND w2;BEGIN (* arbiter.arb.intern *)<< wi := NOT (vi AND w2) >> i.1<< xi : NOT wi >> i.2<< w2 : NOT (v2 AND Wi) >> i.3<< x2 : NOT w2 >> i4END; (* arbiter.arb.intern *)(****************)(* CELL: signal *)(* *** * ** ** * * ** * * * )Appendix B. Transition Arbiter 92STATIC signal: Signal =STATE s, t, U: BOOLEAN;INITIALLY mit: BOOLEAN = NOT Cs OR t OR u OR v OR x);BEGIN (* arbiter.arb.signal *)<< NOT x —* s : c.r >> s.1<< t : s <> c.d >> s.2<<u:s<>c.g>> s.3<< t = u —* v : t >><< x —* c.g := s >> 8.5END; (* arbiter.arb.signal *)STATE ii, vi, x2, v2: BOOLEAN;BEGIN (* arbiter.arb *)intern(xi, vi, x2, v2)signal(xi, vi, ci)signal(x2, v2, c2)END; (* arbiter.arb *)STATE ci, c2: ArbiterClient;INITIALLY mit: BOOLEAN =NOT (cl.r OR cl.g OR ci.d OR c2.r OR c2.g OR c2.d);ALWAYS me: BOOLEAN = NOT (privileged(ci) AND (privileged(c2)));REFINE abstract: BOOLEAN = TRUE;BEGINarb(ci, c2)II client(ci)II client(c2)Appendix B. Transition Arbiter 93END;END.Appendix CArbiter — incorrect versionIn Chapter 6, an incorrect implementation of a transition arbiter was described. TheST description of this implementation is listed here. the incorrect transition arbiterimplementation is list in this appendix. The description consists of a single cell xarbwhich is the description of the incorrect transition arbiter of figure 6.9.The intended operation of this incorrect implementation is similar to the correct one(appendix B). The central difference is that the request to the internal arbiter (ul andu2) are generated by a transparent latch instead of a C-element. Correct operationrequires that the latch be disabled before a grant is issued. This is the purpose of theXOR gates that generate the t and y signals. Note that when, for example, signal dchanges the XOR gate that outputs y is excited. However, the gate that outputs t isexcited as well, and changing t disables the output transition on y. It is this race that liesat the heart of the error in this version, and it can be demonstrated that this circuit doesnot guarantee mutual exclusion when arbitrary gate delays are admitted. A completetrace that leads this incorrect implementation into a state that violates mutual exclusionis list in table 6.7. It consists of 38 state transitions.The following is the ST description of the incorrect transition arbiter implementation:( ** * * ** * * * * * * * * *** **** )(* DEFINITION MODULE *)** * * * ****** *** *** ** )DEFINITION MODULE xarb;94Appendix C. Arbiter — incorrect version 95EXPORT xarb;TYPE C = CELLO;STATIC xarb: C;END.(*************************)(* IMPLEMENTATION MODULE *)C ** * * * * * ** * * * * * *IMPLEMENTATION MODULE xarb;STATICxarb: C =TYPEArbiterClient = RECORD (* arbiter-client interface *)r, g, d: BOOLEANEND;P = FUNCTION(c: ArbiterClient): BOOLEAN;STATICprivileged: P = BEGIN (c.g = c.r) AND (c.d <> c.r) END;STATE(* interfaces to clients *)ci, c2: ArbiterClient;(* internal variables for client 1*)si, ti, ul, vi, wi, xi, yi, zi: BOOLEAN;(* internal variables for client 2*)s2, t2, u2, v2, w2, x2, y2, z2: BOOLEAN;ALWAYS me: BOOLEAN = NOT (privileged(cl) AND privileged(c2));Appendix C. Arbiter — incorrect version 96INITIALLY mit: BOOLEAN =(NOT (ci.r OR cl.g OR ci.d OR c2.r OR c2.g OR c2.d)) AND(NOT (si OR ti OR ui OR wi OR xi OR zi)) AND(vi AND yl) AND(NOT (s2 OR t2 OR u2 OR w2 OR x2 OR z2)) AND(v2 AND y2);BEGIN (* xarb *)(* the internal arbiter *)<< vi := NOT (Ui AND v2) >> 1<< wi := NOT vi >> 2<< v2 : NOT (u2 AND vi) >> 3<< w2 := NOT v2 >> 4(* internal signals for client ci *)<< NOT wi —* si := ci.r >> 5<< ti : si <> ci.g >> 6II << yi — ul : ti >> 7<< Wi —* xl : si >> 8II << yi : xl = ci.d > 9<< zi := yi = ci.d >> 10<< xi = zi —* ci.g : xi >> 11(* internal signals for client c2 *)<< NOT w2 —* s2 : c2.r >> 12<< t2 : s2 <> c2.g >> 13<<y2—*u2 :=t2>> 14<<w2—*x2 :=s2>> 15<< y2 : x2 = c2.d >> 16W << z2 : y2 = c2.d >> 17Appendix C. Arbiter — incorrect version 97<<x2z2—*c2.g:x2>> 18(* actions of client ci *)<< ci.r := NOT ci.g >> 19<< ci.d := ci.g >> 20(* actions of client c2 *)<< c2.r := NOT c2.g >><< c2.d c2.g >> 22END; (* xarb *)END.
- Library Home /
- Search Collections /
- Open Collections /
- Browse Collections /
- UBC Theses and Dissertations /
- ST to FL translation for hardware design verification
Open Collections
UBC Theses and Dissertations
Featured Collection
UBC Theses and Dissertations
ST to FL translation for hardware design verification Lee, Wing Sang 1994
pdf
Page Metadata
Item Metadata
Title | ST to FL translation for hardware design verification |
Creator |
Lee, Wing Sang |
Date Issued | 1994 |
Description | Due to the rapid advances of VLSI technology in the past two decades, complicated hardware designs are now practical and common. Such designs are difficult to verify. Traditionally, design validation had relied on simulation, but exhaustive simulation is impractical, and as designs get larger, simulation becomes more and more inadequate. In my research, I have developed rigorous, formal methods to verify hardware described in ST — a simple, intuitive hardware description language. This goal is achieved by translating hardware modeled in ST to an equivalent representation in FL — a general purpose functional language. With its built-in support for Ordered Binary Decision Diagrams (OBDDs), Boolean expressions can be easily and efficiently manipulated by FL programs. My research is mostly concentrated on safety property verification. Such properties assert that bad things don’t happen to the hardware designs. By using the weakest invari ant calculation algorithm designed, which is based primarily on Boolean manipulations, we are able to verify safety properties of ST programs efficiently. Moreover, a refinement rule is also defined. This refinement rule produces a safety property of an implementation description; it guarantees that all safety properties of its design specification also hold for the implementation. Consequently, we are able to verify a specification, and to verify that all subsequent refinements of the specification are suitable related. |
Extent | 1442871 bytes |
Genre |
Thesis/Dissertation |
Type |
Text |
FileFormat | application/pdf |
Language | eng |
Date Available | 2009-02-26 |
Provider | Vancouver : University of British Columbia Library |
Rights | For non-commercial purposes only, such as research, private study and education. Additional conditions apply, see Terms of Use https://open.library.ubc.ca/terms_of_use. |
DOI | 10.14288/1.0051293 |
URI | http://hdl.handle.net/2429/5209 |
Degree |
Master of Science - MSc |
Program |
Computer Science |
Affiliation |
Science, Faculty of Computer Science, Department of |
Degree Grantor | University of British Columbia |
GraduationDate | 1994-05 |
Campus |
UBCV |
Scholarly Level | Graduate |
AggregatedSourceRepository | DSpace |
Download
- Media
- 831-ubc_1994-0283.pdf [ 1.38MB ]
- Metadata
- JSON: 831-1.0051293.json
- JSON-LD: 831-1.0051293-ld.json
- RDF/XML (Pretty): 831-1.0051293-rdf.xml
- RDF/JSON: 831-1.0051293-rdf.json
- Turtle: 831-1.0051293-turtle.txt
- N-Triples: 831-1.0051293-rdf-ntriples.txt
- Original Record: 831-1.0051293-source.json
- Full Text
- 831-1.0051293-fulltext.txt
- Citation
- 831-1.0051293.ris
Full Text
Cite
Citation Scheme:
Usage Statistics
Share
Embed
Customize your widget with the following options, then copy and paste the code below into the HTML
of your page to embed this item in your website.
<div id="ubcOpenCollectionsWidgetDisplay">
<script id="ubcOpenCollectionsWidget"
src="{[{embed.src}]}"
data-item="{[{embed.item}]}"
data-collection="{[{embed.collection}]}"
data-metadata="{[{embed.showMetadata}]}"
data-width="{[{embed.width}]}"
async >
</script>
</div>
Our image viewer uses the IIIF 2.0 standard.
To load this item in other compatible viewers, use this url:
https://iiif.library.ubc.ca/presentation/dsp.831.1-0051293/manifest