Verifying a Self-Timed Division Chip by Tarik Ono-Tesfaye Diplom, Universitat Wiirzburg, Germany,1995 A T H E S I S S U B M I T T E D IN P A R T I A L F U L F I L L M E N T O F THE REQUIREMENTS FOR T H E D E G R E E OF M a s t e r of Science in T H E F A C U L T Y OF G R A D U A T E STUDIES (Department of Computer Science) We accept this thesis as conforming to the required standard The University of British Columbia October 1997 © Tarik Ono-Tesfaye, 1997 In presenting degree freely at this the thesis in partial fulfilment of University of British Columbia, I agree available for copying of department publication this or of reference thesis by for his this thesis and study. scholarly or for her I further purposes gain permission; Department CQ?1?U (fcR. £Q£)JC£ of t h e University of British Vancouver, Canada Date DE-6 (2/88) OO l <, L Columbia , requirements that agree may representatives. financial the It shall h o t be that the by understood be allowed an advanced Library shall permission granted is for for the that without make it extensive head of my copying or my written Abstract T h e formal verification of asynchronous circuits is challenging, because they often have non-deterministic t i m i n g relations between circuit components. T h i s thesis presents a formal proof strategy for verifying the correctness of a dual-rail, asynchronous divider chip. F o r t h a t purpose, this thesis w i l l extend t i m i n g verification techniques t h a t were originally developed for c o m b i n a t i o n a l logic to apply to d u a l rail, self-timed designs. T h e proof strategy is refinement based and employs four progressively more detailed models of the divider. K e y safety properties are first established for the abstract models using model checking. These properties are then shown to hold for the more detailed models by verifying refinement between adjacent levels in the model hierarchy. Contents Abstract ii Contents i" List of Tables vi List of Figures vii Acknowledgements viii 1 2 Introduction 1 1.1 Related Work 2 1.2 Overview of Thesis 4 Background 5 2.1 The Division Chip 5 2.2 Synchronized Transitions 8 2.3 Definitions 9 2.3.1 State Sets and State Transition Relations 9 2.3.2 Speed Independence, Invariants and Safety Properties 2.3.3 Refinement . . . . 10 12 iii 3 Proof Strategy 1 4 19 The Word Level Models 6 4.1 Word Level Programs 19 4.2 Speed-Independent Word Level Program 22 4.3 Timed Word Level Program 23 4.3.1 Time Model 24 4.3.2 The Program 25 4.3.3 Simulation 26 4.3.4 Non-Zenoness 27 4.4 Proof of Refinement 27 5 The Transistor Level Model 31 5.1 6 Description of the Model 32 5.1.1 Data Representation 33 5.1.2 Implementation Details 37 5.2 Definitions 39 5.3 Proof of Refinement 47 5.3.1 The Abstraction Mapping A 5.3.2 Overview of the Proof 5.3.3 Timing Graph 5.3.4 The Abstract Programs P 5.3.5 P is a refinement of P a b 3 57 5.3.6 P i is a refinement of P w l 62 Q ti t 51 ( p t a b 3 > si Conclusion 6.1 48 t l ) W l i , w and P ( a b 3 T ^ ) ) \ ^ M i ) 5 3 55 65 Future Work 66 iv Bibliography Appendix A Source Code List of Tables 4.1 Speed-Independent D i v i d e r P r o g r a m 22 4.2 T i m e d W o r d Level P r o g r a m 25 5.1 Transistor Level P r o g r a m 33 5.2 Dual-Rail Full-Adder 40 vi List of Figures 2.1 Array of Stages "6 2.2 Structure of an Arithmetic Element 3.1 Proof Strategy 17 4.1 State Transition of the Arithmetic Array 20 4.2 Timing Diagram 21 5.1 Structure of A n Arithmetic Stage 32 5.2 Inputs and Outputs of A n Arithmetic Stage 34 5.3 Bit-Adder for Sum B i t 36 5.4 Bit-Adder for Carry Bit 36 5.5 2-Bit Full-Adder 41 5.6 Dependency Graph 45 5.7 Refinement Proof 52 5.8 The Abstract Stage 56 5.9 Hybrid Program 58 vii 7 Acknowledgements I a m very grateful to D r . M a r k Greenstreet for all his invaluable help and suggestions in getting this thesis done. T h r o u g h o u t the last two years he has been a very helpful and understanding supervisor. I'd also like to t h a n k C h r i s t o p h K e r n for the support i n using the proofchecker and my second reader, D r . A l a n H u , for his t i m e and patience, M a n y thanks to my parents as well, who have always been there for me. TARIK The University of British Columbia October 1997 viii ONO-TESFAYE Chapter 1 Introduction Recent well publicized and exorbitantly expensive mishaps due to software or hardware bugs such as the Intel Pentium floating point divider or the European Space Agency's Ariane 5 rocket have demonstrated the motivation for more formal, mathematically rigorous verification methods in hardware and software design — either as a supplement to conventional methods such as testing and simulation or as a replacement of those. In the hardware field, formal verification has started to gain acceptance in the past few years. However, not many industry relevant examples exist yet. Asynchronous circuits, which often have non-deterministic timing relations between circuit components, are especially challenging. Asynchronous circuits do not have a global clock to synchronize components; instead, signals that coordinate the actions of different components are derived internally. Self-timed designs have the potential of being faster than their synchronous counterparts because components in a self-timed design don't have to wait for a clock signal before starting their computation; more modular because communication is regulated by handshaking protocols 1 rather than global timing constraints; and more intellectually challenging because self-timed design is not as widespread as synchronous approaches. This thesis will identify a four level, refinement based, formal proof strategy for a dual-rail, asynchronous divider chip. The feasibility of the strategy will be demonstrated by proving two of the refinement relations. Although asynchronous circuits are often speed-independent, performance considerations have motivated a divider chip design that exploits timing relationships between different components. In verifying such a circuit, a method needs to be developed for introducing time into the specification and for formulating and verifying timing constraints. This thesis will extend timing verification techniques that were originally developed for combinational logic to apply to dual-rail, self-timed designs. In the division chip considered here, the fact that the computation iterates around an array of arithmetic elements presents additional complexity to the timing verification, as the timing dependencies are circular. To overcome that, the proof strategy exploits the fact that the dual-rail, precharged circuit has monotonic transitions in the precharging and evaluation phase. Synchronized Transitions, a concurrent programming language, was used to model the division chip, as it provided a natural way to describe the nondeterministic next state relation of the self-timed chip. 1.1 Related Work After the Intel Pentium floating point divider bug, several papers were published that dealt with the verification of SRT division and synchronous division chips. Ruefi et al. [13] verified the general SRT division theory using the theorem proving system P V S [12]. They then extend the proof to a simple SRT divider implemen2 tation. Bryant [3] demonstrates how BDD-based verification can be used to verify one iteration of a radix-4 SRT division at the bit level. He first generates a "checker circuit" that determines if the inputs and outputs of the divider, modeled at the gate level, satisfy the desired arithmetic properties. "Checker circuits" have the advantage that they can be reused, but they can be much larger than the actual circuit that is being verified and errors can be introduced in their construction. Both of these papers deal with clocked circuits without timing constraints between components that need to be verified. A methodology for designing and analyzing speed-independent asynchronous circuits is described by Spars0 and Staunstrup [15]. Their design technique uses a compositional approach, where pipelines and rings are composed to create multi-ring structures. They show that is possible to analyze the performance of such multi-ring based asynchronous circuits, even for non-trivial designs. Lee et al. [9] show how more general asynchronous circuits can be modeled in ST (see 2.2) and then verified using B D D s . Their verification is based on the automatic derivation of an invariant that guarantees a desired safety property of the circuit. The first part of the proof in this thesis is based on their approach. However, for the larger divider model used here, their approach is impractical, as will be shown later. There have been other asynchronous SRT division chip implementations described in the literature. Williams and Horowitz [20] describe a modified divider chip from the one considered in this thesis. Their design uses five arithmetic stages rather than three, which allows overlapping execution in the stages. In their fivestage design, control and precharging overhead are fully overlapped by evaluation of quotient bits and partial remainders. The authors claim that this leads to "zerooverhead" : an iterative design that is much smaller than a full combinational array 3 and divides as quickly. T h e precharging and return-to-zero encoding of this dual-rail d y n a m i c circuit leads t o increased power c o n s u m p t i o n . F o r t h a t reason, M a t s u b a r a and Ide [11] combine a single-rail static circuit w i t h a dual-rail d y n a m i c circuit w i t h o u t c o m p u t a t i o n t i m e penalty. T i m i n g verification has attracted much attention i n the real-time systems c o m m u n i t y . In real-time systems the correctness of the system depends not only on the value of the result of a c o m p u t a t i o n , but also on the t i m e at which the result was computed [16]. A self-timed chip that is not speed-independent this definition a real-time system. represents by Henzinger et a l . [8] extend t e m p o r a l logic to allow the verification of t i m i n g constraints in real-time systems while B e r t h o m i e u and D i a z [2] use time Petri nets, an extension of P e t r i nets w i t h lower and upper t i m i n g bounds for transitions, for modeling and verifying real-time systems. 1.2 Overview of Thesis T h e next chapter introduces n o t a t i o n and terminology used in this thesis and describes the divider chip. C h a p t e r 3 then delineates the p r o o f strategy developed for proving the chip correct. C h a p t e r 4 describes the asynchronous w o r d level models of the divider and the p r o o f t h a t the t i m e d model is a refinement of the speedindependent model. T h e detailed transistor level model of the divider is presented in chapter 5 and it is proven t h a t it is a refinement of the t i m e d word level model. C h a p t e r 6 summarizes the results of this thesis and suggests possible extensions to this research. 4 Chapter 2 Background This chapter describes the division chip verified in this thesis and establishes the theoretical foundations on which this thesis is based. The S R T division chip is described in the next section and the following section gives a short introduction to S T , the language in which the divider was modeled. Section 2.3 then defines terminology used in this thesis. 2.1 The Division Chip The divider chip implemented by Ted Williams et al. [18] implements radix-2 SRT division for floating point numbers. In SRT division, unlike the common "paper and pencil" method, the quotient digits are chosen out of a redundant digit set. This means that there is more than one representation of the quotient. In irredundant division it is necessary to compute the entire partial remainder before the next quotient digit can be determined. The main advantage of using a redundant quotient representation is speed. Because of the redundancy, an approximation of the partial remainder can be used to compute the next quotient digit. It is thus not necessary to 5 propagate the carry value across the entire length of the remainder, but rather only a fraction thereof (see [5] for details). A "small mistake" in the choice of the quotient digits due to the imprecise approximation can be corrected in later iterations. Quotient Output Registers Dividend Arithmetic Element Remainder Quotient Quotient Quotient Arithmetic Element 0 1 Arithmetic Element 2 Remainder Figure 2.1: Array of Stages The divider chip consists of an array of three arithmetic elements (henceforth also referred to as stages), over which the computation is iterated (see figure 2.1). Each arithmetic element determines one digit of the quotient and the next partial remainder. The cyclic computation around this array continues until the arrival of a completion signal, which is generated by the shift registers that hold the quotient digits. All the signals that control the speed of the elements are derived from within the array. There is no global clock; thus, the array is self-timed. For performance, the arithmetic elements use precharged function block logic. Each element can be in one of the three states, precharging, evaluating or holding. When a stage is precharging, all its signals are reset to low. During the evaluation state, the stage determines the next quotient digit and the next partial remainder. A stage is in the holding state when it is simply holding its output 6 unchanged for its successor stage. When one stage completes its evaluation (i.e. it has determined the next partial remainder and the next quotient digit), precharging in its predecessor stage is enabled. Furthermore, the precharge signal of its successor stage is removed to enable evaluation in that stage. For example when stage 1 has determined its partial remainder and its quotient digit, precharging in stage 0 is started. Next, the precharge signal of stage 2 is removed to start the evaluation. This control logic is explained in more detail in section 4.1. P b(i) • sum(i) sum(i-l) ' carry(i-l) • carry(i) CSA divisor • 0 • MUX - divisor " CPA qiiotient(i-l) • QSL quotient(i) Figure 2.2: Structure of an Arithmetic Element Figure 2.2 depicts the structure of the arithmetic elements. They consist of a multiplexer, a 55-bit wide carry-save adder, a 3-bit wide carry-propagate adder and the quotient selection logic. During evaluation, the multiplexer chooses — based on the quotient digit of the previous stage — either the divisor, the negative of the divisor or zero. The multiplexer output is added in the carry-save adder to the carry and sum from the previous stage. This result is the new remainder. When the top three bits of both carry-save adder outputs (the carry and the sum output) have been determined, their sum is computed in the carry-propagate adder. The 7 quotient selection logic then determines the next quotient digit based only on these three digits (see [19] for details). 2.2 Synchronized Transitions A l l the divider chip models were w r i t t e n i n Synchronized Transitions ( S T ) , a hardware description language (see [17]). In S T , a c i r c u i t is modeled as a collection o f state variables a n d a set o f transitions. A transitions has the form Ti =< Gi -»• Mi >, where Gi is the guard and M,- the multi-assignment of the transition. T h e guard is a Boolean valued expression a n d the multi-assignment can be executed only i f the guard is satisfied. A t r a n s i t i o n is said t o be enabled, i f its guard is satisfied. F o r example <C a A b —> x, y := y, x » is a transition w i t h the guard a A b a n d the multi-assignment x,y •:= y,x. T h e transition is enabled t o swap the values o f x a n d y i n p r o g r a m states where a Ab holds. Transitions are executed atomically, i.e. the evaluation o f the guard a n d performing the multi-assignment is a single indivisible operation. Transitions can be combined using the asynchronous combinator, ||. A t each step i n p r o g r a m execution, a t r a n s i t i o n is selected non-deterministically amongst those t h a t are enabled. F o r example, given the following p r o g r a m : < a ->• c := d > || <6->-c:=e>, 8 from if only one of a or 6 holds, the corresponding multi-assignment will be executed. If however both a and b hold, one of the transitions will be chosen arbitrarily. ST provides two other combinators that can be used in synchronous models. These are not used in this thesis. A description of these operators is given in [17]. 2.3 2.3.1 Definitions State Sets and State Transition Relations Definition 1 (State Space) The state space V of a ST program P with the vari- ables VQ, VI, ..., v is defined as D(v ) X D(v{) x . . . X D(v ), the cross product of n 0 n the variable domains. D e f i n i t i o n 2 (Initial State P r e d i c a t e a n d Initial State Set) An initial state predicate QQ is a Boolean predicate over the state space V. The initial state set Q is the subset ofD that satisfies QQ. A state that satisfies the initial state predicate is an initial state. Definition 3 (State T r a n s i t i o n R e l a t i o n ) Given a program TQ \\T\\\ ... \\ Tm and a set of states S C V, the state transition relation TZ C V X V is defined as: Vs,s'e<S : (s,s')eTZ 3{ : Gi(s) As - Mi(s), where Gi denotes the guard and Mi the multi-assignment of transition The set of reachable states is defined as the subset of the state space that can be reached from a state satisfying QQ after executing a finite number of transitions: 9 Definition 4 (Reachable States) Let P be a ST program with the initial set Q C V and the state transition defined recursively • IfseQ relation states, S, is by: then s G S. • If s G S and (s, s') 6 TZ, then s' £ S. • No other states are in S. 2.3.2 TZ. The set of reachable state Speed Independence, Invariants and Safety Properties In the following definitions P denotes a ST model of a circuit with • the set of transitions T = {T , T ..., T } where T =< G{ 0 u n { M > ; the t transitions are combined asynchronously, • the set of reachable states <S, • the state transition relation TZ defined by S and T, • the initial state predicate of the program QQ. A variable is read by a transition T,-, if it appears in its guard G ; or on the right side of its multiassignment Mi. A variable is written by a transition T;, if it appears on the left side of its multiassignment Mi. Let r[Ti) denote the set of variables read by transition T,- and w(Ti) the set of variables written by transition Ti. A property of P is an invariant of P if once it holds in one state of P it holds in all subsequent states of P. A safety property of P is a predicate that holds in every reachable state of P. This is formalized in these two definitions: 10 Definition 5 (Invariant) I is an invariant of program P iff V(s,s')-eK : I(s) =>• I(s') Definition 6 (Safety Property) Q is a safety property of program P iff : Q(s) VseS A p r o g r a m P is said t o be speed-independent i f once a t r a n s i t i o n is enabled, i t remains enabled u n t i l i t performs some action and its multiassignment is not affected by other transitions. M o r e formally: Definition 7 (Speed Independence) A program P is speed-independent V s , s eS V? iff : : = 0 (s,sO € n A Gi(s) A (s ^ Mi(s)) (8 = Mi(8)) V (Gi(s') The A V i / € w(Ti) : v(Mi(s)) = v(M (s'))) i stable inputs property implies speed-independence and states t h a t when a t r a n s i t i o n is enabled, none o f the variables t h a t i t reads are changed by other transitions: Definition 8 (Stable Inputs) Vs, s 6 S : V7 : =0 (s,s') eTZ A Gi(s) A => (s = (s^Mi(s)) Mi(s)) V ( V i / G r(Ti) : v(s) = v(s')) Speed independence and stable inputs are b o t h safety properties. 11 In this thesis, two methods are used to establish safety properties. In m o d e l checking, a sequence of sets of states, So, Si,... is constructed as shown below: Qo, Si Si-i if i U (RoSi-i), = 0, i f »" > 0 where noSi Note that l i m ; _ > 0 0 = {sev\ Si = S. 3seSi •. (s,s)en). F o r finite state systems, this fix-point is reached in a finite number of steps. Once S is thus c o m p u t e d , one can show t h a t Q is a safety property by verifying S => Q. In practice, it is often convenient to represent the sets of states s y m b o l i c a l l y using B D D s [4]. T h i s yields symbolic model checking. In this thesis, the t e r m model checking is used to refer to the s y m b o l i c approach. M o d e l checking has an advantage t h a t the verification can be completely automated. However, it is often infeasible for c o m p l e x designs due to the size of the state spaces i n v o l v e d . In such cases, the fixpoint calculation can be avoided if the designer can propose an invariant, I, such t h a t QQ => I and I = > Q. It is straightforward to show t h a t this establishes t h a t Q is a safety property. T y p i c a l l y , a designer finds the invariant I based on some i n t u i t i o n about the operation of the circuit. 2.3.3 Refinement T h e refinement property enables one to reason about the relationship of one prog r a m to another; t y p i c a l l y these are the specification and the i m p l e m e n t a t i o n m o d els. Refinement is defined under a function t h a t maps the states of one p r o g r a m t o those of the other p r o g r a m : 12 Definition 9 (Abstraction Mapping) An abstraction mapping m a p is a func- tion that maps a state from the state space of the implementation the state space of the to a state from specification: map = V ->• V imp spcc N o t e t h a t this m a p p i n g m a y be a p a r t i a l function. Definition 10 (Refinement) A program P with initial finement Q imp of a program P spcc with initial condition So condition Qi 0 under the abstraction is a remapping m a p , if map o Q io CQ So and V s , s € S : (s, s) e TZ imp (map(s) — map(s')) V ((map(s), map(s')) e where lZ, mp P i m p and lZ sptc are the state transition is thus a refinement of P 3pec relations of P imp 7l , spec and P . spec i f either the state of the i m p l e m e n t a t i o n before and the state after a t r a n s i t i o n m a p to the same state i n the specification or there exists an equivalent state t r a n s i t i o n i n the specification. Instead of proving safety properties on a detailed m o d e l , i t is often easier to prove the safety properties on a more abstract model and then to show t h a t the detailed model is a refinement of the abstract m o d e l . T h e following theorem states t h a t safety properties are preserved i n refinement relations. Theorem 1 If the program Pimp is a refinement abstraction mapping safety property map, of the program then for every safety property of Pimp- 13 Q of P c, spe P c spe under the Q ° map is a T h e proof of this theorem is straightforward a n d is o m i t t e d here. T h e next definition states how transitions of the i m p l e m e n t a t i o n c a n be matched against transitions i n the specification. T h e o r e m 2 then shows how transition m a t c h i n g can be used to show t h a t the i m p l e m e n t a t i o n p r o g r a m is a refinement of the specification (see [10]). D e f i n i t i o n 11 ( T r a n s i t i o n M a t c h i n g ) Let be a transition specification in the concrete implementation mp and P, pcc be the abstract program L^spec —— llj = l ^ ^ T, program is m a t c h e d against P spec Vs e S, mp : G (s) imp ( 3 i : G {map(s)) speCt P , 3pec • m a p iff =^ )V mp imp ^ ^^specj under the mapping ( map(s) = map(M, (s)) T h e function match(T , ^specj A (map(M, (s)) = mp map) denotes t h a t T i m p M (map(s))) j S speci is matched against P 3 p e c under the m a p p i n g map. Theorem 2 P imp is a refinement (Qi 0 is a of P, pec under the abstraction Qs o map) A (^Ai match(T , 0 =1 impi P , spec mapping m a p , iff map)) tautology. T h e o r e m 2 states t h a t if all transitions of the i m p l e m e n t a t i o n can be matched against transitions of the specification under the abstraction m a p p i n g map a n d i f (Qi => 0 14 Q SQ o map) holds, then P i m p is a refinement of P . spec straightforward and is o m i t t e d here. 15 T h e proof of theorem 2 Chapter 3 Proof Strategy T h i s chapter describes the proof strategy developed for verifying the correctness of the divider. T h e transistor level model of the divider is too large to permit m o d e l checking, and t o o complicated to verify from first principles using a theorem prover. Therefore it is desirable to prove safety properties on a less detailed, higher level model. A c c o r d i n g to theorem 1, i f the more detailed model is a refinement of the higher level m o d e l , the safety property w i l l hold i n the detailed model as well. T h e strategy described i n this chapter is based on the fact t h a t safety properties are preserved by a refinement relation. F o u r models of the divider, three w o r d level models and one detailed t r a n sistor level model, are used for the proof. T h e w o r d level models of the divider chip determine the quotient digits at the word level rather t h a n modeling the a c t u a l hardware of the chip at the gate level. T h e y o n l y implement the handshaking p r o t o c o l between the a r i t h m e t i c stages of the divider. T h e first model of the divider chip is a synchronous, deterministic m o d e l . T h e second model of the divider is asynchronous and has no t i m i n g i n f o r m a t i o n . T h e t h i r d p r o g r a m is a more accurate model of the 16 protocol between the stages and includes timing information. The transistor level program implements the entire transistor level logic of the divider stages. It has lower and upper timing bounds for all transitions. Synchronous Word Level Divider Model P, „ y functional correctness ch r e f i n e m e n t Asynchronous Speed-Indep. Word Level Divider Model P A r e f i n e m e n t ] Asynchronous Timed Word Level Divider Model P„, f r e f i n e m e n t ! Transistor Level Model P u Figure 3.1: Proof Strategy The proof strategy consists of five steps (see figure 3.1), which correspond to five proof obligations: (i) the synchronous, word level model P g y n c h of the divider divides cor- rectly; (ii) the asynchronous, word level model without timing properties P si a refinemnt of the synchronous model; (iii) P is speed-independent; si 17 is (iv) the t i m e d , w o r d level model F , is a refinement of the w speed- independent model P ; 3i (v) the transistor level model P tl model P w l is a refinement of the t i m e d w o r d level . T h e last three properties are proven i n this thesis, the first two properties are not proven a n d will be left for future w o r k . E v e n though this means t h a t this thesis doesn't prove t h a t the divider divides correctly, it w i l l show t h a t races or other t i m ing hazards cannot occur d u r i n g the operation of the divider. T h i s follows from the fact t h a t speed-independent circuits function correctly regardless of the internal delays of modules. If the transistor level model is a refinement of the speed-independent model, it follows t h a t the behaviour of the transistor level model must be explainable by the (speed-independent) behaviour of the speed-independent m o d e l . Obligations (iii) and (iv) are proven in chapter 4, w h i c h also includes detailed descriptions of the two asynchronous word level models. C h a p t e r 5 then proves t h a t P t l is a refinement of P w l . 18 Chapter 4 The Word Level Models This chapter focuses on the two asynchronous word level divider models - one without timing information and one with. In the first two sections, the two programs are described and the non-timed model is shown to be speed-independent. Section 4.3 then explains how time was modeled in the timed program and section 4.4 proves that the timed model is a refinement of the non-timed model. All the divider models were written in Synchronized Transitions. 4.1 W o r d Level P r o g r a m s The two higher level programs implement the control logic (i.e. the protocol) between the stages of the arithmetic array and determine quotient digits at the word level. Each arithmetic stage has a precharge_bar and a quotient_done signal as both input and output signals. The input prechargeJbar signal tells a stage when to precharge. When it is low, a stage precharges and sets the output quotient .done signal to low. The input quotient_done signal is generated by the previous stage when it has finished evaluating its quotient. For a stage to evaluate, both the input 19 p r e c h a r g e _ b a r signal a n d the i n p u t q u o t i e n t _ d o n e signal have t o be high. W h e n both are high, i t c a n set its o u t p u t q u o t i e n t _ d o n e signal to high. A stage c a n start precharging as soon as the following stage has finished evaluating its quotient, because the value t h a t i t is holding is not needed a n y m o r e . Consequently, the i n p u t p r e c h a r g e _ b a r signal t o stage i c a n be set t o low after stage i © 1 sets its o u t p u t q u o t i e n t _ d o n e signal t o high (the operators and " © " represent the a d d i t i o n a n d s u b t r a c t i o n operators m o d u l o 3, e.g. i © 1 means (i+l)%3). iMi.i- p!>(2) t- T ' FT T T TF 9(0) <- FF? T T TF) [ F T T T FF P Ho)«- F / »(°)«- ^ F F F T T wy^m «- T 9(2) \ [ T T T T FT) 9(1) [ F F T T TT) pb{l) <- F <r-T . [FF FT IT) [TT T F FF) ,(2) <- F / 9(1) < - F / \ p 6 ( l ) <- T 9(2) -r ^ < } L\-1MI III' FL J 6 ( 0 ) <- T P <-F [ T F F F TT) [TT FF FT) p 6 ( 2 ) <- F \p6(0)«-T f F F F F TT) H , E , P ] [TT FF FF) I T T F FT) ^ r — ' pi.(l) <-r TT FF T T 9(0) <- T F i g u r e 4.1: State T r a n s i t i o n o f the A r i t h m e t i c A r r a y E a c h stage can be i n one of the three states, precharging (P), evaluating (E) o r holding (H). F i g u r e 4.1 shows the state t r a n s i t i o n d i a g r a m of the divider. E a c h state is described by a six-tuple, which corresponds t o the values o f pb(0), q(0), pb(l), g ( l ) , pb(2) a n d q(2). T h e r e are three states i n which exactly one stage 20 is precharging (pb = FALSE), q — T R U E ) , one stage is evaluating (pb FALSE, and one stage is holding (pb = T R U E , q TRUE). = = T R U E , q = F o r example the state ( P , H , E ) in the figure refers to the state of the a r i t h m e t i c array where stage 0 is precharging, stage 1 h o l d i n g and stage 2 evaluating. T h e arcs in the d i a g r a m are labeled by the signals t h a t trigger the state t r a n s i t i o n and show the value of the signal after the t r a n s i t i o n . T h e input p r e c h a r g e J b a r signal of stage i is denoted as pb(i) and the o u t p u t q u o t i e n t _ d o n e signal as q(i). F i g u r e 4.2 depicts the t i m i n g d i a g r a m of the pb(i) and q(i) signals. E.P.H) P E.P.tl) (H-F.-P) (H,E,P b(0) q(0) P b(i) q(i) pb(2) r - fall lillll I|H1 q(2) prec large time evaluate time F i g u r e 4.2: T i m i n g D i a g r a m F i g u r e 4.2 is a t i m i n g d i a g r a m of the signals i n the divider. 21 < < < « © 1) -> pb(i) : = T R U E » p6(i 9 1) A q(i 9 1) p6(i), sum(i), carry(i), qbit(i) : = ->p6(i) ->• := FALSE » p6(«) A ->q(i © 1) - J sum(i), carry(i), qbit(i) := ->pb(i FALSE, FALSE, FALSE, 0 > TRUE, 5i?Ts«m(sum(« 0 1), carry(i9 1), q b i t ( z ' © l ) , divisor), SRTcarry(sum(.i Q 1), carry(i9 1), q b i t ( i © 1), divisor), SRTquot(sum(i Q 1), c a r r y ( i © l ) , q b i t ( i e l ) , divisor) > Table 4.1: Speed-Independent D i v i d e r P r o g r a m 4.2 Speed-Independent Word Level Program T h e S T implementation of the speed-independent p r o g r a m is given in table 4.1. T h e remainder value determined by stage i is represented using two bit-vectors, c a r r y ( i ) and s u m ( i ) , which correspond to the carry and s u m part of the remainder, q b i t ( i ) is the quotient bit determined by stage i. T h e first t r a n s i t i o n sets the p r e c h a r g e _ b a r signal of stage i to true, when the successor stage has its p r e c h a r g e _ b a r signal low and is consequently precharging. T h i s allows stage i to evaluate the next p a r t i a l remainder and quotient bit when inputs become available from stage iQl. T h e second t r a n s i t i o n enables precharging in stage i, when its successor has finished evaluating. W h e n precharging is started, each bit of the vectors c a r r y ( i ) and s u m ( i ) is set to FALSE. T h e quotient bit q b i t ( i ) is set to zero . W h e n the p r e c h a r g e _ b a r signal l It doesn't matter what values carry ( i ) , sum(i) and q b i t ( i ) are set to as long as these values are known. It is necessary to assign them known values for the proof that the transistor level program is a refinement of the word level program. The definition of the abstraction mapping depends upon these values. The variables are not read by other transitions while they hold this 1 22 is low, the q u o t i e n t _ d o n e signal w i l l get set to low by t r a n s i t i o n three. transition sets the q u o t i e n t - d o n e signal to TRUE s u m ( i ) and q b i t ( i ) using the functions SRTsum, T h e last and assigns values to c a r r y ( i ) , SRTcarry and SRTquot, which represent the operations of the S R T a l g o r i t h m . T h e second g u a r d , -*q{i © 1), is necessary to ensure the speed-independence of the p r o g r a m . It guarantees t h a t a stage will set its q u o t i e n t _ d o n e signal t o high after the successor stage has finished precharging (i.e. set its q u o t i e n t - d o n e signal to l o w ) . T h e i n i t i a l state predicate of the speed-independent w o r d level p r o g r a m is: Q = S0 pb(0).v A q(0).v A ->pb{l).v A ->q(l).v A pb(2).v A q(2).v T h e speed-independence of this p r o g r a m was shown using model checking. 4.3 Timed Word Level Program In the actual divider chip, precharge operations can be shown t o always take less time t h a n evaluation. A s seen in figure 4.1, when pb(i © 1) goes low, this enables precharging i n stage z © l . T h e same event enables setting pb(i) t o true. W h e n g ( i © l ) is FALSE (i.e. precharged), and pb(i) is true, then the g u a r d of the fourth t r a n s i t i o n is satisfied, and stage i can s t a r t evaluation. Because precharging is faster than evaluation, the design can be modified so t h a t evaluation starts as soon as pb(i) is true: evaluation will not complete u n t i l after stage i © l is precharged and the guard of the fourth t r a n s i t i o n is satisfied. T h i s allows precharging in stage i © 1 to overlap evaluation i n stage i, rather t h a n performing these t w o actions sequentially. By removing precharging from the c r i t i c a l t i m i n g p a t h , the performance of the divider is increased, values. 23 T h e arguments of the previous paragraph describe the i n t u i t i o n and m o t i v a t i o n behind the t i m e d design of the actual divider. T o verify the resulting design, the t i m e d design is modeled w i t h an S T p r o g r a m , and this p r o g r a m is shown t o be a refinement of the speed-independent 4.3.1 one. Time Model In the t i m e d word level program stages have bounds for precharge t i m e and evaluate t i m e . T h e next section describes how t i m i n g is used i n this p r o g r a m and how lower and upper bounds are implemented (see also [7], [1]). In the section thereafter the a c t u a l t i m e d program and its differences to the speed-independent p r o g r a m are presented. T i m e is modeled as a real-valued variable r and is part of the environment in w h i c h the programs operate. P r o t o c o l s describe the relationships between states before and after environment actions. T h e expression r.pre denotes the value of T before an environment action and r.post its value after the environment a c t i o n . W h e n it is necessary to distinguish the value of a variable before a state t r a n s i t i o n and after a state t r a n s i t i o n , the variable will appear w i t h the .pre and .post suffix. Variables t h a t are unchanged by the environment action or state t r a n s i t i o n generally appear w i t h o u t a .pre or .post field. In the timed divider model, only r can be changed by environment actions. In the t i m e d program the variables pb(i) and q(i) are now structures w i t h t w o fields, T and v. T h e discrete value of the variable is stored in v and the t i m e at which this value was assigned is stored i n r . T o add lower t i m i n g bounds to a t r a n s i t i o n in a S T p r o g r a m , an a d d i t i o n a l 24 { IliU I || <S —*pb(i © l).i> A —ipb(i).v —>• pb(i).v,pb(i).T < pb(i®l).v := TRUE, T » A g ( z © l ) . v A pb(i).v -> p6(i).w,p6(f).r,sum(i), c a r r y ( i ) , q b i t ( i ) F A L S E , T,F A L S E , F A L S E , 0 := » || -C -ip6(I).U A q(i).v -¥ q(i).v,q(i).T : = F A L S E , T » || < p&(I).V A -ig(i).i> A ( r > p6(i).r + T e v a l u a t e q(i).v,q(i).T, s u m ( i ) , c a r r y ( i ) , q b i t ( i ) ) ^ := T R U E , T, SRTsum(sum(i 0 1), c a r r y ( i © l ) , SRTcarry(sum(i 0 1), c a r r y ( i © l ) , qbit(i©l), divisor), qbit(i©l), divisor), SRTquot(sum(i © 1), c a r r y ( i 0 1), q b i t ( i © l ) , divisor) » Table 4.2: T i m e d W o r d Level P r o g r a m condition of the form T > (variable.r + T l o w e r b o u n d ) is added to its g u a r d . U p p e r t i m i n g bounds cannot be implemented in this way. Instead the protocol for the environment is changed to express these bounds. F o r example (var.v = TRUE) means t h a t var.v must change to 4.3.2 T.post < (var.r + T FALSE u p p e r b o u n d ) before r reaches the t i m e var.T+T nppeT b o u n d . The Program T h e transitions of the t i m e d word level p r o g r a m are the same as those of the speedindependent p r o g r a m , except for the last one (see table 4.2). T 25 e v a l u a t e is the m i n i m u m time i t w i l l take for a stage t o evaluate. N o t e how the last t r a n s i t i o n doesn't have -*q(i © 1) i n i t s g u a r d , unlike the speed-independent p r o g r a m . In a d d i t i o n t o these transitions we have a protocol t h a t states t h a t t i m e is monotonic a n d how long precharging w i l l take at most: Proto : r.pre < r.post A (q(i) A -ipb(i).v => r.post < (pb(i).T + T p r e c h a r , Tp ,charge is the m a x i m u m amount o f t i m e for precharging i n a stage. r< In the t i m e d p r o g r a m we make the following assumption about t i m i n g : •^timing • ( Tp h rge ^ T &\ .t ) A ( 0 <^ -^~p h g ) rec a ev ua rec e ar e ^timing states t h a t precharging takes less t i m e t h a n evaluating a n d t h a t precharging takes a positive amount o f t i m e . T h e i n i t i a l state predicate o f the t i m e d w o r d level p r o g r a m is: Qi 0 = pb(0).v A q(0).v A -^pb(l).v A ~>q(l).v A pb(2).v A q{2).v A (pb(2).r < pb(l).r) A (pb(0).r<T) A(g(0).r<r) 4.3.3 A (pb(l).r < pb(0).r) A (p&(l).r< r ) A A (gr(l).r < r ) A (pb{2).T<r) (g(2).r<r). Simulation W h e n s i m u l a t i n g t h e d i v i d e r p r o g r a m , t h e m o v i n g forward o f time is modeled by h a v i n g a r a n d o m number generator t h a t chooses a floating point value number as the "new" t i m e . T h i s t i m e has t o be greater t h a n the current t i m e . T h e p r o t o c o l is realized by p l a c i n g the value p 6 ( i ) . r + r p r e c h a r g e i n an array at the same t i m e aspb(i).v is set t o l o w . T h e array entry is deleted when q(i).v goes l o w . T h e m o d u l e t h a t 26 moves time forward looks at this array and chooses a real value t h a t is greater t h a n the current time but less t h a n the smallest time in the array. T h i s same m e t h o d is also applied when s i m u l a t i n g the transistor level divider. 4.3.4 Non-Zenoness A safety property t h a t allows the system to reach a state t h a t bounds the progress of time is called Z e n o (see [1]). Zeno specifications can be a source of incompleteness for proof methods. In this thesis formal proofs of Non-Zenoness are o m i t t e d . However, it can be shown t h a t in all t i m e d programs described in this thesis there is a lower b o u n d on the amount of time by which the upper bound is incremented. F u r t h e r m o r e , bounds on t i m e are introduced to assert upper bounds on the time between when a t r a n s i t i o n is enabled and when it performs its a c t i o n . T h i s means t h a t there is always a transition t h a t is enabled to remove the upper bound on the progress of time. 4.4 P r o o f of Refinement A c c o r d i n g to theorem 2, to prove t h a t the t i m e d p r o g r a m is a refinement of the speed-independent p r o g r a m it has to be shown t h a t each transition in the t i m e d program can be matched against a t r a n s i t i o n in the speed-independent L e t Pspec be the speed-independent program and P , - m p program. the t i m e d p r o g r a m . L e t A be a function from the states i n the t i m e d p r o g r a m to the states in the speed-independent program t h a t maps the variables pb(i).v and q(i).v of the t i m e d program t o the variables pb(i) and q(i) of the speed-independent p r o g r a m . In the speed-independent p r o g r a m any state change effected by a transition changes the .v field of at least one variable. State changes due to environment actions only 27 change the r value, and states t h a t differ only by their values for r m a p t o the same specification state. It follows t h a t : V ( s , s ) e TZ imp s ^ / ^ A(s) ^ A(s'). Since transitions cannot change r , showing t h a t the t i m e d program is a refinement of the speed-independent program is equivalent t o p r o v i n g : {Qio => Qs 0 V <C Gimp oA) A Mi V s € Simp • Gimp(s) ^3 ^ <^ Gspec ^ ^d-spec A A(M G {A(s)) spec t m p G Tspcc • (s)) = M s p e c (A(s))) T h i s follows directly from theorem 2. Since Qi Q 0 5 o o A and the first three transitions of the timed program are t r i v i a l l y matched by the first three transitions o f the speed-independent program, this is equivalent t o p r o v i n g t h a t whenever the t r a n s i t i o n < pb(i).v A (r > p6(i).r + T evalliate ) A -.g(i) -> q{i).v, q(i).T : = TRUE, r > is enabled, the t r a n s i t i o n < A ->g(z © 1) A - i g ( i ) ->• : = TRUE > in the speed-independent p r o g r a m is enabled as well. T h i s means t h a t the i m p l i c a tion pb(i).v A (r > p6(i).r + T =^ pb(i).v e v a l u a t e A -<q(i(Bl).v 28 ) A ->q(i).v A ->q(i).v has t o be a safety property of the timed p r o g r a m . T h e i m p l i c a t i o n can be rewritten as pb(i).v A ( r > p 6 ( i ) . r + T e v a l u a t e ) A q(i®l).v q(i).v. Theorem 3 Q s : pb(i).v A (T>pb{i).T +T ) evaluate A q(i®l).v q(i)-v is a safety property of the timed program Pi with the protocol P r o t o and the initial mp state predicate Qi . 0 Proof. Let Inv = 7,(0) A 7,(1) A 7i(2) A 7 (0) A 7 ( 1 ) A 7 ( 2 ) 2 2 2 A (/ (0) V J (l) V 7 (2)). 3 3 3 where /!(») = (( g ( i © l).v\t ( ( r > pb(i® l).r + -^evaluate ) A pb(i®l).v) A~<q(i).v A => ( r < pb(i).r ) pb(i).vj + -^evaluate) I (i) 2 = (pb(i).T < T) A {{pb(i).v A pb(i®l).v A -^pb(i Q l).v) ((p6(*'©l).r > p 6 ( i 0 1 ) . T ) A ( p 6 ( * 0 l ) . r >p6(i).r))) A A - i p 6 ( i © l ) . u A -ip6(z© l ) . u ) . 29 ((p6(i© l ) . r > pb(i).r) A [pb(i).T > pb(i® l).r))) / (i) = 3 (pb(i).v A -iq(i).v A pb(iQl).v V A -ipb(i®l).v A ?(?91).») A A ->pb(i®l).v A p6(iei).u A g(i91)-«) A^q(i®l).v V (pfr(i).t; A -i<7(i).u A - i p 6 ( i © l ) . u A-^(i©l).u A -ip6(J0 T h e clause J i is necessary to i m p l y the safety property a n d was derived using the invariant derivation m e t h o d described by Lee [10]. C l a u s e I? states the t i m i n g relationship between the p r e c h a r g e _ b a r signals and I3 is an enumeration of the possible states of the divider. U s i n g a decision procedure for predicate logic and linear inequality the foll o w i n g properties for I n v were proven: 1. Q =^ I n v 0 2. ( I n v A A 3. ( A t i m i n g 4. I n v Thus, Q s t i m i n g ) =^ wp(P , imp Inv) .pre A Inv.jore A P r o t o ) =>- Iiiv.post Q s is a safety property of P ; m p S as claimed. T h i s completes the proof t h a t _ P ; m p 30 is a refinement of P cspe Chapter 5 The Transistor Level Model The most detailed divider p r o g r a m t h a t was used to verify the correctness of the divider models the chip at the transistor level. T o increase the speed of the divider, the divider circuit design takes advantage of of two t i m i n g properties of the circuit. F i r s t l y , instead of having an explicit done detection where all the o u t p u t s of a stage are tested to see if they have been c o m p u t e d , only the o u t p u t of the quotient selection logic is tested. T h i s o p t i m i z a t i o n is based on the assumption t h a t the quotient selection logic will always take longer t h a n the carry-save adder. Secondly, it is assumed t h a t precharging takes less t i m e t h a n evaluating. T h i s means t h a t the o u t p u t s of a stage do not need to be tested to determine if the stage has finished precharging, when its predecessor stage has finished evaluating. These t i m i n g assumptions w i l l be proven in this chapter. T h e next section describes the transistor level model and section 5.2 defines n o t a t i o n used in this chapter. Section 5.3 then presents the proof t h a t the transistor level p r o g r a m is a refinement of the w o r d level p r o g r a m . T h r o u g h o u t this chapter the transistor level program w i l l be denoted by P , its set of transitions by T ti 31 ti and its set of variables by V . t l 5.1 Description of the Model P b(i) 1 C S A Done I sum(i-l) carry(i-l) sum(i) carry(i) C S A D o n e divisor qbit(i-l) M U X qbit(i) Q S L C P A Figure 5.1: Structure of A n Arithmetic Stage In the transistor level program P each arithmetic stage is modeled by one tl ST cell consisting of four sub-cells: • a multiplexer (MUX) • a carry-save adder (CSA) • a carry-propagate adder (CPA) • a quotient selection logic (QSL) which model the modules of the arithmetic elements as shown in figure 2.2. They operate as explained in section 2.1. In addition to these modules, there is a Done and a CSAJ)one module. The Done module determines when the stage has finished selecting a quotient bit and the CSAJ)one module determines when the carry save adder has computed all the sum and carry bits. Figure 5.1 depicts the structure of one arithmetic stage and the corresponding ST code is shown in table 5.1. If pb(i).v is FALSE, the module Done sets q(i).v and q s l _ d o n e to 32 FALSE. When pb(i).v is high, { IlLo i < || <C A -<pb(i).v -<pb(i(&\).v pb(i®l).v A q(i®l).v pb(i).v,pb(i).T - > pb(i).v,pb(i).T := TRUE,r > A : = FALSE, r > || M U X ( pb(i).v, q b i t ( i 0 l ) , d i v i s o r , muxout) || CSA ( pb(i).v, c a r r y ( i © 1), s u m ( i © l ) , muxout c a r r y ( i ) , sum(i) ) CPA( pb(i).v, c a r r y ( i ) , s u m ( i ) , cpsum ) II QSL( pb(i).v, cpsum, q b i t ( i ) ) II Done ( pb(i).v, II CSA-Done q b i t ( i ) , q(i), q s l _ d o n e ) ( pb(i).v, c a r r y ( i ) , sum(i), csa.done ) } Table 5.1: Transistor Level P r o g r a m q(i).v and q s l _ d o n e are only set to high after a quotient bit has been selected by the cell QSL. T h e signal csa_done is set to FALSE by CSA-Done if pb(i).v is FALSE, and it is set to T R U E , if all the sum and c a r r y bits have been determined. Both these modules are assumed to execute in zero t i m e and were introduced to simplify the proof. T h e y do not change the functionality of the d i v i d e r and are not read by any t r a n s i t i o n . In the remainder of this chapter, the .v n o t a t i o n of variables w i l l be d r o p p e d whenever it is obvious t h a t it is the variable value and not the t i m e at which it was assigned t h a t is referenced. 5.1.1 Data Representation In the transistor level m o d e l , a l l the d a t a except the quotient are encoded using a d u a l - r a i l code. T w o wires are used for d u a l - r a i l encoded signals. In the S T models, the variables t h a t represent these signals have t w o B o o l e a n valued fields, F and 33 T, with the following translation to truth values for the variable: x.T x.F value FALSE FALSE empty FALSE TRUE FALSE TRUE FALSE TRUE TRUE TRUE undefined During correct operation, no variable will have the undefined value. When a stage is precharging, all the variables are reset to empty, which in the hardware implementation corresponds to resetting all signals to low. While a stage is evaluating, a variable can only change its value from empty to F A L S E or T R U E . It cannot go back to the empty value. Consequently, if a variable has the value TRUE or FALSE, it will retain this value until the stage is precharging. Henceforth, the expression variable will not be used to refer to a dual-rail variable. Rather, it will be addressing a variable of the form x.T or x.F. divider pb i / '55 / '55 r 55 / sum(i-l) „ * 55 / carry / „ '55 '55 / (i-1) Arithmetic „ / / / / „ 55 / / . carry(i) 3 3 qbit(i-l) „ 55 Stage 55 ^ 00 „ / „ qbit(i) Figure 5.2: Inputs and Outputs of An Arithmetic Stage 34 The inputs and o u t p u t s of an arithmetic stage are depicted in figure 5.2. For the double precision floating point a r i t h m e t i c used in the divider, 55 bits are required to represent mantissas. D u a l - r a i l encoding doubles the number of wires to 110. T h e quotient is encoded using three wires ( q b i t _ , q b i t 1 0 a n d q b i t j , one wire for each of the three possible quotient values (-1, 0, 1). T o illustrate how transistor-level models using d u a l - r a i l encoding can be represented in the S T language, the following example describes the S T i m p l e m e n t a t i o n of an adder. E x a m p l e > T h e carry-save and carry-propagate adders used in the divider consist of one-bit full-adders, which operate in parallel in the carry-save adder and in series in the carry-propagate adder. T h e bit-adder determines the s u m bit and the c a r r y bit, b o t h of which are encoded in dual-rail. Precharged logic is used throughout the divider design. W h e n the pb i n p u t to a logic element is low, the p-channel pull-up transistor is turned o n , pulling the input of the inverter high, which then drives the o u t p u t low. W h e n pb is high, the input to the inverter w i l l be pulled low if there is a p a t h to ground t h r o u g h the network of n-channel transistors, and the o u t p u t of the inverter will go high. O t h e r w i s e , the i n p u t of the inverter remains high, and its o u t p u t remains l o w . P u b l i s h e d descriptions of the divider design do not include detailed designs for most functional blocks. Instead, we derived models for these blocks based on the d o c u m e n t a t i o n t h a t pre-charged logic was used and earlier discussions w i t h the designer. T h e design presented here should be representative of the a c t u a l design, but is probably not an exact replica. If the exact design were available, we expect t h a t the verification techniques described in this thesis would be equally applicable. F o r example, figure 5.3 shows a schematic o f the part o f the one-bit full-adder t h a t 35 -HE |f cin.F rin.T If j | ciu.Tjl cin.F Figure 5.4: Bit-Adder for Carry B i t Figure 5.3: Bit-Adder for Sum B i t determines the sum.T value of three dual-rail encoded inputs. T h e design is such t h a t the pull-up overpowers the pull-down chain. F o r example i f pb is low and a.T, b.T and cin.T are high, the inverter o u t p u t w i l l still be low. O n l y when the pull-up is removed can the output of the inverter become T R U E . T h i s approach produces a faster design at a cost of greater power c o n s u m p t i o n compared w i t h one where each pull-down p a t h includes a n-channel transistor controlled by pb. In S T , the one-bit full-adder can be modeled in the following way: || < ->pb < pb ->• sum.T A ((a.T Ab.T := F A L S E > Acin.T) V (a.F A ((b.T A cin.F) V (b.F A V (a.T A b.F A -> cin.T))) cin.F)) sum.T :— T R U E > T h e guard for the t r a n s i t i o n t h a t sets sum.T to true is constructed d i r e c t l y from the schematic: series connected transistors or networks are combined w i t h conjunction; parallel connections are represented by disjunction. T h e sum.F value is determined i n an analogous fashion, s u b s t i t u t i n g a . T , b.T, cin.T w i t h a.F, b.F, cin.F and viceversa. 36 Likewise, figure 5.4 shows a precharged logic element that computes cout.T. Its ST model is: || < -ipb ->• cout.T < pb A {{a.T A 6.T) V (a.T A cin.T) V (6.T A c m . T ) ) ->• cout.T := F A L S E := T R U E > > Each variable f in the transistor level program F , is written by exactly t l two transitions: one transition that sets the variable to FALSE. The notation T (u) and T TRUBM and G , i(v) and G T[a Eit (v) FALSEtti FALSE|tl TRUE and one that sets it to (u) will be used to refer to these transitions to refer to their guards. A l l transitions write only one variable. 5.1.2 Implementation Details Section 4.3.1 described how upper and lower bounds for transitions are incorporated into the word level program. Lower bounds were implemented by adding an additional constraint of the form (r > a.r) to the guard of a transition. Upper bounds are described in protocols. For simplicity, it is assumed that all the transitions in the transistor level model — except those of the Done and CSA-Done modules — have the same lower and upper bound for evaluating, once they have been enabled. These execution time bounds, which will be referred to as 8j ,a and #p , correspond x to the minimum and maximum gate delays. Similarly it is assumed that all gates have the same lower and upper time bound when precharging. These will be referred to as 7 y and yf - . As described above, disjunctions of variables in transitions of P in / a x ti represent transistors in parallel in the circuit and conjunctions represent transistors in series. Based on that observation, the enabled time of a transition T; with the 37 guard Gi is defined to be E(Gi), where 1/Q.T, max{z/o.T, E(v) = VI.T}, min{z/o.T, z^i.r}, if v VQ w i t h VQ £ V,t i t if v UQ iff i / o V f i , where UQ and 1/1 are either A and a variable of V i or a B o o l e a n formula t over variables i n V . t] The lower t i m i n g bound ( r > E(Gi) + <5f ) is added to the guard of each t r a n s i t i o n . in The m a x i m u m delay before transition T; executes once enabled is E(Gi) + 5™*- The protocol for the transistor level program is constructed using these upper bounds for transitions and the requirement T.pre < T.post, when an environment action occurs (see section 4.3.1). E(Gi) is not necessarily the time at which the guard Gi was enabled, as the actual enabling time depends on the values of the variables in the g u a r d . F o r example, given the transition < v Vv 0 if the values of b o t h VQ and V\ v := x 2 V2, >, are T R U E , then the guard is enabled at mm{y§.T, If'i/o is F A L S E , then the guard is enabled at V\.T, even i f V\.T > VQ.T. VI.T}. However, E(v) is an upper b o u n d on the time at which the t r a n s i t i o n w r i t i n g v becomes enabled. T h i s yields conservative upper bounds on the t i m e at which variables are updated. The model may a d m i t behaviours t h a t the real circuit does not. Because the correctness conditions for the divider are safety properties, the verification remains sound. 38 5.2 Definitions This section introduces notations and definitions used in this chapter. Some of the definitions will be specific to the transistor level program, others will be general and applicable to any ST program. To illustrate these, a dual-rail carry-propagate adder will be used throughout this section as example. Definition 12 (Notation) For a variable a of a ST program P with the set of transitions T, let • p(a) denote the set of variables that appear in the read set of transitions that write a: v £ p{a) W a 3 Ti E T : v £ r(T;) A a e w(Ti) C T denote the set of transitions that write the variable a, p be a predicate over p(a) W \p denote the set of transitions that can write a given that p holds. a p(a)\ p denote the set of variables that appear in the read set of transitions that write a, given that p holds: vep(a)\p O 3TieW \ a p : v£r(Ti) Example > The dual-rail carry-propagate adder depicted in figure 5.5 consists of one-bit full-adders as those shown in figure 5.3 and 5.4 and adds two dual-rail vectors, a = [ai, 02] and b = [b\, 62] and a likewise dual-rail encoded carry bit cin to produce a dual-rail sum vector sum and carry output cout (see 5.5). Table 5.2 shows the ST 39 < || ->pb -> c.T := FALSE > < pb A ( (01 .T A (bi .T V cin.T)) V (h .T A cin.T) ) C.T := T R U E > || <C ->pb || < pb A ( ( a i . F A {bi.FV cin.F)) V (b^.F A cin.F) ) ->• -> c.F c.F := := FALSE T R U E » > || < —>• sumi.T := || < p 6 A ( ( o i . T A {{h.F A cin.F) V ( & i . T A cin.T))) FALSE > V ( a , . F A ( ( 6 i . T A cm.F) V ( 6 . F A cin.T)))) ->• sumi.T := T R U E > —>• sum\.F :— F A L S E || <C || < p & A ( ( a i . F A ( ( 6 , . T A cin.T) V (&,.F A cin.F))) > V ( a i . T A ((61 . F A c i n . T ) V (b.T A cin.F)))) ->• sumx.F :— T R U E > || < -<pb -» sum .T || < p6 A ( ( a . T A ((6 .r A c . T ) V (6 .F A c . F ) ) ) := 2 2 FALSE > 2 2 V ( a . F A ((6 .F A c.T) V (6.T A c . F ) ) ) ) 2 2 ->• sum .T 2 :— T —>• sum .F R U E > :— F A L S E || <C || < p i A ( ( a . F A ( ( 6 . F A c . F ) V (6 .T A c.T))) 2 2 > 2 2 V(a .T A ((b .T A c.F) V (b.F A c.T)))) 2 2 ->• sum .F 2 := T R U E > || -ip6 ->• cout.T : = F A L S E > < p6 A ( (a .T A (b .T V c.T)) V (6 .T A c.T) ) || < || < p6 A ( ( a . F A (6 .F V c . F ) ) V (6 .F A c . F ) ) || <C 2 2 —• cout.T := 2 T R U E -» cout.F := 2 ->• cout.F > FALSE 2 := T R U E > 2 > T a b l e 5.2: D u a l - R a i l F u l l - A d d e r 40 pb cin.T cin.F • sum\.T Fullo,.Tai.F • sum\.F Adder i,.r- c.F bi.F- sumi.T sum^.F Full- a .T • a .F • b .Tb .F- Adder 2 2 2 cout.T 2 cout.F F i g u r e 5.5: 2 - B i t F u l l - A d d e r p r o g r a m for this adder. C o n s i d e r the variable c.T. T h e set p(c.T) = {pb, a i . T , & i . T , cin.T}, and the set W .T consists of the first two transitions. If the predicate —>p6 C holds, only the first t r a n s i t i o n is enabled to w r i t e c.T. Therefore, W . x | - . & contains c P o n l y the t r a n s i t i o n < -ipb -t Definition 13 (Input Variable) able that is not written c.T by any transition of P and is read by at least one All variables of P that are not input tk) such that Qo(to) relation 1Z, a trace is a sequence of states and (t,-_i, U) G TZ for i = 1, 2 , . . . , k. T h e set o f all traces is denoted by T(P,QQ). length k vari- Given a program P with the initial predicate QQ, the set of reachable states S and the state transition £2,..., transition. variables. Definition 15 (Trace) (to, t\, . An input variable of a ST program P is a vari- Definition 14 (Non-Input Variable) ables are non-input := FALSE > A trace t G T(P,QQ) i f it consists of a sequence of k states. T h e notation t is said to have k 41 w i l l be used to refer to a trace of length k and t\ to refer to the «-th state of the trace. The predicate settled(v>) evaluates to true if no transition writing v is enabled and all inputs to v are settled: Definition 16 (Settled Signal) If v is an input variable to a program P with the set of transitions T, then settled(v) If v is a non-input variable, = TRUE. then settled(v) =4> V T . S T W : € p(f) where G{ denotes the guard of the transition ->Gi A : settled(v ) T . t The next four definitions have mutually recursive definitions and are used to determine the time by which an internal signal will have settled. In a precharged circuit, signals can only change from FALSE to TRUE in the evaluation phase (i.e. when the precharge signal is low). That means that any transition that is enabled will set a signal to A transition that has a conjunction of terms in its guard TRUE. will always have to wait for the last one of these variables to be settled before it can be enabled. On the other hand, if a transition has a disjunction of terms in its guard, the transition can be enabled as early as the earliest settling time of either term. In the following: e(T\ ) is earliest time at which the guard of transition T p can be satisfied, and e(x\ ) is the earliest time at which expression x can become p true. Likewise, l(T\ ) p and l(x\ ) are the latest possible times for these events. The p earliest time at which variable v can be set to true given that p holds is given by min \ , u p and max \ u p gives the maximum time. Formal definitions are given below. 42 Definition 17 (Earliest Enabled Time) Let a be a non-input variable and let p be a predicate over p(a) such that W \ This transition and its guard by G. The earliest enabled time for transition a p will be denoted by T \ a p T\ Q P is denoted by e(T \ ) consists of only one element. and is defined as: a p e(T \ ) a p = e(G\ ) p where if v = i/o with VQ € p(ot), min \ Vo pi max{min \ , min Vo p i \p) e v = \ }, Vl { mm{min \ , p miny^p}, Vo p if v = vo A v\ and if v = VQVVI, variables of p(a) over variables and where where vo and v\ are either or Boolean formulas in p(a) defined below. Definition 18 (Latest Enabled Time) The latest enabled time for transition is denoted by l(T \ ) T\ a p and is defined as: a p l(T \ ) a p = l(G\ ) p where -„ max., 0 if v = i> with vo e ip, 0 ma,x{max | , max \ }, Vo p Vl p p{a), if v — Vo A v\ or v = VQ V v\, where vo and v\ are either a variables Boolean formulas and where miny \ 0 p and max \ Vo p of p(a) or over variables in p(a) are defined below. T h e m i n i m u m settling time is the earliest time by which settled(a) can hold and the m a x i m u m settling time is the time by which a signal must have settled. 43 Definition 19 (Minimum Settling Time) The minimum settling time of a, given that p holds is e(T \ ) a min \ a = p < p -\-Sf , if a is a non-input m 0, variable, otherwise Definition 20 (Maximum Settling Time) The maximum settling time of a, given that p holds is l(T \ ) a max \p = a p + 5j , if a is a non-input ax variable, < 0, otherwise Example > In the adder program (see table 5.2), T \ b and T \ b are uniquely a p a p determined for all a that are non-input variables. A s s u m i n g t h a t all internal signals have been precharged and have settled to and all i n p u t signals are stable FALSE (i.e. d o n ' t change their values) by the time the precharge signal pb goes high, the m i n i m u m time until settled(c.T) evaluates to true is the m i n i m u m t i m e it takes for the transition w r i t i n g c.T to be executed: min , \ c T pb = e(T . \pb) = e{pb c T + 6f a A -ic.T A ((oi.r A (b .T V cin.T)) V (b .T A cin.T))) + Sf" x x T h e m a x i m u m settling time for c.T is analogously max . \ b c T = P £f ax T h e sum variables sum2.T and sum^.F depend on the internal c a r r y variables c.T and c.F. T h e y are w r i t t e n by the n i n t h , tenth, eleventh and twelfth transition of table 5.2. After pb is set to min . \ sum T pb = TRUE, the m i n i m u m settling t i m e of sum2-T is e((oi.TA((ii.TAc.r)V(6i.FAc.f))) 44 V ( a i . F A {(h.F A c.T) V {b.T A c . F ) ) ) ) + Sf in = min{mm . | = mm{Sf ,5f } = 25f . c n T n , min _ \ } + 6f m p i ) c F pb + Sf n a < aT v m.F b .T x bi.F cin.T cin.F a .T 2 sumi.T SWTIQ.F a .F 2 b .T 2 b .F cout.T cout.F 2 F i g u r e 5.6: Dependency G r a p h F o r a variable a, the function />(<*) gives the predecessors o f a i n the dependency graph for the p r o g r a m . A t i m i n g graph is a dependency g r a p h annotated w i t h t i m i n g i n f o r m a t i o n . T h e dependency graph of the example adder p r o g r a m is depicted i n figure 5.6. In the dependency g r a p h , the nodes are the variables of the adder a n d a n arc exists from a node t o another, i f one of the nodes has the other as an i n p u t . 45 Definition 21 (Timing Graph) The timing graph of program P for the set of variables A under the assumption that p holds, denoted by G(P,A)\P> consists of the set of nodes N(p^\ , the set of arcs E(p^\ p p and the timing properties K(P,A)\P S U C A that • n £ N( )\ PtA • (P,A)\P - E <3> n £ A V 3a £ A : n £ p{ot)\ p p {(^1,^2) e V x V • V n : (n,min \ ,max \p) n p £ n I n E A 2 A ni £ p{n )\ } 2 P K(p )\ . jA p L e t T ] denote the set of transitions w i t h i n stage i of the transistor level t divider. These are the transitions i n the i-th i n s t a n t i a t i o n of the MUX, CSA, CPA, QSL a n d Done cells as well as the t w o transitions t h a t write pb(i). Stage i i n the divider is i n evaluation mode, when its precharge signal pb(i) is high a n d q(i) signal is low: Definition 22 (Evaluation Mode) pb(i) A ~<q(i). eval(i) T h e inputs t o stage i are stable, i f no t r a n s i t i o n from outside o f stage i is enabled t o w r i t e a variable w r i t t e n or read by a t r a n s i t i o n of stage i. Definition 23 (Stable Inputs) stable{i) « • ( V i ; eT -V, tl : Gj w{Tf) D (w(V,) U r ( 7 ^ ' ) ) = 0 ) L e t r(7l\) € V denote the set o f variables read by transitions i n T \ a n d let t ] t w{T2) G V i denote the set of variables w r i t t e n by T^. T h e expression for empty i n t the next definition stems from the fact t h a t a dual-rail encoded variable is empty, when b o t h its .T a n d .F field are FALSE. 46 Definition 24 (Empty Stage) empty(i) & (a £ w{T?,) =>• ->a.) The inputs to a stage are valid, if the quotient bit from the previous stage is valid and all dual-rail inputs are valid. A dual-rail valued variable is valid, if it evaluates to TRUE or FALSE and the quotient bit is valid, if exactly one of the wires representing the choices 0, 1 or -1 is high. Definition 25 (Valid Inputs) valid(i) O - Vi/.T, v.F e (r(73) - tw(73')) : iy.T A -.i/.F) V (-.i/.T A v.F) A 3j_ : qbit^i) A V 0 fc#j : -.qbit (») fe where the set r(T^) — w(T^) is the set of input variables of TJ. The next predicate states what the values of variables should be when they are settled after evaluating. Definition 26 (Settled Value) settlejval(i) <=> v € w(Tf ) : settled(v) A eval(i) t =$> v = G TRUE) ,;(v)) The predicates empty(i), stable(i), eval(i), valid(i) and settlejval(i) will ap- pear with a .pre and .post suffix, when it is necessary to distinguish their value before and after a state transition. The .r field denotes the time when the predicate last changed its value. 5.3 Proof of Refinement This section will prove that the transistor level program P is a refinement of the tl word level program P wl and is structured as follows. First a suitable abstraction 47 mapping will be defined and it will be discussed what obligations need to be shown for the refinement proof. In section 5.3.2 an overview of the proof will be given and the proof obligations will be proven in the remainder of this chapter. 5.3.1 The Abstraction Mapping A In the word level program all the bits of t l ) W l c a r r y ( i ) , sum(i) and qbit(i) are assigned values simultaneously and always have valid values. In the transistor level program each transition only writes one variable. This means that there are reachable states of P where some of the dual-rail encoded output bits of a stage are empty and tl others are TRUE or FALSE. The abstraction mapping between P and P tl wl needs to be defined in such a way that transitions writing variables of a stage appear as "stuttering" steps until all the outputs of this stage have valid values. In effect the abstraction mapping has to "hide" those states of the transistor level program that have output values that don't conform to those of P wl and only make the output of a stage "visible" when it has a valid value. Under this abstraction mapping, it then needs to be shown that the behaviour of the transistor level program is explainable by the behaviour of the word level program. Since the transistor level model uses dual-rail encoded variables and the word level model bit vectors (vectors of Boolean valued "bits") for the sum and carry values, the abstraction mapping of states in »S to states in S tl wi has to convert the dual-rail variables to Boolean values. An appropriate data abstraction for qbit has to be defined as well, since P uses three Boolean valued variables for each tl qbit(i) whereas in the word level program qbit(i) is one integer valued variable. Let / be a function that maps dual-rail variables of the transistor level stage to the corresponding variable in the word level program, with the following conversion of 48 d u a l - r a i l values to B o o l e a n : if - i x . T , FALSE, f (x.T, x.F) < [ T R U E , if X.T. F u r t h e r m o r e , let g be a m a p p i n g from the three transistor level q b i t ( i ) variables t o the integer valued q b i t variable in P -1, </(qbit(i)) Let A t l > w l = { if q b i t , ( i ) 0, else. be a m a p p i n g from states in the transistor level program P tl transistor level sum and w l . If pb(i) A q(i) holds for stage i, then to the carry variables of stage i are m a p p e d to the w o r d level carry variables using the function / and q b i t ( i ) is m a p p e d to ^ ( q b i t ( i ) ) . Otherwise, A sum and if q b i t . ^ i ) , 1, states i n the w o r d level p r o g r a m P sum and : w l t l ) W l maps the q b i t variables to the value 0 and all the transistor level carry dual-rail variables to FALSE. T h e variables pb(i) and q(i) are m a p p e d to the variables w i t h the same names in the word level p r o g r a m . T h e internal variables of the transistor level p r o g r a m are not part of the state space of P w l and are dropped by the abstraction m a p p i n g . Essentially, A t l i W l only makes the o u t p u t values of a stage "visible" when it is i n its holding phase. A l l transitions t h a t take place while a stage is precharging or evaluating appear as s t u t t e r i n g steps in the state space of P i and the o u t p u t w variables are mapped to t r a n s i t i o n in P MUX, t l FALSE and zero respectively. It follows t h a t i f a state from state s t o state s' is caused by a t r a n s i t i o n in one of the CPA, QSL or CSA-Done the abstraction m a p p i n g A t l ) V V l CSA, modules, both s and s' m a p t o the same s t a t e under . O n l y the transitions that change one of the 49 pb(i) or q(i) variables can lead to a state change at the w o r d level after the a b s t r a c t i o n mapping. T h e transitions T and T (q(i)) FAL5EM FALSE , ( g ( i ) ) both only have -ipb(i) i n their wl g u a r d and are identical. T h e transitions T (pb(i)) and T TRVEiti identical. A s for the t r a n s i t i o n T FALSEjtl TRUE>wl ( p 6 ( i ) ) are also ( p & ( i ) ) , its guard is identical t o the g u a r d of the corresponding w o r d level t r a n s i t i o n . N o t e t h a t after performing the transistor level t r a n s i t i o n , the abstraction m a p p i n g w i l l m a p the output signals of this stage to the FALSE vector and the value zero. These are the same values t h a t are assigned to the o u t p u t s by t r a n s i t i o n T FALSEW1 ( p 6 ( i ) ) at the word level. It follows t h a t the refinement obligation is t r i v i a l l y discharged for a l l state transitions except those where the value of q(i) changes from FALSE to TRUE. P r o t o c o l s are used in both programs solely to assert upper bounds on the times between when a t r a n s i t i o n is enabled and when it performs its a c t i o n . A tighter bound is more restrictive on allowed behaviours of the component modeled by the t r a n s i t i o n . Therefore, we require t h a t the protocol of the i m p l e m e n t a t i o n be at least as strong as the protocol of the specification. N o t e t h a t for b o t h programs, the protocols allow an unbounded advance of t i m e . Therefore, p r o v i n g that P ping Ai,wi t l is a refinement of P w l under the abstraction map- requires proving the following obligations: • W h e n a t r a n s i t i o n in P t l is enabled to set q(i) to high, the t r a n s i t i o n in P i w t h a t sets q(i) to high is also enabled. • F u r t h e r m o r e , it has to be shown t h a t after q(i) is set to high and the values of c a r r y ( i ) , sum(i) and q b i t ( i ) become "visible" under the abstraction m a p p i n g , these values agree w i t h the values c o m p u t e d by the word level p r o g r a m . 50 • T h e p r o t o c o l of P mapping A The t l ) W l t l implies the p r o t o c o l of P w l composed w i t h the abstraction . next section gives an overview of how these obligations will get dis- charged. 5.3.2 O v e r v i e w of the P r o o f The refinement proof will proceed as follows (see figure 5.7): • A t i m i n g graph of stage i of P is constructed and t i m i n g properties derived t l from i t . T h i s t i m i n g g r a p h represents stage i of P , d u r i n g its evaluation phase. t T i m i n g bounds for the quotient selection logic and carry-save adder can be derived from this graph as well as the i n p u t - o u t p u t relation of the c o m b i n a t i o n a l network implemented by the internal gates of the stage. These derivations are only valid under the assumption t h a t the following four properties hold: Qi : -*eval(i) A -iq(i) A G Q : eval(i) Q3 : the t i m i n g g r a p h is acyclic Q4 : i f eval(i), then only those transitions in 72 that set variables 2 (pb(i)) TRVEiii empty(i) => stable(i) to T R U E are enabled Qi states t h a t the stage i is e m p t y at the start of evaluation and Q 2 states t h a t its inputs are stable. Q3 can easily be verified using a graph traversal a l g o r i t h m and Q4 follows from Q. 2 • Since model checking the transistor level m o d e l is infeasible due to the large reachable state space, a speed-independent abstract p r o g r a m , P a bs, si) is constructed, a n d i t is shown t h a t Qi, Q 51 2 a n d Q4 are safety properties of P a b 3 ] s i . Asynchronous Timed Word Level Divider Model P„, • Speed-Indep. Abstract Model refinement .. valid(i) eval(i) =£• stable(i) -^eval(i) A ->q(i) A refinement refinement eval(i) G (pb(i)) m => empty(i) Timed Abstract Model Transistor Level Model P„ Figure 5.7: Refinement Proof The abstract program is described in section 5.3.4. In addition, the properties Q5 : eval(i) =>• valid(i) FALSE,tl ( < ? ( » ) ) => -.p6(i) TRUE.tl are proven to be safety properties of P a b 3 i si . These properties are needed to prove that P is a refinement of P . t l • A timed version of P w l a b 3 i 3i is constructed and it is shown that the timed program is a refinement of the speed-independent program. This proof is analogous to the refinement proof in chapter 4. • Next it is proven in section 5.3.5 that P is a refinement of the timed, abstract t l program. Consequently, safety properties of P • a b 3 are also safety properties of Subsection 5.3.6 completes the proof that P is a refinement of the word level t l program P . The timing properties derived from the graph as well as propw l 52 erties Q\ — Q7 are used in the proof. 5.3.3 £(p ,(r'))Ui(i) Timing Graph lw t t Assuming that a stage i is empty at the start of the evaluation and that all the variables read by transitions in are stable, the earliest and latest settling times for variables in w(T \) can be determined from the timing graph G'™^^^. This is t captured in the next theorem. T h e o r e m 4 If the following properties hold for P : l tl (i) —<eval(i) A —>a(i) A G TRUE,u(pb(i)) (ii) eval(i) empty(i) stable(i) (iii) the timing graph G(p (Ti ))\^ai(i) of stage i is acyclic (iv) if eval(i), then only those transitions in 7~*, that set variables to tlW l TRUE enabled then Property (i) is an assertion about the internal and output signals of stage i and states that they all have to be enabled. After T (pb(i)) rmeM FALSE, when the transition T (pb(i)) TRUBM is has executed, eval(i) will hold. Property (ii) states that when a stage is evaluating, all the inputs to the stage have to be stable. The last property follows from property (ii), because all transitions that set variables to FALSE have ->pb(i) in their guard, except the transition that writes pb(i) itself. Since 53 are pb(i) is an input to stage i, stable(i) implies that the t r a n s i t i o n T fal3e> tl ( p 6 ( i ) ) is not enabled. T h e proof of theorem 4 w i l l be o m i t t e d here, but it can be proven using an i n d u c t i v e proof over the depth of nodes i n the tree. T h e o r e m 4 applies t o any pipeline or ring structure t h a t uses dual-rail c o d i n g and precharged logic. T h u s , it provides a framework for verifying other designs in the same style of this divider. C o r o l l a r y 1 below specializes the theorem for application to the divider. Corollary 1 With the same hypotheses as theorem 4'- A A T h e theorem enables reasoning about the relationship between the t i m e when the signal csa_done goes high a n d when the q s l _ d o n e signal goes high. Since the transistor level divider uses only the o u t p u t of the QSL module to determine when a stage has finished evaluating, part of the refinement proof involves p r o v i n g t h a t the CSA module will always be finished by the time the q s l _ d o n e signal is set to TRUE. T h i s is stated i n the next theorem. However, for the signals csa_done and q s l _ d o n e to be settled does not i m p l y t h a t they have the value TRUE. T h i s only follows from the property t h a t valid(i) was true and is expressed i n theorem 6. Theorem 5 / / the four properties of theorem 4 hold for P , l a < then min, =>• (seri/ed(qsl_done) 54 seM/ed(csa_done)). This follows directly from theorem 4. Theorem 6 //, in addition to the four properties eval(i) holds for P\ it follows v eval(i) of theorem 4, =>• valid(i) then that => ( V v G w(TJ) => valid(i © 1) : settled(v)) and eval(i) => ( seM/ed(qsl_done) A =>• se^/ec?(csa_done) qsl.done csa_done) This theorem makes a statement about the relationship between inputs and outputs of a stage and follows from the settle-val(i) Theorem 7 The timing graph Q(p {T} ))\ tuW t predicate by Boolean algebra. of stage i is acyclic. Proof. This theorem is proven using a depth first search based algorithm on the graph. 5.3.4 & T h e Abstract Programs P a b S ) si and P a b s Two additional programs have to be constructed to prove that the transistor level model is a refinement of the word level program. They consist of three stages that have the same inputs and outputs as the transistor level stages, but they do not divide. The first one of these abstract programs, P a b a > ai is speed-independent and is used to derive safety properties for P . It doesn't have any timing information tl and can be model checked. The second abstract program, P , has the same timing abs bounds as P and is only used as an intermediate model to prove that the transistor wl 55 sum(i-l) CSA Don. qsl_done carry (i-1) sum(i) "CSA" carry (i) QSL Dond quolient(i-l) divisor X "QSL" quotientbit(i) Figure 5.8: The Abstract Stage level program is a refinement of P _ . ab3 si Both abstract programs have the same variables as the transistor level program and the same initial state predicate. Figure 5.8 shows the structure of an abstract stage. The cells " C S A " and "QSL" are in quotes, as they don't actually add correctly or select a quotient sensibly. Rather, each of the 55 carry and sum bits is assigned TRUE or FALSE nonde- terministically under the restriction that dual-rail pair cannot be set to undefined. A l l internal variables are also assigned values in this way. The quotient is nondeterministically set to -1, 0 or 1. During the precharge phase, all signals are set to FALSE. The abstract models, like the transistor level divider, also have q(i) signals that control the evaluation flow. In the abstract models this signal is only set to high after explicitly testing that all the outputs of a stage have valid values (see figure 5.8). In addition to testing that all outputs of a stage have valid values, P ->q{i © 1) in the guard of the transition that sets q(i) to high. 56 a b 3 i 3i has T h e o r e m 8 The following properties are safety properties of Pabs, si • 0 eval(i) => valid(i) (0 (ii) i=0 stable(i) ->eval(i) A -<q{i) A G (iii) ,(pb(i)) =>• empty(i) rRVE>t (iv) i=0 (v) Proof. eval(i) G , (q(i)) => ->pb(i) FALSE tl G ,u(pb(i)) TRms =>• ->q(i) All five properties were shown using model checking. O The timed abstract program has the lower timing bound r > p&(i).r+T evaluate in the guard of the transition that sets the q(i) signal to high and a protocol that specifies how long precharging will take at most. It includes upper bounds of the form for each variable v as well as for the signal q(i). The proof that P ab3 is a refinement of P ab3 , 8i is analogous to the refinement proof in chapter 4 and will not be described here. Since the interfaces between a stage of P ab3 and a stage of P are identical, tl one can easily exchange a stage of one program with that of the other. This property will be used in the next section to prove that P is a refinement of P . tl 5.3.5 P tl is a r e f i n e m e n t o f P ab3 a b s Instead of showing that the entire transistor level divider P is a refinement of the tI abstract program P , one stage at a time of P ab3 shown in figure 5.9. Let P J h ybrid ab3 is replaced by a stage of P , as tl denote the program that is obtained by replacing 57 Abstract Arithmetic Abstract Stage Stage Stage F i g u r e 5.9: H y b r i d P r o g r a m stage i o f -^hybrid) P a b w i t h a stage from 3 a -^hybrid n d hybrid a r e e a c n a P t It is then proven t h a t the h y b r i d programs l refinement of P a b 3 . A s the stages are identical, the proof is identical for a l l three programs. It follows then t h a t P of P a b 3 (see t l is a refinement [6]). In proving t h a t the transistor level program is a refinement of the abstract p r o g r a m , it is necessary t o use some of the safety properties of P it hasn't been proven yet t h a t cannot be utilized a priori. P t l is indeed a refinement of P a b 3 , a b 3 . However, since the safety properties T h e next theorem enables the use o f safety properties of a specification p r o g r a m i n proving t h a t an i m p l e m e n t a t i o n is a refinement of the specification. In the following let P 3 p e c (<S 3 p e c , TZ , <2o, ec) denote a specification p r o g r a m spec 3P w i t h the set o f reachable states <S , the state t r a n s i t i o n relation 7Z 3pec i n i t i a l state predicate <5o, ec- T h e i m p l e m e n t a t i o n p r o g r a m is denoted by sp T^impj Qo,im )P a n d the spec P i m p (>S i m p , T o simplify the n o t a t i o n , it will be assumed t h a t the state t r a n s i t i o n relations include a l l "stuttering" steps, i.e. V s € S of the i m p l e m e n t a t i o n is denoted by T h e o r e m 9 Given the T ( P i m p properties 58 , Qo,im )P : (s, s) € TZ. T h e set of traces (*) Q'(si) (ii) (iii) => ( ( s i , s ) G n 2 V s G <S W : spec V s G <S the implementation : 0iimp (VtoQ»pec(A(£f)) mp apec =• VjL 0 Q0,spec(M )) S P P, G TZ ) spec : Qo,,m (s) imp 2 SL Q (s) eT(P, ,Q ) mp A(s )) (A{ ), i m p is a refinement of the specification P spec under the abstrac- tion mapping A : Vs, s G S, mp : (s, s) G 1l imp =• ( (A(S), A(s') ) G P r o p e r t y (i) states t h a t the predicate Q' implies t h a t P imp P spec K ). spcc is a refinement of under the abstraction m a p p i n g A . P r o p e r t y (ii) states t h a t Q is a safety spec p r o p e r t y of the specification p r o g r a m . If property (iii) can be shown for a l l k, where is a n a t u r a l number, then it follows t h a t Q' is a safety p r o p e r t y of P i m p . T h e last property states t h a t i f s is an i n i t i a l state of the i m p l i c a t i o n p r o g r a m , its m a p p i n g A(s) is an i n i t i a l state in the specification P Proof. 3 p e c and thus a reachable state in T h e proof is an i n d u c t i v e proof over the length o f traces. shown t h a t the theorem holds for a l l traces of length 1. P . spec It w i l l first be T h e i n d u c t i v e step w i l l prove t h a t i f the theorem holds for traces of length /, it w i l l hold for a l l traces of length / + 1. B y the definition o f the set o f reachable states, it follows then t h a t the theorem holds for V s , s G <S imp w i t h (s, s) G 7 ^ i mp 59 Vi eT(P 1 i m p ,Q , 0 i m p ), : g , 0 i m p(io) => Qo, ec(A(i )) => A(tl) G S 3 P 0 spec => Q'(th) (A{t ),A{t\)) 0 en s p e c F r o m the last implication follows t h a t the m a p p i n g of t\ is also a reachable state i n P 3 p e c . Since Q 3 p e c ( A ( i ) ) and Q 0 3 p e c ( A ( i } ) ) holds, Q'(t\) must hold as well by property (in). A s s u m i n g that for a n a t u r a l number / it has been shown t h a t Q' holds for all states of all traces of length I a n d t h a t V': (A(tj.),A(tj. )) € 7 e 0 +1 3 p e c , it follows t h a t W + 1 eT(P i m p ,Qo, m p ), : Q'(t\ ) (A(t' ),A(t l\)) +1 +1 eR l l l 3pec S and w i t h property (iii) this implies t h a t Q'(iJ+j) holds. Since P A h y brid,ab3) a b 3 and P hybr id have the same variables, let the abstraction m a p p i n g which maps states from P h y b r i d t o states in P a b 3 , be defined as the identity function: Vs G £ h y b r T h e o r e m 1 0 The program P abstraction mapping A d : A hybr i d]ab3 ( s ) = (s). with the initial state predicate Qo,h brid is a refine- hybrid ment of the abstract program i y P { , with the initial a s ,. hybridiab 60 state predicate Qo,ab, under the P r o o f S k e t c h . T h i s theorem was proven using a proof checker. Instead of presenting the details of the proof here, only an overview of the strategy applied w i l l be presented. It suffices to show t h a t there exists a predicate Q'(s) erty Q (s) such that the first three properties of theorem 9 hold. A s by definition 3pec = Qo.hybrid and a safety prop- Qo.abs ° A h v b r i d i a b 3 , the last property holds trivially. For stage i of the abstract m o d e l , let the predicates of section 5.2 be defined in an analogous fashion and let Q spec P a b 3 be a predicate over the state space of p r o g r a m defined as: Qs ec{s) V? = P eval(i) => stable(i) =0 AV- ->eval(i) = 0 A V^_o A -iq(i) G A (pb(i)) eval(i) =$> valid(i). Let Q' be a predicate over the h y b r i d p r o g r a m P , j Q'(s) = eval(i) => empty(i) Tm]EM => valid(i) A stable(i) A + mm : settle-val(i) A ( r > eval(i).T + m a a ; A ( r < eval(i).r y b r i d c s a q ! l . . „ | „ , => csa_done) d 0 d o n 9 o e a | „ , e a w -iqsl.done) w P r o p e r t y (i) of theorem 9 is discharged by Boolean m a n i p u l a t i o n using a proof checker and property (ii) is a safety property of P _ ab3 If eval(i) evaluates to false, Q'(s) si and hence also of P is t r i v i a l l y true and property (iii) holds. t i m i n g graph analysis discharges p r o p e r t y (iii) for the states where eval(i) a b 3 The holds S (see theorems 4, 6 and 7). Let A be defined as the identity function over the set of states <S . t l ) a b 3 t] T h e o r e m 1 1 The program P„ with the initial state predicate Qo „ = Qo, b, ° A „ is a refinement state predicate straction . of program P , mapping ab A„ )(l6s with the initial . 61 t a ) 0 6 , Qo, b, under the aba T h i s follows from theorem 10 and [6]. 5.3.6 P t l is a refinement of P wl Theorem 12 The program P is a refinement of P under the abstraction u ml mapping Proof Sketch. T h i s refinement proof was also proven using a proof checker. O n l y a sketch of the proof w i l l be presented here t o give an i n t u i t i v e understanding of the proof. A s described i n section 5.3.1, these obligations must be discharged: (i) W h e n a t r a n s i t i o n i n P t l is enabled to set q(i) t o high, the t r a n s i t i o n i n P i t h a t w sets q(i) to high is also enabled. (n) T h e variables carry(i), sum(i) and q b i t ( i ) of P Ai.wi (iii) t l under the abstraction m a p p i n g have the same values as the variables i n P T h e protocol of P ti implies the p r o t o c o l o f P m l w l oA . t l ; W l . Obligation (i): Since P t l is a refinement of P a b 3 (see theorem 11), the previously proven safety properties of the abstract p r o g r a m are also safety properties o f P , subject t o the t l abstraction m a p p i n g . These safety properties then satisfy the assumptions o f theorem 4. It then follows t h a t Q'(s) is a safety property of P , where t l Q'(s) = V^_ 0 eval(i) =>• valid(i) A stable(i) A A (T > eval(i).T settlejval(i) + maa; IHJlin A (r < eval(i).r + m m . „ qsl 62 d0 , 8 csa_done) -iqsl.done). The variable q s l . d o n e is set to T R U E w i t h o u t any t i m e delay as soon as one of the q b i t variables goes high, hence i t follows t h a t V 2 t = 0 eval{i) =4> ( r < eval(i).r + min _„„„, V j _ -iqbit^i)) vi 0 F u r t h e r m o r e , the properties FALSE,tl * 2 = 0 => -.pft(i) (q(i)) ^TRUE.tl (p&(*)) =>• are safety properties of P for a b 3 ] 3 i and therefore of P t ! --ffW (see theorem 8). T h e y i m p l y t h a t , eval(i) t o hold, first g(i) must have been set t o false and then pb(i) t o high. It follows that V _ 2 and 0 eval(i) eval(i).r = pb(i).r that Vf_ eval(i) A q b i t ^ ( i ) 0 => r > pb(i).r + mzn . qsl d<in „ N o t e that according t o theorem 6 only one q b i t - ( i ) can have the value T R U E . The transition T (q(i)) TRVEM which sets q(i) t o T R U E i n the transistor level p r o g r a m is enabled iff exactly one of the q b i t ( i ) variables is T R U E and eval(i) mm,, .n. u >T e v a l u a t e , it follows t h a t (q(i)) where G TRUE holds. If G TRUE.wl , i ( g ( « ) ) is the guard of the transition setting q(i) t o T R U E in the word w level p r o g r a m . T h i s discharges obligation (i). Obligation (ii): The predicate settle-val(i) establishes a connection between the inputs and the out- puts of a stage. Based on this predicate, tautology checking using the proof checker 63 proved t h a t the values of the transistor level stage o u t p u t s were the same under the abstraction m a p p i n g as the values of the word level stages. Obligation (iii): T h e p r o t o c o l of P t l includes an upper bound for the t r a n s i t i o n t h a t sets q(i) to FALSE: ( r < pb(i).T + 7? ). (-ipb(i) A q(i)) Therefore, if *yf ax ax < T p r e c h a r g e ? the p r o t o c o l of P f the abstraction m a p p i n g A t l ) W l t l implies the p r o t o c o l of P and obligation (ii) is discharged. T h i s completes the p r o o f t h a t P t l is a refinement of P 64 w l . w l under Chapter 6 Conclusion T h i s thesis presented a refinement based proof strategy for verifying the correctness of an asynchronous d i v i d e r c h i p . D u e t o the large state space o f the transistor level m o d e l , a u t o m a t i c model checking is infeasible. Likewise, c o n s t r u c t i n g a proof from first principles i n a t r a d i t i o n a l theorem prover would be extremely t i m e consuming and tedious. T h i s thesis presented a p r a c t i c a l approach e m p l o y i n g four progressively more detailed models of the d i v i d e r . K e y safety properties are established for the abstract models using model checking. These properties are shown to hold for the more detailed models by verifying refinement between adjacent levels i n the model hierarchy. F u n c t i o n a l correctness of the divider is proven on the first, most abstract m o d e l , and the second model is shown t o be speed-independent. T h e p r a c t i c a l i t y of the strategy is demonstrated by p r o v i n g three out of the five steps t h a t constitute the correctness proof for the d i v i d e r . F u r t h e r m o r e , this thesis showed how different formal verification methodologies can be combined t o prove a c h i p design correct. T h e p r o o f strategy combined techniques from model checking, theorem p r o v i n g as well as t i m i n g verification using 65 graph based approaches to overcome the l i m i t a t i o n s t h a t each exhibits on its o w n . M o d e l checking was used to a u t o m a t i c a l l y prove safety properties on the abstract models and a t i m i n g graph was used to extract t i m i n g properties of the transistor level m o d e l . These were needed to prove t h a t its behaviour corresponds to the behaviour allowed by the word-level models. T h e aforementioned verification techniques were formalized as domain-specific decision procedures in a proof checker, w h i c h also includes general purpose decision procedures for propositional logic and linear equalities and inequalities. T h e proof checker ensured t h a t a l l pending proof obligations were discharged, and thus ascertained soundness of the proof, given the soundness of the decision procedures. T h e proof checker used for this research is still under development and the research presented in this thesis provided a significant example for its development. T h e first prototype of the proof checker was w r i t t e n in the F L language [14]. T h e proofs a t t e m p t e d here revealed performance problems in the first prototype; verifying speed-independence of the word-level m o d e l took several hours. A newer version, implemented in M L has significantly better performance; the proofs described in this thesis took only a few minutes. T o achieve this performance, it was necessary to specify good orderings for variables for the B D D based methods. V a r i a b l e ordering affects the performance but not the semantics of these decision procedures. Interfaces for specifying variable ordering were added to the proof checker in response to experience gained in developing the proofs presented here. 6.1 Future W o r k T o complete the proof of the divider proposed in chapter 3, two more steps are required. F i r s t , a suitable synchronous divider model needs to be constructed, 66 and it need to be proven t h a t its o u t p u t converges towards the quotient of the inputs. Second, it has to be shown t h a t the speed-independent word level model is a refinement of the synchronous m o d e l . It would furthermore be interesting t o a p p l y the research presented i n this thesis to other t i m e d chip designs. T h e proof strategy of this thesis was geared towards p r o v i n g this particular divider chip correct. A p p l y i n g the m e t h o d t o other t i m e d chip designs might lead to a more general description of the proof m e t h o d ology. F o r example extending the proof of the three stage divider to the five stage divider described in [20] could be a first step towards developing a general strategy in proving t i m e d chips correct. 67 Bibliography [1] Martin Abadi and Leslie Lamport. A n old-fashioned recipe for real time. In J . W . de Bakker et al., editors, Proceedings Theory in Practice". of the REX "Real-Time: Springer-Verlag, 1992. L N C S 600. [2] Bernard Bertholomieu and Michel Diaz. Modeling and verification of time dependent systems using time petri nets. IEEE gineering, Workshop, Transactions on Software En- 17(3):259-273, March 1991. [3] Randal E . Bryant. Bit-level analysis of an SRT divider circuit. Technical Report CMU-CS-95-140, School of Computer Science, Carnegie Mellon University, Pittsburgh, P A , 1995. [4] J . R. Burch, E . M . Clarke, D . E . Long, K . L . McMillan, and D . L . Dill. Symbolic model checking for sequential circuit verification. Technical Report C M U - C S 93-211, School of Computer Science, Carnegie Mellon Univeristy, July 1993. [5] Joseph J . F . Cavanagh. Digital Computer Arithmetic : Design and Implemen- tation. McGraw-Hill, New York, 1984. [6] Mark Greenstreet. Synchronized Transitions, 68 unpublished manuscript, 1997. [7] Mark R. Greenstreet. START. A Technique for High-Bandwidth Communi- cation. P h D thesis, Department of Computer Science, Princeton University, January 1993. [8] Thomas A . Henzinger, Zohar Manna, and A m i r Pnueli. methodologies for real-time systems. Temporal proof In ACM Symposium on Principles of Programming Languages, pages 353-366, 1991. [9] Trevor Lee, Mark Greenstreet, and Carl-Johan H . Seger. Automatic verification of asynchronous circuits. Technical Report TR-93-40, Department of Computer Science, University of British Columbia, Vancouver, November 1993. URL: http://www.cs.ubc.ca/tr/1993/TR-93-40.ps. [10] Trevor W . S. Lee. ST to F L translation for hardware design verification. Master's thesis, Department of Computer Science, University of British Columbia, April 1994. [11] Gensoh Matsubara and Nobuhiro Ide. A low power zero-overhead self-timed division and square root unit. In Proc. International Symposium on Advanced Research in Asynchronous Circuits and Systems. I E E E Computer Society Press, April 1997. [12] S. Owre, J . M . Rushby, and N . Shankar. P V S : A prototype verification system. In Deepak Kapur, editor, 11th International Conference on Automated Deduc- tion (CADE), number 607 in Lecture Notes in Artificial Intelligence, pages 748-752, Saratoga, N Y , 1992. Springer Veriag. [13] H . Ruefi, N . Shankar, and M . K . Srivas. Modular verification of SRT division. In R. Alur and T . A . Henzinger, editors, Computer-Aided 69 Verification, CAV '96, Lecture Notes in Computer Science, New Brunswick, N J , July 1996. SpringerVerlag. To appear. [14] Carl-Johan Seger. Voss — A formal hardware verification system: User's guide. Technical Report UBC-CS-93-45, Department of Computer Science, University of British Columbia, Vancouver, B C , 1993. [15] Jens Spars0 and J0rgen Staunstrup. INTEGRATION, Delay-insensitive multi-ring structures. 15(3):313-340, October 1993. [16] J . A . Stankovic. Misconceptions about real-time computing. IEEE Computer, 21(10):10-19, October 1988. [17] J0rgen Staunstrup. A formal approach to hardware design. Kluwer Academic Publishers, Boston, 1994. [18] T . E . Williams, M . A . Horowitz, R. L . Alverson, and T . S. Yang. A self-timed chip for division. In Stanford Conference on Advanced Research in VLSI, pages 75-96, March 1987. [19] Ted E . Williams and Mark A . Horowitz. SRT division diagrams and their usage in designing custom integrated circuits for division. Technical Report C S L - T R 87-326, Computer Systems Lab, Dept. of E E , Stanford, November 1986. [20] Ted E . Williams and Mark A . Horowitz. A 160ns 54 bit C M O S division implementation using self-timing and symmetrically overlapped SRT stages. In 10th IEEE Symposium on Computer Arithmetic, June 1991. 70 Appendix A Source Code c* * d e f i n i t i o n module f o r the main f u n c t i o n * of the timed word l e v e l program *) DEFINITION MODULE main; FROM types IMPORT BinNumber, BinElement, ResElement, ResNumb DRArray, ArrayOfDRA; FROM d i v i d e r IMPORT BinArray; EXPORT D i v i d e r ; TYPE I n t A r r a y ( n : INTEGER) = ARRAY(i: INDEX(n)): INTEGER; T = CELL(STATIC r e a l d i v i d e n d , r e a l d i v i s o r : REAL); F l = FUNCTION(binelem: BinElement): BOOLEAN; F2 = FUNCTION(binnum: BinNumber; n: INTEGER): BinArray; F3 = FUNCTION(binnum: BinNumber; n: INTEGER): IntArray; STATIC D i v i d e r : T; BinElemToBool: F l ; BinNumToBool: F2 ; BinNumToInt: F3 ; END. (* main *) 71 (* * implementation module f o r t h e main f u n c t i o n * of the timed word l e v e l program *) IMPLEMENTATION MODULE main; FROM s t r i n g l O IMPORT W r i t e S t r i n g ; FROM s t r i n g s IMPORT I n t T o S t r i n g , BoolToString; FROM FROM FROM FROM cast IMPORT round; mycast IMPORT Makebin, MakeString; d i v i d e r IMPORT D i v i d e r A r r a y ; h i g h e r l e v e l IMPORT BinToReal, s h i f t b i n , GetMantissa, GetExponent; IMPORT con; IMPORT mycast; STATIC changequot e ( [ , ] ) i f e l s e ( P R E C , 1, INTEGER i f e l s e ( P R E C , 1, INTEGER ifelse(PREC, [ P r e c i s i o n : INTEGER = 6;], PREC, 2, [ P r e c i s i o n = 32;], [ P r e c i s i o n : INTEGER = 64] ) [MantPrec : INTEGER = 3 ; ] , PREC, 2, [MantPrec : = 23;], [MantPrec : INTEGER = 52] ) 1, [ExpPrec : INTEGER = 2 ; ] , PREC, 2, [ExpPrec : INTEGER = 8 ; ] , [ExpPrec : INTEGER = 1 1 ] ) ResBits : INTEGER = MantPrec; MantBits : INTEGER = MantPrec + 3; Divider: T = STATE step: INTEGER = 1; STATIC (* * f u n c t i o n t o change a b i n a r y * number i n t o a boolean v a r i a b l e *) 72 BinElemToBool: Fl= BEGIN { ONE | (binelem = 1) ? TRUE, (binelem = 0) ? FALSE } END; (* BinElemToBool *) BinNumToBool: F2 = STATIC z: BinArray(n) = BEGIN BinElemToBool(binnum(i)) END; BEGIN z END; (* BinNumToBool *) b i n r e a l d i v i d e n d : BinNumber(Precision) = Makebin(realdividend); b i n r e a l d i v i s o r : BinNumber(Precision) = Makebin(realdivisor); booldividend: BinArray(Precision) = BinNumToBool(binrealdividend, b i n r e a l d i v i d e n d . n ) ; booldivisor: BinArray(Precision) = BinNumToBool(binrealdivisor, b i n r e a l d i v i s o r . n ) ; dividendexp: REAL =(BinToReal(GetExponent(booldividend), 2)); d i v i s o r e x p : REAL = (BinToReal(GetExponent(booldivisor), 2)); BEGIN (* * p r i n t out the arguments i n f i r s t 2 steps *) I| « step= 1 -> step := step+1 » * W r i t e S t r i n g ( BEGIN con.cat2("dividend: ", M a k e S t r i n g ( r e a l d i v i d e n d ) ) END) « step= 2 -> step := step+1 » * W r i t e S t r i n g ( BEGIN con.cat2("divisor: ", M a k e S t r i n g ( r e a l d i v i s o r ) ) END) 73 (* * c a l l the d i v i d e r array *) I| END; END. « (step = 3) » * D i v i d e r A r r a y ( GetMantissa(booldividend), GetMantissa(booldivisor), round(dividendexp - d i v i s o r e x p ) , MantBits, R e s B i t s ) (* D i v i d e r *) (* main module *) (* * d e f i n i t i o n module f o r WLTimedDivider *) DEFINITION MODULE WLTimedDivider ; FROM types IMPORT ResElement, ResNumber; FROM timer IMPORT Time, TimeArray; EXPORT D i v i d e r A r r a y , BinArray; TYPE B i n A r r a y ( n : INTEGER) = ARRAY(i: INDEX(n)): BOOLEAN; PrechargeBar = RECORD t : Time; (* time a t which value was l a s t changed *) v : BOOLEAN (* value *) t (* time at which value was END; Output = RECORD : Time; l a s t changed *) v : BOOLEAN (* value *) END; StageState = RECORD pb: PrechargeBar; q: Output END; StageArray(n:INTEGER) = ARRAY(i:INDEX(n)):StageState; 74 F = CELL(me, next, prev: StageState; r e s u l t : R'esNumber; quotientnumber: INTEGER; remainder, divisor:BinArray; STATIC MantBits: INTEGER; STATIC exp: INTEGER; t a u : Time; NextTime: TimeArray; STATIC number: INTEGER); CI = CELL(STATIC b i n d i v i d e n d , b i n d i v i s o r : B i n A r r a y ; STATIC exp INTEGER; STATIC MantBits, R e s B i t s : INTEGER); STATIC process: F; D i v i d e r A r r a y : CI; END. (* d i v i d e r *) (**********************************************) (* * implementation module f o r WLTimedDivider *) IMPLEMENTATION MODULE WLTimedDivider; FROM s t r i n g l O IMPORT W r i t e S t r i n g ; FROM s t r i n g s IMPORT I n t T o S t r i n g , B o o l T o S t r i n g ; FROM WLTimedHigherlevel IMPORT d i v i d e , i n v e r t e r , b i n p r i n t ; FROM timer IMPORT ChangeTime, StopPrechargeTime, StartEvaluationTime; IMPORT con; STATIC NoOfStage : INTEGER = 3 ; process: F = BEGIN (* * enable e v a l u a t i o n , i f the successor stage * has s t a r t e d t o precharge * ( j u s t added the a d d i t i o n a l c o n s t r a i n t t h a t * the output has t o drop f i r s t ) *) « NOT next.pb.v AND NOT me.pb.v -> me.pb.v, me.pb.t := TRUE, t a u » 75 (* * i f successor stage has f i n i s h e d 0 . * and i s h o l d i n g the output, we can s t a r t * precharging I I *) « next.pb.v AND next.q.v AND me.pb.v -> me.pb.v, NextTime(number).otime, me.pb.t := FALSE, t a u + StopPrechargeTime, t a u » (* * as soon as we s t a r t precharging, we can * drop the output II signal *) « NOT me.pb.v AND me.q.v -> me.q.v, NextTime(number).otime, me.q.t := FALSE, 0.0, tau » (* * i f i n 0 . mode ( i . e . no precharge), * and predecessor has v a l u e , can determine * the next q u o t i e n t * * s e t t i n g count t o zero enables the d i v i d e r * which s e t s me.q.v t o TRUE a f t e r determining * the next q u o t i e n t d i g i t *) II « me.pb.v AND (tau >= me.pb.t + StartEvaluationTime) AND NOT me.q.v * » d i v i d e ( r e m a i n d e r , d i v i s o r , r e s u l t , exp, MantBits, quotientnumber, me.q.v) END; (* process *) STATIC D i v i d e r A r r a y : CI = TYPE LCI = C E L L ( f i r s t , second, t h i r d : StageState; r e s u l t : ResNumber); LF1 = FUNCTION(first, STRING; second, t h i r d : S t a g e S t a t e ) : 76 LF2 = FUNCTION(bindividend, b i n d i v i s o r : BinArray; n: INTEGER): ResElement; LF3 = FUNCTION(bindividend: BinArray; n: INTEGER): ResElement; STATE NextTime: TimeArray(NoOfStage); t a u : Time = 0.0; f i r s t : StageState; second: StageState; t h i r d : StageState; I n i t : BOOLEAN = TRUE; counter: INTEGER = 0; quotientnumber: INTEGER = ResBits-2; r e s u l t : ResNumber(ResBits); (* * work with p o s i t i v e d i v i d e n d and d i v i s o r *) remainder: BinArray(MantBits) = BEGIN {ONE | ( NOT b i n d i v i d e n d ( M a n t B i t s - D ) ? bindividend(i), bindividend(MantBits-l) ? i n v e r t e r ( b i n d i v i d e n d , M a n t B i t s ) ( i ) } END; p o s d i v i s o r : BinArray(MantBits) = BEGIN {ONE I ( NOT b i n d i v i s o r ( M a n t B i t s - 1 ) ) ? b i n d i v i s o r ( i bindivisor(MantBits-1) ? inverter(bindivisor, M a n t B i t s ) ( i ) } END; n e g d i v i s o r : BinArray(MantBits) = BEGIN {ONE | b i n d i v i s o r ( M a n t B i t s - l ) ? b i n d i v i s o r ( i ) , ( NOT b i n d i v i s o r ( M a n t B i t s - l ) ) ? i n v e r t e r ( b i n d i v i s o r , M a n t B i t s ) ( i ) } END; STATIC d e t s i g n : LF2 = (* f u n c t i o n t o determine s i g n of r e s u l t *) BEGIN { ONE| (NOT b i n d i v i d e n d ( n - 1 ) ) AND (NOT bindivisor(n-l))? 0 bindividend(n-1) AND b i n d i v i s o r ( n - 1 ) ? 0, (NOT ( b i n d i v i d e n d ( n - l ) = b i n d i v i s o r ( n - l ) ) ) ? 1 } 77 END; STATIC d e t q u o t i e n t : LF3 = (* f u n c t i o n t o determine q u o t i e n t b i t *) BEGIN { ONE | NOT ( b i n d i v i d e n d ( n - l ) ) ? 1, ( b i n d i v i d e n d ( n - l ) AND bindividend(n-2) ) AND b i n d i v i d e n d ( n - 3 ) ? 0, (bindividend(n-1)) AND ( NOT (bindividend(n-2)) OR NOT ( b i n d i v i d e n d ( n - 3 ) ) ) ? -1 } END; STATIC I n i t i a l i z e : LCI = (* * i n i t i a l i z e s t a t e of stage * and put the s i g n of the * quotient into result.n-1 *) BEGIN « f i r s t . p b . v , f i r s t . q . v , second.pb.v, second.q.v, third.pb.v, third.q.v, result(result.n-1), result(result.n-2), f i r s t . p b . t , second.pb.t, t h i r d . p b . t := TRUE, TRUE, FALSE, FALSE, TRUE, TRUE, detsign(bindividend, b i n d i v i s o r , MantBits), detquotient(remainder, M a n t B i t s ) , 0.0, 0.0, 0.0 » * WriteString(BEGIN " I n i t i a l i z i n g . . . " END) END; STATIC P r i n t e r : LF1 = (* p r i n t s t a t e of the stages *) BEGIN con.cat3( con.cat3( B o o l T o S t r i n g ( f i r s t . p b . v , FALSE), B o o l T o S t r i n g ( f i r s t . q . v , FALSE), " " ) , con.cat3( BoolToString(second.pb.v, FALSE), BoolToString(second.q.v, FALSE), " " ), con.cat3( B o o l T o S t r i n g ( t h i r d . p b . v , FALSE), 78 B o o l T o S t r i n g ( t h i r d . q . v , FALSE), " " ) ) END; STATE s i g n : ResElement = d e t s i g n ( b i n d i v i d e n d , bindivisor, MantBits); BEGIN « II « I n i t -> I n i t := FALSE » * I n i t i a l i z e d i r s t , second, t h i r d , NOT I n i t AND (counter < 2000) -> result) counter := counter + 1 » * ( process( f i r s t . s e c o n d , t h i r d , r e s u l t , quotientnumber, remainder, p o s d i v i s o r , M a n t B i t s , exp, t a u , NextTime, 0) II process( second,third,first, result, quotientnumber, remainder, p o s d i v i s o r , M a n t B i t s , exp, t a u , NextTime, 1) II p r o c e s s ( I| t h i r d , f i r s t , second, r e s u l t , quotientnumber, remainder, p o s d i v i s o r , M a n t B i t s , exp, t a u , NextTime, 2) ChangeTime(tau, t a u , NextTime) ) END; (* D i v i d e r A r r a y *) END. (* d i v i d e r module *) (* * d e f i n i t i o n module f o r WLTimedHigherlevel *) DEFINITION MODULE WLTimedHigherlevel; FROM types IMPORT ResElement, ResNumber, BinNumber, ArrayOfBool; FROM WLTimedDivider IMPORT B i n A r r a y ; EXPORT B i n T o R e a l , d i v i d e , GetExponent, GetMantissa, resprint, shiftbin, printresult, inverter, binprint; 79 TYPE F l = FUMCTIOM(m, n b i t s : INTEGER): BinArray; F2 = FUNCTION(bindividend, b i n d i v i s o r : BinArray; n: INTEGER): BOOLEAN; F4 = FUNCTION(bool: BOOLEAN): INTEGER; F5 = FUNCTION(bindividend, b i n d i v i s o r : BinArray; n: INTEGER): BinArray; F6 = FUNCTION(binnumber: BinArray; n: INTEGER): BOOLEAN; F7 = FUNCTION(binnumber: BinArray; n: INTEGER): BinArray; F8 = FUNCTION(binnumber: BinArray; n: INTEGER): REAL; F9 = FUNCTION(bindividend, b i n d i v i s o r : BinArray; n, m: INTEGER): BinArray; F10 = FUNCTION(result: ResNumber; n, exp: INTEGER): STRING; F l l = FUNCTION(bindividend, b i n d i v i s o r : BinArray; n: INTEGER): ResElement; F12 = FUNCTION(bindivisor: BinArray; n: INTEGER; m: ResElement) BinArray; F13 = FUNCTION(a: INTEGER): REAL; F14 = FUNCTION(bindividend: BinArray; n: INTEGER): ResElement; F15 F16 F17 F18 = = = = FUNCTION(binnumber: B i n A r r a y ) : BinArray; FUNCTION(binnumber: B i n A r r a y ) : BinArray; FUNCTION( num: BinArray; n: INTEGER):STRING; FUNCTI0N( num: ResNumber; n: INTEGER):STRING; F19 = FUNCTION(summand: BinArray; n: INTEGER):BinArray; CI = CELL(remainder, divisor:BinArray ; result: ResNumber; STATIC exp: INTEGER; STATIC n: INTEGER; quotientnumber: INTEGER; done: BOOLEAN ); STATIC change2bin: F l ; b i t a d d : F2; c a r r y : F2; BoolToInt: F4; b i t a d d e r : F5; adder: F9; detsign: F l l ; 80 getsummand: F12; d e t q u o t i e n t : F14; BinToReal: F8; d i v i d e : CI; c a r r i e r : F5; i n v e r t : F6; i n v e r t e r : F7; s h i f t b i n : F7; p r i n t r e s u . l t : F10; power2: F13; IntToReal: F13; b i n p r i n t : F17; r e s p r i n t : F18; g e t s h o r t : F19; GetMantissa: F15; GetExponent: F16; END. (* h i g h e r l e v e l *) (* * implementation module f o r WLTimedHigherlevel *) IMPLEMENTATION MODULE WLTimedHigherlevel; FROM s t r i n g l O IMPORT W r i t e S t r i n g ; FROM s t r i n g s IMPORT I n t T o S t r i n g , BoolToString; FROM cast IMPORT r e a l , round; FROM mycast IMPORT Makebin, MakeString; IMPORT con; IMPORT mycast; STATIC changequot e ( [ , ] ) i f e l s e ( P R E C , 1, [ P r e c i s i o n : INTEGER = 6;], PREC, 2, INTEGER = 32;], [ P r e c i s i o n [Precision : INTEGER = 64] ) i f e l s e ( P R E C , 1, [MantPrec : INTEGER = 3 ; ] , PREC, 2, [MantPrec : INTEGER = 23;], [MantPrec : INTEGER = 52] ) i f e l s e ( P R E C , 1, [ExpPrec : INTEGER = 2 ; ] , PREC, 2, [ExpPrec : 81 INTEGER =8;], [ExpPrec : INTEGER =11]) ResBits : INTEGER = MantPrec; MantBits : INTEGER = MantPrec + 3; (* * function to compute the powers of 2 *) power2: F13 = BEGIN ONE 1 a = -1 ? 0.5, a = -2 ? 0.25, a = -3 ? 0.125, a = -4 ? 0.0625, a = -5 ? 0.03125, a < -5 ? 0.03125* a = 0 ? 1, a = 1 ? 2, a = 2 ? 4, a = 3 ? 8, a = 4 ? 16, a = 5 ? 32, a = 6 ? 64, a = 7 ? 128, a = 8 ? 256, a = 9 ? 512, a > 9 ? 1024.0 *p } END; resprint: F18 = (* function f o r printing *) BEGIN con.cat2( { ONE | n = 0 ? IntToString(num(n), 3), n > 0 ? con.cat2(IntToString(num(n), 3), resprint(num, n-1)) }, END; (* resprint *) 82 STATIC b i n p r i n t : F17 = (* f u n c t i o n f o r p r i n t i n g BEGIN con.cat2( •C ONE | *) n = 0 ? BoolToString(num(n) , FALSE), n > 0 ? con.cat2(BoolToString(num(n), FALSE), binprint(num, n-1)) >, M END; II ^ (* b i n p r i n t *) (* * f u n c t i o n t o change a b i n a r y * number i n t o a decimal number *) BinToReal: F8 = TYPE ArrayIndex = INTEGER SUBRANGE 0 .. binnumber.n-2; BEGIN • {+ i : ArrayIndex I r e a l ( BoolToInt(binnumber(i))) * (power2(i-(n-2))) } * { ONE I ( NOT binnumber(binnumber.n-1))? 1.0, binnumber(binnumber.n-1) ? -1.0 } END; (* * f u n c t i o n t o change a number i n t o a b i n a r y number * ( f i r s t b i t i s sign b i t ) *) change2bin: F l = STATIC z: B i n A r r a y ( n b i t s ) = BEGIN FALSE BEGIN z END; (* * function to (* change2binary *) a b i n a r y number * t o the l e f t *) shiftbin: F7= 83 END; STATIC z: BinArray(n) = BEGIN { ONE | i = n-1 ? binnumber(n-l), i = 0 ? 0, ((i>0) AND ( i < n - l ) ) ? binnumber(i-l) } END; BEGIN z END; (* * f u n c t i o n t o change a boolean * i n t o a b i n a r y number *) BoolToInt: F4= BEGIN { ONE I bool = TRUE ? 1, bool = FALSE ? 0 } END; (* BoolToInt *) (* * f u n c t i o n t h a t adds two b i t s *) b i t a d d : F2 = BEGIN (bindividend(n) END; (* add *) XOR b i n d i v i s o r ( n ) ) (* * f u n c t i o n t h a t adds the b i t s * of a b i n a r y number *) b i t a d d e r : F5 = STATIC z: BinArray(n) = BEGIN b i t a d d ( b i n d i v i d e n d , b i n d i v i s o r , END; BEGIN z END; (* b i t a d d e r *) 84 (* * f u n c t i o n t o add two b i n a r y numbers *) adder: F9 = STATIC z: BinArray(n) = { ONE | m>0 ? adder( b i t a d d e r ( b i n d i v i d e n d , b i n d i v i s o r , i carrier(bindividend, bindivisor, n, m-1), m = 0 ? b i t a d d e r ( b i n d i v i d e n d , b i n d i v i s o r , n) }; BEGIN z END; (* adder *) (* * f u n c t i o n that determines the c a r r y b i t of two b i t s *) c a r r y : F2 = BEGIN { ONE I n = 0 ? FALSE, n > 0 ? ( b i n d i v i d e n d ( n - l ) AND b i n d i v i s o r ( n - l ) ) } END; (* c a r r y *) (* * f u n c t i o n that determines the c a r r y * b i t s of two b i n a r y numbers *) c a r r i e r : F5 = STATIC z: BinArray(n) = BEGIN carry(bindividend, bindivisor, i ) END; BEGIN z END; (* c a r r i e r *) (* * function to invert b i t s *) i n v e r t : F6 = 85 BEGIN ( NOT binnumber(n) ) END; (* i n v e r t *) (* * f u n c t i o n t o i n v e r t a b i n a r y number * (hope t h i s works f o r a l l cases! ) *) i n v e r t e r : F7 = STATIC z: BinArray(n) = x: BinArray(n) = { 0NE| i = i > BEGIN adder(z, x, n, n) END; (* i n v e r t e r *) BEGIN i n v e r t (birinumber, i ) END; BEGIN 0? TRUE, 0? FALSE } END; (* * c e l l t h a t does the d i v i s i o n * i t f i r s t checks i f the mantissa of the * d i v i d e n d and d i v i s o r are the same *) d i v i d e : CI = STATIC getsummand: F12 = (* f u n c t i o n t o determine the summand *) STATIC z: BinArray(n) = { ONE | m = 0 ? change2bin(0,n), m = -1 ? b i n d i v i s o r , m = 1 ? i n v e r t e r ( b i n d i v i s o r , n) >; BEGIN z END; d e t q u o t i e n t : F14 = (* f u n c t i o n t o determine quotient b i t *) BEGIN { ONE | NOT ( b i n d i v i d e n d ( n - l ) ) ? 1, ( ( b i n d i v i d e n d ( n - l ) ) AND ( b i n d i v i d e n d ( n - 2 ) ) ) AND ( b i n d i v i d e n d ( n - 3 ) ) ? 0, 86 ( b i n d i v i d e n d ( n - l ) ) AND ( NOT (bindividend(n-2)) OR NOT ( b i n d i v i d e n d ( n - 3 ) ) ) ? -1 } END; d e t s i g n : F l l = (* f m i c t i o n t o determine s i g n of r e s u l t BEGIN { ONE| (NOT b i n d i v i d e n d ( n - l ) ) AND (NOT b i n d i v i s o r ( n - 1 ) ) ? 0, bindividend(n-1) AND b i n d i v i s o r ( n - 1 ) ? 0, (NOT ( b i n d i v i d e n d ( n - l ) = b i n d i v i s o r ( n - l ) ) ) ? 1 } END; g e t s h o r t : F19 = STATIC z: BinArray(3) = BEGIN summand(n-(4-i)) END; BEGIN z END; STATE count : INTEGER = 0; BEGIN (* * note t h a t the quotient i s determined u s i n g approx * r a t h e r than remainder; t h i s i s t o simulate the * quotient s e l e c t i o n of the t r a n s i s t o r l e v e l d i v i d e r *) « ^ NOT done AND ((quotientnumber >= 1) AND (quotientnumber <= ResBits-1)) -> result(quotientnumber-1), remainder , quotientnumber, done := detquotient(adder(getshort(remainder, n) , getshort(getsummand(divisor, n, r e s u l t ( q u o t i e n t n u m b e r ) ) , n ) , 3, 3 ) , 3 ) , s h i f t b i n ( adder(remainder, 87 getsummand(divisor, n, r e s u l t ( q u o t i e n t n u m b e r ) ) , n, n ) , n ) , quotientnumber-1, TRUE » « NOT done AND (count = 0) AND (quotientnumber = 0) -> quotientnumber := -1 » * W r i t e S t r i n g ( BEGIN p r i n t r e s u l t ( r e s u l t , R e s B i t s , exp) END) I| END; p r i n t r e s u l t : F10 = STATIC p o s b i t s : BinArray(n) = BEGIN { 0NE| r e s u l t ( i ) = 0 ? FALSE, r e s u l t ( i ) = 1 ? TRUE, r e s u l t ( i ) = -1 ? FALSE } END; n e g b i t s : BinArray(n) { ONE I r e s u l t ( i ) result(i) result(i) = BEGIN = 0 ? FALSE, = 1 ? FALSE, = -1 ? TRUE } END; getsummand: F5 = STATIC z: BinArray(n) = { ONE | b i n d i v i d e n d ( n - l ) ? i n v e r t e r ( b i n d i v i s o r , n ) , ( NOT b i n d i v i d e n d ( n - l ) ) ? i n v e r t e r ( b i n d i v i s o r , n) >; BEGIN z END; BEGIN c o n . c a t 3 ( " r e s u l t : ", MakeString(BinToReal(adder(posbits, getsummand(posbits, negbits.result.n), result.n, result.n), result.n) * power2(exp)), "\n") END; (* * f u n c t i o n t o get the mantissa of the r e a l number * ( i n s i n g l e format); note t h a t the i m p l i c i t "1" * at the most s i g n i f i c a n t b i t i s e x p l i c i t here; * i n case i t i s a neg number, have t o use the i n v e r t e d * number 88 *) GetMantissa: F15 = TYPE LF1 = FUNCTION(binnumber: BinArray; i : INTEGER): INTEGER; STATIC b i n i n v e r t : BinArray(MantPrec+2) = BEGIN inverter(binnumber, MantPrec+2)(i) END; (* * need t o check i f the whole mantissa * (without the u n i t y and i m p l i c i t * b i t ) i s z e r o , because i n that case i n v e r t i n g the * number g i v e s an * overflow; i f i t i s z e r o , the i m p l i c i t b i t has t o be * set t o 1 * e.g. i n the case of 4 or 8 *) c h e c k i f z e r o : LF1 = BEGIN { ONE| i > 0 ? { ONE| binnumber(i) ( NOT ? 1, binnumber(i) checkifzero(binnumber, i )? i-1) }, = 0? { ONE I binnumber(0) ? 1, ( NOT binnumber(0)) ? 0 } }END; z: BinArray(MantBits) = BEGIN { ONE | i = (MantBits-3) ? { ONE I checkifzero(binnumber, MantPrec-1)=0 ? TRUE , checkifzero(binnumber, MantPrec-1) = 1 ? (NOT b i n n u m b e r ( P r e c i s i o n - l ) ) }, i = (MantBits-2) ? { 0NE| i (* " i m p l i c i t " b i t *) (* u n i t y b i t *) ( NOT b i n n u m b e r ( P r e c i s i o n - l ) )? FALSE, b i n n u m b e r ( P r e c i s i o n - l ) ? TRUE }, = (MantBits-1) ? b i n n u m b e r ( P r e c i s i o n - l ) , (* s i g n b i t *) ( i < MantBits-3) NOT ? { ONE| binnumber(Precision-l) ? binnumber(i), 89 binnumber(Precision-l) ? bininvert(i) } } END; BEGIN z END; (* * f u n c t i o n t o get the exponent of the r e a l number * b i t number ExpPrec+1 s i g n i f i e s t h e * s i g n of the exponent *) GetExponent: F16 = STATIC z: BinArray(ExpPrec + 1) = BEGIN { ONE I i < (ExpPrec)? { ONE I binnumber(i + MantPrec) ? TRUE, (NOT binnumber(i + MantPrec)) ? FALSE }, i = (ExpPrec)? FALSE }END; BEGIN z END; END. (* h i g h e r l e v e l module *) (***************************************) (* * d e f i n i t i o n module f o r the main f u n c t i o n * of the t r a n s i s t o r l e v e l program *) DEFINITION MODULE main; FROM types IMPORT BinNumber, BinElement, ResElement, ResNumber, DRArray, ArrayOfDRA; EXPORT D i v i d e r ; TYPE T = CELL(STATIC r e a l d i v i d e n d , r e a l d i v i s o r : REAL); STATIC 90 D i v i d e r : T; END. (* main *) (* * implementation module f o r t h e main f u n c t i o n * of t h e t r a n s i s t o r l e v e l program *) IMPLEMENTATION MODULE main; FROM s t r i n g l O IMPORT W r i t e S t r i n g ; FROM s t r i n g s IMPORT I n t T o S t r i n g , B o o l T o S t r i n g ; FROM cast IMPORT round; FROM mycast IMPORT Makebin, MakeString; FROM t r a n s i s t o r l e v e l IMPORT PrintDRArray, T r a n s i s t o r L e v e l D i v i d e r ; FROM h i g h e r l e v e l IMPORT getmantissa, BinToReal, d i v i d e , BinToDR, getexponent, shiftbin, inverter; IMPORT con; IMPORT mycast; STATIC changequot e ( [ , ] ) i f e l s e ( P R E C , 1, [ P r e c i s i o n : INTEGER = 6;], PREC, 2, [ P r e c i s i o n : INTEGER = 32;], [ P r e c i s i o n : INTEGER = 64] ) i f e l s e ( P R E C , 1, [MantPrec : INTEGER = 3 ; ] , PREC, 2, [MantPrec : INTEGER = 23;], [MantPrec : INTEGER = 52] ) i f e l s e ( P R E C , 1, [ExpPrec : INTEGER = 2 ; ] , PREC, 2, [ExpPrec : INTEGER = 8 ; ] , [ExpPrec : INTEGER = 1 1 ] ) ResBits : INTEGER = MantPrec; MantBits : INTEGER = MantPrec + 3; Divider: T = TYPE LF1 = FUNCTION(bindividend, b i n d i v i s o r : BinNumber; n: INTEGER): BOOLEAN; qindex = INTEGER SUBRANGE 0 .. MantBits-1; 91 STATIC b i n r e a l d i v i d e n d : BinNumber(Precision) = Makebin(realdividend); b i n r e a l d i v i s o r : BinNumber(Precision) = Makebin(realdivisor); dividendexp: REAL= (BinToReal(getexponent(binrealdividend), 2) ) ; d i v i s o r e x p : REAL = (BinToReal(getexponent(binrealdivisor), 2 ) ) ; STATE q u o t i e n t r e g : ArrayOfDRA(MantBits, 3 ) ; r e s u l t : ResNumber(ResBits); step: INTEGER = 1 ; d i v i d e r d o n e : BOOLEAN = FALSE; D R d i v i s o r : DRArray(MantBits); DRdividend: Array0fDRA(3,MantBits); b i n d i v i s o r : BinNumber(MantBits) = getmantissa(binrealdivisor); b i n d i v i d e n d : BinNumber(MantBits) = getmantissa(binrealdividend); s i g n : DRArray(3); q u o t i e n t : INTEGER = 0; STATIC p o s d i v i d e n d : BinNumber(MantBits) = BEGIN {ONE | b i n d i v i d e n d ( M a n t B i t s - l ) = 0? b i n d i v i d e n d ( i ) , b i n d i v i d e n d ( M a n t B i t s - l ) = 1? inverter(bindividend, MantBits)(i) }END; p o s d i v i s o r : BinNumber(MantBits) = BEGIN {ONE | b i n d i v i s o r ( M a n t B i t s - l ) = 0? b i n d i v i s o r ( i ) , b i n d i v i s o r ( M a n t B i t s - l ) = 1? inverter(bindivisor, MantBits)(i) } END; d e t s i g n : LF1 = (* f u n c t i o n t o determine s i g n of r e s u l t *) BEGIN { 0NE| (bindividend(n-l)=0) AND (bindivisor(n-l)=0)? FALSE, ( b i n d i v i d e n d ( n - l ) = l ) AND ( b i n d i v i s o r ( n - l ) = l ) ? 92 (NOT FALSE, ( b i n d i v i d e n d ( n - l ) = b i n d i v i s o r ( n - l ) ) ) ? TRUE } END; BEGIN « step= 1 -> step := step+1 » * W r i t e S t r i n g ( BEGIN con.cat2("dividend: ", MakeString(realdividend)) END) II « step= 2 -> step := step+1 » I| I| I| * W r i t e S t r i n g ( BEGIN c o n . c a t 2 ( " d i v i s o r : ", M a k e S t r i n g ( r e a l d i v i s o r ) ) END) « step = 3 -> step := step + 1 » * B i n T o D R ( s h i f t b i n ( p o s d i v i s o r , MantBits), DRdivisor) * BinToDR(posdividend, DRdividend(l)) « step = 4 -> step := step + 1 » * W r i t e S t r i n g ( BEGIN c o n . c a t 2 ( " D i v i s o r : ", PrintDRArray(DRdivisor)) END) * W r i t e S t r i n g ( BEGIN con.cat2("Dividend: ", PrintDRArray(DRdividend(l))) END) « step = 5 » * T r a n s i s t o r L e v e l D i v i d e r ( D R d i v i s o r , DRdividend, q u o t i e n t r e g , round(dividendexp - d i v i s o r e x p ) ) END; END. (* D i v i d e r *) (* main module *) ^^^^^^^^^^^^^^^ic^^^^^^^:^:^:^^*************) (* * d e f i n i t i o n module f o r t r a n s i s t o r l e v e l * of the timed word l e v e l program *) DEFINITION MODULE t r a n s i s t o r l e v e l ; FROM types IMPORT BinNumber, BinElement, ResElement, ResNumber, D u a l R a i l , DRArray, ArrayOfDRA, ArrayOfBool, BoolArray; FROM timer IMPORT Time, TimeRecord, ArrayOfPrechargeBar, PrechargeBar; EXPORT T r a n s i s t o r L e v e l D i v i d e r , PrintDRArray, DRtoRes ; 93 TYPE DR2B C101 C102 C103 = = = = FUNCTION(x: D u a l R a i l ) : BOOLEAN; CELL(pb: BOOLEAN; a, b, c a r r y i n , sum : D u a l R a i l ) ; CELL(pb: BOOLEAN; a, b, c a r r y i n , carryout : D u a l R a i l ) ; CELL(a, b, c, d : DRArray); C104 = CELL(pb: BOOLEAN; a, b, c a r r y i n , c a r r y o u t , sum : DualRail); C105 = CELL(pb: BOOLEAN; c a r r y , remainder, d i v i s o r , c a r r y o u t , sum : DRArray; c a r r y b i t : D u a l R a i l ; TimeTable: TimeRecord;STATIC me: INTEGER); C106 = CELL(pb: BOOLEAN; quotient:ArrayOfBool; d i v i s o r , output: DRArray; c a r r y b i t : D u a l R a i l ; TimeTable: TimeRecord; STATIC me: INTEGER); C107 = CELL(pb: PrechargeBar; sum: DRArray; q u o t i e n t : ArrayOfBool; qsldone: D u a l R a i l ; TimeTable: TimeRecord; t a u : Time; STATIC me: INTEGER); C108 = CELL(pb: BOOLEAN; a, b, sum : DRArray; TimeTable: TimeRecord; STATIC me: INTEGER); C109 = CELL(drarray: DRArray); C1010 = CELL(a, nega: DRArray); C1011 = CELL(pb: BOOLEAN; input: DRArray; done: D u a l R a i l ) ; C1012 = CELL(pb: PrechargeBar;STATIC number: INTEGER; qsldone: DualRail; done, donenext: DRArray; t a u : Time); P r o c e s s C e l l = CELL(pb: ArrayOfPrechargeBar;STATIC number: INTEGER; d i v i s o r : DRArray; c a r r y , sum: ArrayOfDRA; q u o t i e n t : BoolArray; done: ArrayOfDRA; quotientnumber: INTEGER; t a u : Time; TimeTable: TimeRecord); S t a g e C e l l = CELL(pb: ArrayOfPrechargeBar;STATIC number: INTEGER; d i v i s o r : DRArray; c a r r y , sum: ArrayOfDRA; q u o t i e n t : BoolArray; done: ArrayOfDRA; TimeTable: TimeRecord; t a u : Time); C1013 = CELL(quotient: DRArray; q u o t i e n t r e g : ArrayOfDRA; quotientnumber: INTEGER); C1014 = CELL(resnumber: ResNumber; dualrailnumber:ArrayOfDRA); C1015 = CELL(dualrailnum, shiftednum: DRArray); C1016 = CELL(pb: BOOLEAN; input: ArrayOfBool; done: D u a l R a i l ; TimeTable: TimeRecord;STATIC me: INTEGER); F101 = FUNCTION( a, b, c a r r y i n , c a r r y o u t , sum : DRArray) 94 : STRING; F102 = FUNCTION( a, b, c a r r y i n , carryout, sum : DRArray; i INTEGER): STRING; F103 = FUNCTI0N( a, b, c a r r y i n , c a r r y o u t , sum : D u a l R a i l ) : STRING; F104= FUNCTION(a: D u a l R a i l ) : STRING; F105= FUNCTION(array: DRArray): STRING; F106= FUNCTION(a: INTEGER): INTEGER; F107= FUNCTIONS: D u a l R a i l ) : BOOLEAN; T10 = C E L L ( d i v i s o r : DRArray; sum, q u o t i e n t r e g : ArrayOfDRA; STATIC exp: INTEGER ); STATIC AdderPos : AdderNeg : CarryPos : CarryNeg : Initialize AdderStage: CarrySave: MUX: C106; QSL: C107; C101; C101; C102; C102; : C103; C104; C105; CarryPropagat e: C108; InitEmpty: C109; I n i t F a l s e : C109; MakeNeg: C1010; StageProcess: S t a g e C e l l ; Process: P r o c e s s C e l l ; Done: C1012; AdderDone: C1011; QSLDone: C1016; DRPrinter: F103; PrintDR: F104; PrintDRArray: F105; F u l l : F107; T r a n s i s t o r L e v e l D i v i d e r : T10; DRtoRes: C1014; 95 ShiftDR: C1015; END. (* t r a n s i s t o r l e v e l *) (* * implementation module f o r the t r a n s i s t o r l e v e l *) IMPLEMENTATION MODULE t r a n s i s t o r l e v e l ; FROM s t r i n g l O IMPORT W r i t e S t r i n g ; FROM s t r i n g s IMPORT I n t T o S t r i n g , BoolToString; FROM h i g h e r l e v e l IMPORT r e s p r i n t , p r i n t r e s u l t ; FROM mycast IMPORT Rand, R e a l P r i n t ; FROM timer IMPORT ChangeTime, PrintTime, GetNextTime, ChangeTTPrecharge, ChangeTTEvaluate, AdderPMaxTime, MUXPMaxTime, QSLPMaxTime, AdderEMinTime, AdderEMaxTime, MUXMaxTime, QSLMaxTime, QSLMinTime, StopPrechargeTime, S t a r t E v a l u a t i o n T i m e ; FROM S T V e r i f i c a t i o n IMPORT Proto, TimingLowerBound; IMPORT con; FROM constants IMPORT P r e c i s i o n , MantPrec, ExpPrec, R e s B i t s , MantBits; STATE STATIC (* * function *) to a DRArray number by 1 b i t t o the l e f t ShiftDR: C1015 = TYPE Index = INTEGER SUBRANGE 1 .. dualrailnum.n-1; BEGIN {* i : Index I « shiftednum(i).f, shiftednum(i).t := dualrailnum(i-l).f, dualrailnum(i-l).t } * « shiftednum(O).f, shiftednum(O).t := TRUE, FALSE END; O * function » t o copy a DRArray number 96 » *) CopyDR: C1015 = TYPE Index = INTEGER SUBRANGE 0 .. dualrailnum.n-1; BEGIN {* i : Index I « s h i f t e d n u m ( i ) . f , s h i f t e d n u m ( i ) . t := dualrailnum(i).f, dualrailnum(i).t » } END; (* * f u n c t i o n to change DRArray (quotientreg.) i n t o ResNumber *) DRtoRes: C1014 = TYPE LF1= FUNCTION(dualrailnumber: DRArray): ResElement; STATIC DRtoResElem: LF1 = BEGIN { 0NE| dualrailnumber(2).t ? 1, dualrailnumber(1).t ? 0, dualrailnumber(0).t ? -1} END; BEGIN {* i : INDEX(resnumber.n-1) | « resnumber(i) := DRtoResElem(dualrailnumber(resnumber.n-l-i)) > END; Empty: F107 BEGIN (NOT = x.t AND NOT x.f) END; F u l l : F107 BEGIN (x.t OR = x.f) END; InitEmpty: C109 = 97 » BEGIN {* i : INDEX(drarray.n) I « d r a r r a y ( i ) . f , d r a r r a y ( i ) . t := FALSE, FALSE » } END; I n i t F a l s e : C109 = BEGIN {* i : INDEX(drarray.n) I « d r a r r a y ( i ) . f , d r a r r a y ( i ) . t := TRUE, FALSE » } END; I n i t T r u e : C109 = BEGIN {* i : INDEX(drarray.n) I « d r a r r a y ( i ) . t , d r a r r a y ( i ) . f TRUE, FALSE » } := END; (* * i f an odd number of inputs i s h i g h , the sum * output i s a l s o h i g h *) AdderPos: C101 = BEGIN « sum.t AND NOT pb -> sum.t := I | « NOT sum.t AND pb AND a.t AND := TRUE » II « NOT sum.t AND pb AND a.f AND (b.t AND c a r r y i n . f ) ) -> sum.t := TRUE II « NOT sum.t AND pb AND a.t AND := TRUE » FALSE » b . t AND c a r r y i n . t -> sum.t ( ( b . f AND c a r r y i n . t ) OR » b . f AND c a r r y i n . f -> sum.t END; (* * i f zero o r an even number of inputs i s h i g h , * the sum output i s low *) AdderNeg: C101 = BEGIN « sum.f AND NOT pb -> sum.f := FALSE » I | « NOT sum.f AND pb AND a.f AND b . f AND c a r r y i n . f -> sum.f 98 II « I| « := TRUE » NOT sum.f AND pb AND a.t AND ( ( b . t AND c a r r y i n . f ) OR (b.f AND c a r r y i n . t ) ) -> sum.f := TRUE » NOT sum.f AND pb AND a.f AND b . t AND c a r r y i n . t -> sum.f := TRUE » END; (* * i f at l e a s t two inputs are high, * the c a r r y output i s a l s o h i g h *) CarryPos: C102 = BEGIN « c a r r y o u t . t AND NOT pb -> c a r r y o u t . t := FALSE » II « NOT c a r r y o u t . t AND pb AND a.t AND b . t AND ( c a r r y i n . f OR c a r r y i n . t ) -> c a r r y o u t . t := TRUE » I | « NOT c a r r y o u t . t AND pb AND a.t AND b . f AND c a r r y i n . t -> c a r r y o u t . t := TRUE » I ! « NOT c a r r y o u t . t AND pb AND a.f AND b . t AND c a r r y i n . t -> c a r r y o u t . t := TRUE » END; (* * i f l e s s than two inputs are high, * the c a r r y output i s low *) CarryNeg: C102 = BEGIN « c a r r y o u t . f AND II « NOT c a r r y o u t . f carryin.f) I | « NOT c a r r y o u t . f carryout.f I | « NOT c a r r y o u t . f carryout.f END; AdderStage: C104 = BEGIN I| NOT pb -> c a r r y o u t . f := FALSE » AND pb AND a.f AND b . f AND ( c a r r y i n . t OR -> c a r r y o u t . f := TRUE » AND pb AND a.f AND b . t AND c a r r y i n . f -> := TRUE » AND pb AND a.t AND b . f AND c a r r y i n . f -> := TRUE » AdderPos(pb, a, b, c a r r y i n , sum) AdderNeg(pb, a, b, c a r r y i n , sum) 99 I I CarryPos(pb, a, b, c a r r y i n , c a r r y o u t ) I| CarryNegCpb, a, b, c a r r y i n , c a r r y o u t ) END; (* * c a r r y propagate adder *) CarryPropagate: C108 = STATE carryout: DRArray(3); c a r r y : DRArray(1); i n i t : BOOLEAN = TRUE; STATIC n: INTEGER = a.n-1; BEGIN « i n i t -> i n i t := FALSE » * I n i t F a l s e ( c a r r y ) * InitEmpty(carryout) * WriteString(BEGIN " I n i t i a l i z i n g i n CarryPropagate" I I « NOT i n i t » * ( AdderStage(pb, a(n-4), b(n-3), c a r r y ( O ) , c a r r y o u t ( 0 ) , sum(0)) II AdderStage(pb, a(n-3), b(n-2), c a r r y o u t ( O ) , c a r r y o u t ( l ) , sum(l)) II AdderStage(pb, a(n-2), b ( n - l ) , c a r r y o u t ( l ) , c a r r y o u t ( 2 ) , sum(2)) END) ) END; CarrySave: C105 = TYPE Stagelndex = INTEGER SUBRANGE 2 .. remainder.n-1; STATE temp: D u a l R a i l ; i n i t : BOOLEAN = TRUE; BEGIN « I| i n i t -> i n i t , temp.f, temp.t « NOT i n i t » * ( { := FALSE, TRUE, FALSE I I i : Stagelndex I AdderStage(pb, c a r r y ( i - 2 ) , r e m a i n d e r ( i - 1 ) , 100 » d i v i s o r ( i ) , c a r r y o u t ( i ) , sum(i)) } II AdderStage(pb, c a r r y b i t , temp, d i v i s o r ( O ) , c a r r y o u t ( 0 ) , sum(0)) AdderStage(pb, temp, remainder(0), d i v i s o r ( i ) , II c a r r y o u t ( l ) , sum(l)) ) END; (* * * * * * * multiplexer; s e l e c t s - depending on the quotient - e i t h e r the d i v i s o r or the complement of the d i v i s o r ( i n that case "1" s t i l l has t o be added t o t h e MUX output, when i n s e r t e d i n t o the adder i f the quotient i s 0, the output of the MUX * i s FALSE *) MUX: C106 = TYPE LCI = CELL(pb: BOOLEAN; d i v i s o r , output: D u a l R a i l ; sn, s z , sp: BOOLEAN); . Stagelndex = INTEGER SUBRANGE 0 .. d i v i s o r . n - 1 ; STATE I n i t : BOOLEAN = TRUE; STATIC posmux: LCI = BEGIN « NOT pb AND output.t -> output.t :=FALSE » II « NOT output.t AND pb AND ((sp AND d i v i s o r . t ) OR II II « « (sn AND d i v i s o r . f ) ) -> output.t := TRUE » NOT pb AND c a r r y b i t . t -> c a r r y b i t . t := FALSE » NOT c a r r y b i t . t AND pb AND sn -> c a r r y b i t . t := TRUE » END; negmux: LCI = BEGIN II « « NOT pb AND output.f -> output.f := FALSE » NOT output.f AND pb AND ( ( s p AND d i v i s o r . f ) OR 101 II I| « « (sn AND d i v i s o r . t ) OR ( s z ) ) -> output.f := TRUE » NOT pb AND c a r r y b i t . t -> c a r r y b i t . f := FALSE NOT c a r r y b i t . f AND pb AND NOT sn -> carrybit.f := TRUE » » END; BEGIN { I I i : Stagelndex I posmuxCpb, d i v i s o r ( i ) , o u t p u t ( i ) , q u o t i e n t ( 2 ) , q u o t i e n t ( l ) , quotient(O)) II negmux(pb, d i v i s o r ( i ) , o u t p u t ( i ) , q u o t i e n t ( 2 ) , q u o t i e n t ( l ) , quotient(O)) } END; (* * remove the qsldone input l a t e r ; added * i t t o make the s i m u l a t i o n run f a s t e r *) QSL: C107 = (* gets as input 3 sum b i t s and outputs * 3 DR numbers, one of which i s T, the * others are F * q u o t i e n t ( 2 ) -> -1 * q u o t i e n t ( 1 ) -> 0 * quotient(0) -> +1 *) BEGIN « « « « II II II II II « « NOT pb.v NOT pb.v NOT pb.v pb.v AND -> quotient(2) := FALSE » -> q u o t i e n t ( l ) := FALSE » -> q u o t i e n t ( 0 ) := FALSE » sum(2).f AND (NOT q u o t i e n t ( 2 ) ) -> quotient(2) := TRUE » pb.v AND sum(2).t AND sum(l).t AND sum(0).t AND (NOT q u o t i e n t ( 1 ) ) -> quotient(1) := TRUE pb.v AND sum(2).t AND (sum(l).f OR sum(O).f) AND (NOT quotient(O)) -> quotient(O) := TRUE END; (* * f u n c t i o n f o r c o n v e r t i n g DRArray t o S t r i n g 102 » » *) PrintDRArray: F105 = TYPE LF1= FUNCTION(a: D u a l R a i l ) : STRING; LF2= FUNCTION(array: DRArray; i : INTEGER): STRING; STATIC printDR: LF1 = (* f u n c t i o n f o r c o n v e r t i n g DR t o S t r i n g *) BEGIN { ONE | (NOT a.t) AND (NOT a.f) ? " _ , (* empty *) (NOT a.t) AND a.f ? "0",(* " f a l s e " *) a.t AND (NOT a.f) ? "1",(* " t r u e " *) a.t AND a.f • ? "#" (* f o r b i d d e n *) n > END; printDRArray: BEGIN LF2 = con.cat2( printDR(array(i)), { 0NE| i = 0? "", i > 0? con.cat2(printDRArray(array, i - 1 ) , " ") } ) END; BEGIN printDRArray(array, array.n-1) END; (* * f u n c t i o n t o check i f the adder i s done * (do I need dual r a i l f o r t h i s ? ? ) *) AdderDone: C1011 = BEGIN « pb AND (NOT done.t) » * {* i : INDEX(input.n) | « F u l l ( i n p u t ( i ) ) » } * « done.t := TRUE » I | « NOT pb AND done.t » * •C* i : INDEX(input.n) I « E m p t y ( i n p u t ( i ) ) » « done.t := FALSE » 103 } * END; (* * function to check i f the QSL i s done *) QSLDone: C1016 = BEGIN « pb AND ((input(O) OR input(l)) OR input(2)) AND NOT done.t -> done.t := TRUE » I I « NOT pb AND NOT ((input(O) OR input(1)) OR input(2)) AND done.t -> done.t := FALSE » END; (* * function to check i f the q s l i s done *) Done: C1012 = BEGIN « pb.v AND NOT done(O).t AND qsldone.t -> done(0).t := TRUE » II « NOT pb.v AND done(O).t -> done(O).t := FALSE » END; (* * function to put the quotient b i t s into * a register *) PutlnRegister: C1013 = BEGIN {* i : INDEX(quotient.n) I « quotientreg(quotientnumber)(i).t, quotientreg(quotientnumber)(i).f := quotient(i).t, quotient(i).f » } END; TransistorLevelDivider: T10 = STATE carry: ArrayOfDRA(3,MantBits); 104 quotient: BoolArrayO,3) ; done: ArrayOfDRA(3,1); pb: ArrayOfPrechargeBar(3); Init: BOOLEAN = TRUE; counter: INTEGER = 0; quotientnumber: INTEGER = 1; carrybit: DualRail; result: ResNumber(ResBits+3); tau : Time = 0.0; TimeTable: TimeRecord(3,10); TYPE Qlndex = INTEGER SUBRANGE 1 .. MantBits-1; BEGIN O * to start the run, I set the f i r s t 2 stages pb to TRUE, and * the done signal of stage no. 1 to T; this way, stage 1 w i l l * be "holding" i t s output, and stage 0 can start precharging; * stage 2 can then start evaluating *) « Init -> I n i t , pb(0).v, pb(l).v, pb(2).v, pb(0).tau, pb(l).tau, pb(2).tau, done(l)(0).t, done(l)(0).f, quotient(1)(0), quotient(l)(1), quotient(l)(2) := FALSE, TRUE, TRUE, FALSE, 0.0, 0.0, 0.0, TRUE, FALSE, FALSE, FALSE, TRUE » * « carrybit.t, carrybit.f := FALSE, FALSE » * InitEmpty(sum(0)) * InitEmpty(sum(2)) * InitEmpty(carry(0)) * InitFalse(carry(l)) * InitEmpty(carry(2)) * {* i : Qlndex I InitFalse(quotientreg(i))} * « quotient(0)(0), quotient(0)(1), quotient(0)(2), quotient(2)(0), quotient(2)(1), quotient(2)(2) := FALSE, TRUE, FALSE, FALSE, FALSE, FALSE » * InitEmpty(done(0)) * InitEmpty(done(2)) * WriteString(BEGIN " I n i t i a l i z i n g " END) 105 II « NOT I n i t AND (quotientnumber < MantBits) » *( II II ) I| Process(pb, 0 , d i v i s o r , c a r r y , sum, q u o t i e n t , done, quotientnumber, t a u , TimeTable) Process(pb, 1 , d i v i s o r , c a r r y , sum, q u o t i e n t , done, quotientnumber, t a u , TimeTable) Process(pb, 2 , d i v i s o r , c a r r y , sum, q u o t i e n t , done, quot ientnumber, t a u , TimeTable) « (quotientnumber = MantBits ) -> quotientnumber := MantBits + 1 » *{* i:QIndex I WriteString(BEGIN c o n . c a t 3 ( I n t T o S t r i n g ( i , 10), : ", P r i n t D R A r r a y ( q u o t i e n t r e g ( i ) ) ) END) } I I « quotientnumber = MantBits + 1 -> quotientnumber : = quotientnumber + 1 » DRtoRes(result, q u o t i e n t r e g ) I | « quotientnumber = MantBits + 2 -> quotientnumber := quotientnumber + 1 » * W r i t e S t r i n g ( BEGIN con.cat2( " r e s u l t : ", r e s p r i n t ( r e s u l t , ResBits+2)) END) * W r i t e S t r i n g ( BEGIN p r i n t r e s u l t ( r e s u l t , ResBits+3, exp) END) 11 END; Process: P r o c e s s C e l l = STATE I n i t : BOOLEAN = TRUE; STATIC prev: INTEGER = (number+2) MOD 3; next: INTEGER = (number+1) MOD 3; me: INTEGER = number; BEGIN (* * enable e v a l u a t i o n , i f the successor stage 106 * has s t a r t e d t o precharge *) ( « * « NOT pb(me).v AND NOT pb(next).v -> pb(me).v, pb(me).tau := TRUE, t a u quotientnumber := quotientnumber + 1 » » (* * i f successor stage has f i n i s h e d 0. * and i s h o l d i n g the output, we can s t a r t * precharging *) M « pb(me).v AND pb(next).v AND done(next)(0).t pb(me).v := FALSE » *PutInRegister(quotient(next), quotientreg, quotientnumber) -> (* * when precharging i s f i n i s h e d , the done * s i g n a l should drop; * i f i n 0. mode ( i . e . no precharge), * and predecessor has value, can s i g n a l * output value *) I| StageProcess( pb, me,divisor, c a r r y , sum, done, TimeTable, tau) I| ChangeTime(tau, t a u , TimeTable) ) END; StageProcess: S t a g e C e l l = STATE muxout: DRArray(MantBits); propagatesum: D R A r r a y O ) ; adderdone: D u a l R a i l ; padderdone: D u a l R a i l ; cadderdone: D u a l R a i l ; qsldone: D u a l R a i l ; carrybit: DualRail; I n i t : BOOLEAN = TRUE; STATIC prev: INTEGER = (number+2) MOD 107 3; quotient, next: INTEGER = (number+1) MOD 3; me: INTEGER = number; BEGIN « I n i t -> adderdone.t, adderdone.f, qsldone.t, qsldone.f, c a r r y b i t . t , c a r r y b i t . f , I n i t , padderdone.t, padderdone.f := FALSE, FALSE, FALSE, FALSE, FALSE, FALSE, FALSE, FALSE, FALSE » I| * InitEmpty(muxout) * InitEmpty(propagatesum) * WriteString(BEGIN con.cat2( " I n i t i a l i z i n g i n StageProcess ", IntToString(me, 10)) END) « NOT I n i t » *( MUX(pb(me).v, q u o t i e n t ( p r e v ) , d i v i s o r , muxout, c a r r y b i t , TimeTable, me) II CarrySave(pb(me).v, c a r r y ( p r e v ) , sum(prev), muxout, carry(me), sum(me), c a r r y b i t , TimeTable, me) II CarryPropagate(pb(me).v, carry(me), sum(me), propagatesum, TimeTable, me) M QSL(pb(me), propagatesum, quotient(me), qsldone, TimeTable, t a u , me) II AdderDone(pb(me).v, sum(me), adderdone) II AdderDone(pb(me).v, carry(me), cadderdone) II QSLDone(pb(me).v, quotient(me), qsldone, TimeTable, me) II Done(pb(me), number, qsldone, done(me), done(next), tau) ) END; END. (* t r a n s i s t o r l e v e l module *) 108
- Library Home /
- Search Collections /
- Open Collections /
- Browse Collections /
- UBC Theses and Dissertations /
- Verifying a self-timed division chip
Open Collections
UBC Theses and Dissertations
Featured Collection
UBC Theses and Dissertations
Verifying a self-timed division chip Ono-Tesfaye, Tarik 1997
pdf
Page Metadata
Item Metadata
Title | Verifying a self-timed division chip |
Creator |
Ono-Tesfaye, Tarik |
Date Issued | 1997 |
Description | The formal verification of asynchronous circuits is challenging, because they often have non-deterministic timing relations between circuit components. This thesis presents a formal proof strategy for verifying the correctness of a dual-rail, asynchronous divider chip. For that purpose, this thesis will extend timing verification techniques that were originally developed for combinational logic to apply to dual-rail, self-timed designs. The proof strategy is refinement based and employs four progressively more detailed models of the divider. Key safety properties are first established for the abstract models using model checking. These properties are then shown to hold for the more detailed models by verifying refinement between adjacent levels in the model hierarchy. |
Extent | 3626084 bytes |
Genre |
Thesis/Dissertation |
Type |
Text |
File Format | application/pdf |
Language | eng |
Date Available | 2009-03-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.0050991 |
URI | http://hdl.handle.net/2429/6572 |
Degree |
Master of Science - MSc |
Program |
Computer Science |
Affiliation |
Science, Faculty of Computer Science, Department of |
Degree Grantor | University of British Columbia |
Graduation Date | 1997-11 |
Campus |
UBCV |
Scholarly Level | Graduate |
Aggregated Source Repository | DSpace |
Download
- Media
- 831-ubc_1997-0580.pdf [ 3.46MB ]
- Metadata
- JSON: 831-1.0050991.json
- JSON-LD: 831-1.0050991-ld.json
- RDF/XML (Pretty): 831-1.0050991-rdf.xml
- RDF/JSON: 831-1.0050991-rdf.json
- Turtle: 831-1.0050991-turtle.txt
- N-Triples: 831-1.0050991-rdf-ntriples.txt
- Original Record: 831-1.0050991-source.json
- Full Text
- 831-1.0050991-fulltext.txt
- Citation
- 831-1.0050991.ris
Full Text
Cite
Citation Scheme:
Usage Statistics
Share
Embed
Customize your widget with the following options, then copy and paste the code below into the HTML
of your page to embed this item in your website.
<div id="ubcOpenCollectionsWidgetDisplay">
<script id="ubcOpenCollectionsWidget"
src="{[{embed.src}]}"
data-item="{[{embed.item}]}"
data-collection="{[{embed.collection}]}"
data-metadata="{[{embed.showMetadata}]}"
data-width="{[{embed.width}]}"
async >
</script>
</div>
Our image viewer uses the IIIF 2.0 standard.
To load this item in other compatible viewers, use this url:
http://iiif.library.ubc.ca/presentation/dsp.831.1-0050991/manifest