1 e A f (Next!02) with 8'% • cr, or Inductive assumption. 3) Suppose g X Sat(a, g). By Lemma 4.3, 35 5 G A % ) such that 5 s C cr. Let T9 = T(59). Note that T9 G T % ) by construction and that 89 C r9. T9 C cr: the proof is by induction. 1- = h. • Proof. (=>•) Recalling the definition of ==§> on page 71, suppose V r 3 e Tb(g), 38h e A*(fc) w i t h ^ C r 3 . Suppose t X Sat(a, g). By Lemma 4.4, 3r9 e T % ) such that r5 C cr. By assumption then, 3Sh G A 9 (/i) , with Sh Q T 3 . By transitivity, C cr. By Lemma 4.3, g ^ Sat(a, h). (<£=) Suppose for all trajectories cr, t ^ Sat(cr, g) implies that t -< Sat(a, h). LetT9eT\g). Then by Lemma 4.4, t ^ Sat(r9,g). By the assumption that g=^h, t ^ Sat(r9, h). By Lemma 4.3, 3g. • Lemma A . l l . Suppose g=C>h. Then Next g=$> Next h Proof. Let a G UT 3 t = Sat(a, Next g). (1) t = Sat(a>i,g) Definition of Sat. (2) t = Sat(a>i,h) g=$>h. (3) t = Sat(Xa>u Next h) Definition of Sat. • (4) t = Sat(a, Next h) (3), monotonicity of Sat, Lemma 4.8. (5) Next g =>Next h. Corollary A.12 (Time-shift - Theorem 5.15). Suppose g=oh. Then Vt > 0, Next*Nexthi and g2 =t>/i2-Then 0i A 02 = t > ^ i A / J 2 -Proof. Let cr e TZT and suppose t = Sat(a, g\ A 02). Appendix A. Proofs (1) t = Sat(a,gi) A Sat(a,g2) Definition of Sat(a,gi A g2). (2) t = Sat(a,gi), i = 1,2 Lemma 3.2(2). (3) t = Sat(a,hi), i = 1,2 Sincegi=o/ii, i = 1,2. (4) t = Sat(a,hi) ASat(a,h2) (3) (5) t = Sat(a, hihh2) Definition of Sat(a, hx A h2). As cr is arbitrary, gi A g 2 =t>hi/\h2. Theorem A.14 (Disjunction - Theorem 5.17). Supposegi=t>/ii andg2=t>h2. Then gx V g2=t>hi V / i 2 . Praq/! Let cr G 7?.r a n d suppose t = Sat(a,gi V g2). (1) t = Sat(a,gi)V Sat(a,g2) Definition of 5ar(cr, ^ V g2). (2) t = 5af(cr, ^ j ) , for i = 1 or i = 2 Lemma 3.2(1), Lemma 4.8. (3) t = Sat(a, hi), for i = 1 or i = 2 Since gi==i>hi, i = 1,2. (4) t = Sat(a,hi) V Sat(a,h2) (3) (5) t = Sat(a,hi V /i 2) Definition of Sar(<7, V /i 2). As cr is arbitrary, gi V g2=S>hi V fc2. Lemma A.15. Suppose A*(5f) CT> A k(/i), a G 7^ r and t = Sctf(cr, fc). Then t = Sat(a,g). Proof. (1) t^Sat(h and Ak(g) \ZV Al(gi) and A\hi) Q-p A^h). Then 0 i= o / i i . Proof. Suppose a £ TZj- is a trajectory such that t = Sat(a, gi). (1) t = Sat(cr,g) Lemma A.15. (2) t = Sat(cr,h) g=$>h. (3) t = Sat( a,Lemma A.15. (4) g1=c>hi Since a is arbitrary. • Theorem A.17 (Transitivity - Theorem 5.19). Suppose gl=c>h1 andg2=c>h2 and that At(g2) C.v At(g1) II A*( / i i ) . Then gi=t>h2. Proof. Suppose a £ TZT is a trajectory such that t = Sat(a, gi). (1) t = Sat(a,hi) g1==c>hi (2) t = Sat(a,giAhi) Definition of Sat(a, gi A hi). (3) 35 £ A*(flfi A / i i ) 9 5 C cr Lemma 4.3. (4) A*(01 A hi) = At(gl) II A*( / i i ) By definition of A*. (5) 35' £ A t ( 0 2 ) 3 8'\Z8 A\g2)nv A\gi)U A\hi). Appendix A. Proofs 220 (6) 8'Q a Applying transitivity to (3) and (5). (7) t d Sat(a, 92) From (6) by Lemma 4.3. (8) t = Sat(a 92) From (7) by Lemma 4.8. (9) t = Sat(a h2) g2=0>h2. (10) 9i = *>h2 Since a was arbitrary. • Lemma A.18 (Substitution Lemma). Suppose |= (\ g=z>h } and let £ be a substitution: then f= i\ £(g)=$>£(h) Proof. Let (j) be an arbitrary interpretation of variables and a £ TZr be an arbitrary trajectory such that t = Sat(v,(Z(g))). (1) Let0' = 0o£ (2) t = Sat(a,(f>'(g)) Rewriting supposition. (3) ' is an interpretation of variables By construction. (4) t = Sat(a,(f>'{h)) \= $g=i>h). (5) t = Sat(a,(f)(t(h))) Rewriting (4). (6) |= { £(g)=t>£(h)} h \: then |= {(e 0)=o(e /i) ). Proof. Suppose t = Sat(a, e ^ g) for some a £ 7£e) V 0, and note that Sat(a, ->e) G By the definition of the satisfaction relation, either: (i) t = Sat(a, ->e). In this case, by definition of satisfaction, t = Sat(a, e =>• h). Appendix A. Proofs 221 (ii) t = Sat(a,g). In this case, by assumption Sat(a, h). So, by definition of satisfaction, t = Sat(a, e =>• h). As a was arbitrary the result follows. Theorem A.20 (Specialisation Theorem — Theorem 5.20). Let E = [(ei, £ 1 ) , . . . , (e„, £ n)] be specialisation, and suppose that |= {] g=S>h ThenHHGjO^E^n. • (1) Fori = 1,... ,n , h U.-(flO=i>6('Or-(2) H(e,-^ 6(s))=^ (e,-=> (3) h 4 A?=1(et- e<(0))=> A?=1(e,- =* £(/i)) (4) |= ^S(^)=l>S(/»)^ By Lemma A. 18. By Lemma A. 19. Repeated application of Theorem A. 13. By definition. • Theorem A.21 (Until Theorem — Theorem 5.21). Supposegl=z>h\ and g2=l>/i2. Then g\ Untilg 2=f>^i Until h2. Proof. Let a £ TZT be a trajectory such that t = Sat(a,gi Untilg 2)-(1) 3i3 t = A}~0 Sat(a, Next^i) A Sat(cr, Next^2) (2) t = Sat(a,Nextig2) and t = Sat(a, Next^gi), j = 0,... , i' — 1 (3) t = Sa^Next*^) and t = 5ar(cr,Next-7fci), j = 0,... ,i — 1 (4) t = AJ~o 5ar(cri? Next^i) A San>,-, Next8'/i2) (5) t = Sat(a,hi Until / i 2 ) (6) gi Untilg2=t>hi Until fc2 Definition of Sat, Lemma 3.2(1), Lemma 4.8. Lemma 3.2(2). g2=C>h2, Corollary A. 12. g1=£>hi, Corollary A.12. Definition of Sat. Definition of Sat. Since a was arbitrary. • Appendix B Detail of testing machines This chapter presents the details of testing machines. Section B . l formally defines composi-tion of machines. Subsequent sections build on this by showing how testing machines can be constructed and composed with the circuit under test: Section B.2 presents some notation used; Section B.3 presents the building blocks from which testing machines are constructed; and Sec-tion B.4 shows how model checking is accomplished. B . l Structural Composition The focus of the research on composition is the property composition described in Chapter 5. However, sometimes it is also desirable to reason about different models and use partial results to describe the behaviour of the composition of the models. A full exploration of composing models of partially ordered state spaces is beyond the scope of this thesis — there are important considerations which need attention [129]. A partial exploration of the area is useful though for two reasons: (1) it gives a flavour of how structural composition could be used; and (2) some of the definitions given are needed in justifying the details of testing machines. The content of this section is very technical. Although conceptually the composition of sys-tems is very simple, the notation needed to keep track of the detail is not. This section is included for completeness and the details of this section are not needed in understanding the thesis. This section has three parts. First, composition of models is defined formally. Second, in-ference rules for reasoning about a composed model is given. The third part elaborates on com-position for circuit models, where the definition of composition has natural instantiation. 222 Appendix B. Detail of testing machines 223 B.l.l Composition of Models Definition B.l. Let Mi = ((Si, ^i),KuYi),M2 = « S 2 , • 2),U2, Y 2 ) , and M = ((S, C),7e ,Y)be models. Let X i , X 2 and X be the bottom elements of Si, S2 and S; Z i , Z 2 , and Z be their top elements; and let Gi, G2 and G be the simple predicates of «S*i, S2 and S respectively. If p : Si x S2 -» S, pi : G\ —> G and p2 : G2 -¥ G then M is a p-composition of Mi and M2if 1. pis monotonic; 2. p(X 1 ,X 2 ) = Xand. /o(Z 1,Z 2) = Z; 3. q = gi(si) ==• q = pi(gi)(p(suX2)); 4. q = g2{s2) =>• q = p2(g2)(p(Xus2)); 5. p(Yi(si),Y2(s2))QY(p(si,s2)). The required properties on p may seem onerous, and indeed in general they may be too restric-tive. However, for the application of composition needed in this thesis they are sufficient. In particular, for compositions where the 'outputs' of one circuit are connected to the 'inputs' of another, these conditions will be met. Definition B.2. We inductively extend the domain of the pi by defining • Pi(gAh) = pi(g) A pi(h); • pii^g) = -"(^ (sO); • pi(Nextg) = Next pi(g); • pi(g\Jntilh) = pi(g) Until pi(h). Appendix B. Detail of testing machines 224 Definition B.3. Let Mi, M2 and be models and M a p-composition of Mi and Mi- Let cr 1 £ ~~h) (1) -ig = SatMl(crl,h) a, b Inductive assumption. Definition B.2 and satisfaction. Sat(a\-^f) = ^Sat(cr1,f) Appendix B. Detail of testing machines 225 (2) -. g r< SatM{p{i(/o((7^0,<7|o),Pi(^i)) A ... A Sar^ (p (al3-, J _ 1 ,cr 2 , J _ 1 ) ,pi( / i i ))A From (1) by induction assumption. . . . A S ^ A 1 ( / > ( c r > i _ 1 , a | J _ 1 ) , p 1 ( / i i ) ) A (2) and (3) Definition of satisfaction. • Lemma B.2 . Let Mi, M2 and be models and M a p-composition of Mi and M2. Let i 6 {1,2}, and suppose that: (1) p is a surjection; (2) cr = p(al,a2), and t •< 5a?x(cr, pi(gi)) implies that t •< SatMi(a\gi). Then K< 1 Pi(9i)^>Pi{h)) iff KM, 4 h Appendix B. Detail of testing machines 226 Proof. Suppose \=M. <] gi=$>hi \ (1) Suppose t •< SatM(a, pi(gi)) (2) 3a 1, a2 3 cr = p(a1,a2) p is a surjection. (3) t < SatMi(cr\gi) By hypothesis (2). (4) t -< SatM, (o-'', hi) Since 1=^ . t\ gi=?>hi \ . (5) t< SatM(a,pi(hi)) ByLemmaB.l. (6) Therefore ^ <| p{ (g{) =§>p; (hi)) Suppose \=M. § pi(gi)=§>pi(hi) ) (1) Suppose t X SatMt( Cn is represented as a vector of next state function (Y[ l ] , . . . ,Y[n]) where each Y[j] : Cn -> C and Y(s) = (Y[l](s),... ,Y[n](s)). To compose two circuit models, we identify r pairs of nodes (each pair comprising one node of both circuits) and 'join' the pairs (i.e., informally, think of these pairs as being soldered to-gether, or physically identical). The state space of the composed circuit consists of mi + m2 — r components. The first mi — r components are the components of Mi that are not shared with Appendix B. Detail of testing machines 227 M2. The next m2— r components are the components of M2 that are not shared with Mi. The final r components are the r components shared by both Mi and M2. The formal definition of composition is a little intricate since it identifies state components by indices. The difficult part of the definition is identifying for each state component in the composed circuit the component or components in Mi and M2 that make it up.1 The idea is simple — the book-keeping is unfortunately off-putting. Let Ii — ( a i , . . . , ar), and Ji = (a[,... , a' _r) be lists of state components of Mi. If s £ Si, then the s[aj] are the components of the state space that are shared with M 2 and the s [a'j] axe the components of the state space that are not. We place the natural restriction that Ii and Jx are disjoint, and that their elements are arranged in strictly ascending order. I2 = (61 , . . . ,br) and J2 = (b[,... , b'm2_r) are the corresponding of lists for M2. Each (a,-, bj) pair is a pair of state components that must be 'joined'. Let convi(j) be the component of M to which the j-th component of Mi contributes. For-mally, define ( k when 3a'k € J i 9 a'k = j mi + m2 — r + k when Ba^ € h 9 a-k — j mi - r + k when 3b'k £ J2 9 b'k = j mi + m2 — r + k when 3bk £ h 3 bk = j Since the Ii and J, are distinct, we can define an inverse to convi. Define indexi(j) = k where convi(k) — j. Note that indexi is not defined on all of {1,... , mi + m2 — r], but that where it is defined, indexi(j) is the component of the state space of Mi which contributes to the j-th component of M. With this technical framework, composition can be defined easily. If si £ 1In practice, composition is a lot easier. Nodes are labelled by names drawn from a global space. We use the convention that if the same name appears in both circuits, then the nodes they label are actually the same physical node. Thus, the pairs that must be connected are implicit and do not have to be given. Appendix B. Detail of testing machines 228 Cmi and s2 e C™2, define Q(SUS2) by Q{SI,S2) = (si[indexi(l)],... , si[indexi{mi — r)], s2[index2{mi — r + 1)],... , s2[index2(mi + m2 — 2r)], si[mflfexi(mi + m 2 — 2r + 1)] U s2[index2(mi + m 2 — 2r + 1)],... , .si[/ndfexi(r)] U s2[ina'ex2(m1 + m2 — r)] ) Part of defining the composition is to define the mapping from simple predicates in M i and M2 to M. For T L n , this is easy since it is only for predicates of the form [j] that a non-trivial mapping has to be defined. Define convi(j)] when g = [j] for some j when g a constant predicates. Then define where Yi[wwfej:i(j)]((s[co/iVi(l)],... ,s[coravi(rai)])), j < mi — r Y[j](s) Y 2 [ i /Mte*2 ( j ) ] ( (s [c0 / iv 2 ( l ) ] , . • • , s[c0 / iv 2 (m 2 )])) , mi — r < j < mi + m 2 — 2r Yi[/nflfexi( i;)]((5[convi(l)],... , s[convi(mi)])) U Then X is \Y 2{index2{j)){(s[conv2{\)],... , s[corav2(m2)])), ? a ^-composition of A ^ i and M2, denoted g{M\,M2). m\ + m 2 — 2r < j Appendix B. Detail of testing machines 229 Lemma B.3. Q meets all the criteria given in Definition B. 1. Proof. (1) Q is monotonic. Q is defined component-wise. Each component is constructed from the identity and join functions. Since both of these are monotonic, monotonicity follows. (2) £(UTOl,Um2) = u m i + m 2 ~ r a n d £ ( Z m i , Z T O 2 ) = Zmi+m2-r Follows straight from the definition of g. (3) q = 51(61) implies thatq ^ /0i(0i)(y>i(si, U™2)) a. Suppose q = # i ( s i ) , let s = Q(SI, Um 2) . b. si[j] = s[convi(j)] From definition of g(si, U7™2). c. Let ^ G C i . Suppose gx — [j] for some j. d. P i ([j]) = [convi(j)]. Definition of 0 i . e- =9i(si) (b)and(d). f. gi(gi)(s) = q By assumption and (e). Otherwise gx must be one of the constant predicates {_L, f , t, T } . g- Qi{9i)=9i Definition of g. h- q = Qi{gi)(s) Q\{g\) is constant. (4) Similarly q = g2{s2) => q r< 02(02X0(1^, s2)). (5) ^ ( Y i ( s i ) , Y 2 ( 3 2 ) ) r< Y(^ ( s i , s 2 ) ) . Proved by showing for all j , Appendix B. Detail of testing machines 230 Q{Y1(s1),Y2(s2))\j]^Y\jMsus2)). Suppose j < mi — r. £(Yi( 5 i) ,Y 2 (s 2 ))[j] = Yi(si)[i/ufe*i(j)] = Y1[indexi(j)](s1) = Yi[indexi(j)] = ((s[convi(l)],... ,s[co/iVi(mi)])) = Y[j](.) Similarly if mi — r < j < mi + m 2 — 2r, ^ (Yi ( 5 i ) , Y 2( 5 2))[j] = Y2[/mfcc2(j)](s2) = Y[j](s) Suppose mi + m 2 — 2r < j £(Yi(6i ) ,Y 2 ( . 2 ) ) [ j ] = Yi(si)[tmfej:i(j)] U Y 2(s 2)[m^x 2(j)] = Yi[mJexi(j)](si) U Y2[iWex2(j)](s2) = Y[j](,) • Lemma B.3 is important because it means that Lemma B . l can be used. Furthermore, where composition of machines is done is such a way that the 'outputs' of one machine are connected to the 'inputs' of the other (so there is no 'feedback' — signals go from one machine to the other, but not vice versa.), Lemma B.2 applies too (to the circuit that provides the outputs). This definition is dependent on 71? I2, J\ and J2; for convenience, the following short-hand is used: Q(A, B)(ri,... , r*) refers to the composition of A and B where the r 1 ? . . . , com-ponents of A are shared with the first k components of B; formally Ii = ( r l 5 . . . ,rk), Jx = (1,. . . , rx - 1, r i + 1,... , r f c - 1, r f c + 1,... , k), I2 = (1,. . . , k) and J2 = (k + 1,... , k). Appendix B. Detail of testing machines 231 B.2 Mathematical Preliminaries for Testing Machines This section assumes the state space of the system is Cn for some n. There is nothing inherent in the method which limits the state space to this. However, from a notational point of view it is easier to explain the method with this simple case; furthermore, this is the important, practical case. The method generalises easily to an arbitrary complete lattice. Suppose that M i and M2 have both been derived from a common machine, M , using a sequence of compositions. (Assume that M = (C n ,Y*) , M i = ( C " + m i , Y i ) and M 2 = (Cn+m2, Y 2 ) .) By the definition of composition the two next state functions Y x and Y 2 re-stricted to Cn are identical and the same as Y * . M{ (i = 1,2) consists of M and a tester T2. The relative composition of M i and M 2 with respect to M is the composition of M , 7\ and T 2. All of this could be described by composition, but it is convenient to define a specific notation. Formally, reLcompM(M1, M 2 ) = (Cn\ Y ) , where n' — n + mi + m 2 and if the current state is s, (ti,... , tn>) = Y(s) is defined by: ^ Y 2 ( ( s i , . . . , s n , s n + m i + i , . . . ,sn>))\j] when n +mi < j < n' B.3 Building Blocks Basic Block BBA Some predicates may depend (in some way) on the value of node 1 at a time t\ and node 2 at time t2. (Formally, a 'node' is a component of the state space; informally since we are reasoning about physical circuits nodes are wires in the circuit.) The purpose of BB A is to provide delay slots so that both values of interest are available at the same 'time'. BBA takes two parameters: a function g : C —> C which is used to combine the values, and n which indicates how many delay slots need to be constructed. Figure B . l depicts BBA(g, 4). when 1 < j < n + m\ Appendix B. Detail of testing machines 232 a Figure B . l : BBA(g,3): a Three Delay-Slot Combiner BBA(g, n) consists of two nodes which act as input nodes, n delay slots, and one node which is the output value of the machine. The two inputs nodes are typically part of the original circuit, which is why BBAs next state function does not affect the first two components. Formally, JL, when j = 1,2; BBA(g,n) = (Cn+3,Y) where if t = Y(s),then^ = < when j = 3 , . . . n + 2; 5 r ( s i , 5 n _ i ) , whenj = n + 3. The comp Jest operator adds the BBA circuit to an existing circuit. Given a machine M and a predicate g which depends on the value of ix at time 11 and i2 at time t2, the composite machine (M plus the testing circuit) is defined by: compJest(M,g, (W2)) (B.l) QiMiBBAfah -t2))(H,i2) ifh>t2 g(M,BBA(g,t2 -ti))(i2,ii) otherwise. The problem with the BBA testing machine is that if the two defining times are far apart, the testing circuit could be large due to the need to retain and propagate values, which has both space and computation costs associated. There is an alternative approach - build a memory into the circuit which keeps the needed information. Define BBA(g) = ( C 5 , Y ) . If the state of the machine is ( s i , . . . , s 5 ) , think of sx and s2 as the inputs, and s 5 as the output. s4 is used as the memory, and s3 indicates whether Appendix B. Detail of testing machines 233 the memory's value should be reset or maintained. Formally, when j 1,2,3 when j 4 and s 3 = 0 < (B.2) whenj 4 and s3 = 1 when j 5 Define compJest(M,g, (ti, «i) (<2 , i 2 ) ) g{M,BBA{g))(i1,i2) if * i > t2 (B.3) p ( M , BBA(g)){i2, i\) otherwise. Although in general the definition of equation B.3 will be more efficient, it cannot always be used. To see why consider this example. Let g and h be two predicates containing no temporal operators, where the result of g can be found at node ix and the value of h at node i2. Suppose we want to evaluate the predicate g A Next3/*. Implicit in this is that we are interested in ix at time 0 and i2 at time 3. For this we could use the second implementation of comp Jest and get the new machine compJest(M, (Xx, y.x A y), (0, i i ) , (3, i2)). Now suppose that we are interested in the predicate Exists [(0,10)] (g A Next3/i). This asks whether there is a time t between 0 and 10 such that g holds at time t and h holds at time t + 3. For this predicate, the second implementation will not work since it only remembers the value of g at one particular time, and we need to have the value of g at a sequence of times. The general rule in choosing between the implementations is that if the predicate for which the tester being constructed is within the scope of temporal operators such as E x i s t s and G l o b a l , then the first implementation must be used; otherwise the second, more efficient im-plementation can be used. Appendix B. Detail of testing machines 234 Basic Block BB B BBB is used when we need to combine the value of a predicate at a number of different times. For example, Globalg and Existsg depend on the value of g at a sequence of times. Define BBB(g,k) = ( C * + 2 , Y ) where if t = Y(s) then: JL when j = 1 S! when j = 2 f(sj,Sj-i) otherwise. Figure B.2 depicts this graphically. t3 = { Figure B.2: BBB(g,4) Basic Block BB c This is just a simple latch with a comparator. 5 5 c = (C 3, Y ) where Y((s i , s2, s3)) = (-L , 5 2 , 5 l = S2). Inverter Define / = ( C 2 , Y ) where Y ( ( s i , s 2 » = ( J - , - -* ! ) . B.4 Model Checking This section shows how to accomplish the following: Appendix B. Detail of testing machines 235 Given a machine M and an assertion of the form |= t\ A=Og construct a ma-chine M' and trajectory formulae A', C such that |= \ A=f>g } -£=^ > |=M» Every temporal formula, g, has an associated tuple (i,t, A, M')\ i indicates that the formula can be evaluated by examining the i-th component of the state space of the new machine; t indi-cates the time at which the component should be examined; A' gives a set of trajectory formulas which are used as auxiliary antecedents for the new machine; and M' is the new machine. The tuple is defined recursively on the structure of the temporal formula.2 1. g is ([i] — v). The tester which checks this compares the value of node i to v. The asso-ciated tuple is (n + 2,1, A', M'), where • A' = ([n + 2]=v) • M' = g(M,BBc){i). 2. g is Nextjg'. This does not require any extra circuitry — the tester that tests g' is already built in, and the only difference is that the result is checked at a different time. If the tuple associated with g is (i,t, A, M'), the tuple associated with Next jg is (i, t + j, A, M'). 3. gis~>g'. If the tester for g' is already built, an inverter will compute the answer for g. So, if the tuple associated with g is (i, t, A, M'), the tuple associated with -•/ is ( | M " | , t + 1, A, M"), where M" = g(M, 4. g is g'(gi,g2). Typically g' would be conjunction or disjunction. The tester takes as its input the results of gx and g2 and applies g' to them. Let the tuple associated with gx be (ii, tx, A i , M i ) and the tuple associated with g2 be (i2,t2, A2, M2). Assume that \M\ \ — n + mi and \M2\ = n + m2. 2Note that in this discussion M refers to the original machine, and n = \M\. Appendix B. Detail of testing machines 236 The tuple associated with g(gi,g2) is ( |M' | , max(£i, tf2) + 1, M A A2, M') where M ' = compJest(M",g,(t1,n+ml),(t2ln+ml+m2)) andM" = rel.compM(Mi, M 2 ) . 3 5. fi- is Global [(i, j)] This can be computed as Next8'(NextV A . . . A^ext^-'V))-Evaluating this directly is too inefficient (since lots of redundant work will be done). The following approach computes g' exactly once and then provides appropriate circuitry to combine this value produced at various times. If the tuple associated with g' is (i1? t, A 1 ; Mx), where \MX | = mi then the new tuple associated with g is ( |M' | , t + 1, A ' , M') where: A smaller, more efficient testing machine can be built provided that Global operator is not nested within another temporal operator. In this case, suppose the tuple associated with g is (iu tx, Ax, Mx), where | M i | = mi. The new tuple is ( |M' | ,*i + 1,A',M') where: |^si A s2 when j = 2. • A'= Ai A(Next*1[mi + 1] = 1). 6. g = Exists [(i,j)] g'. This is analogous to the Global case, and can be computed as Next'(Next V V . . . V (Next^'-4'^')). All the remarks pertaining to the Global oper-ator apply to the Exists operator - the difference is that instead of conjunction being 3Recall that M is the underlying machine. . M' = g(M, BBB((Xx, y.x A y), (j - i)))(n) • M' — g(M,M")(ii) • M" = (C 2 ,Y) • ift = Y(s) then: when j = 1. Appendix B. Detail of testing machines 237 applied, disjunction is applied. This shows that De Morgan's laws have a direct corre-spondence in the testing machines. 7. The bounded strong until, weak until, and periodic operators are all derived operators (see Definition 3.8). A straight-forward approach to model-checking these operators is model-check their more primitive definitions. For all three, smaller and more efficient machines are possible too. There are competing threads here—the more operators the easier it is for a verifier to express properties, but with the wider choice comes the cost of greater complexity for the verifier. Con-structing testing machines for the derived operators using the primitive definitions is not the most efficient approach: if the operators are going to be used, optimised testing machines should be constructed; but, if they are not going to be used the verification system will be more com-plicated that it needs to be. There are two further types of optimisations which could be done. Testing machines are not canonical—there are different ways with different complexities of evaluation. The rewriting of formulas could yield improvement. The other issue has been discussed already: in some cases the testing machine needed for a formula depends on whether that formula is embedded within other temporal operators. If a formula stands by itself, then its satisfaction can checked by ex-amining one component of the testing circuit at one instant in time. However, if the formula is embedded within some of the temporal operators, then we need to know the satisfaction of the formula at a number of instants in time. Appendix C Program listing C l FL Code for Simple Example 1 let c_size = bit_width; let bwidth = ' c_size; let i = IVar " i " ; let j = IVar " j " ; let k = IVar "k"; let 1 = IVar "1"; let GND = "GND"; let a = Var "a"; let A = "a"; let B = "b"; let C = "c"; let D = "d"; let E = "e"; let FNode = "f"; let Globallnput = ((A ISINT i)_&_(B ISINT j)_&_(C ISINT k)) FROM 0 TO 100; let l i s t l = [ ( " i " , 1 upto 8), ("j", 9 upto 16), ("k", 17 upto 24)]; let varmapl = BVARS l i s t l ; let varmap2 = BVARS (("a", [25]):listl); let Al = Globallnput; let Cl = D ISBOOL (i > j) FROM 10 TO 100; let TI = VOSS varmapl (Al ==» Cl) ; let A2 = Globallnput _&_ ((D ISBOOL a) FROM 10 TO 100); let C2 = Globallnput _&_ ((E ISINT i WHEN a) _&_ (E ISINT j WHEN (Not a)) FROM 20 TO 100); let T2 = VOSS varmap2 (A2 ==» C2); let A3 = E ISINT 1 C ISINT k FROM 20 TO 100; let C3 = FNode ISINT (1 '+ k) FROM 50 TO 100; let T3 = VOSS varmapl (A3 ==» C3) ; let proof = let GI = SPTRANS [] TI T2 in let G2 = SPTRANS [] GI T3 in G2 ; 238 Appendix C. Program listing 239 C.2 FL Code for Hidden Weighted Bit let N = bit_width; let x = IVar "x"; let InputNode = let BufferNodel= let Chooser = let j = IVar " j " ; " InputNode"; "bufferl"; "chooser"; "error"; let CountNode = "CountNode let BufferNode2= "buffer2"; let Result = "result"; let Error let varmapl = BVARS([("x",1 upto N)]); let BufferTheorem = VOSS varmapl ((InputNode ISINT x FROM 0 TO 1000) ==» ( (BufferNodel IS INT x) _&_ (BufferNode2 ISINT x) FROM 5 TO 1000)); letrec add_bits x num = x = N => BIT2 ('N) num | (BIT2 C x ) num) '+ (add_bits (x+1) num); letrec count_of num = add_bits 1 num; let CounterGoal = (BufferNodel ISINT x FROM 0 TO 990) ==» (CountNode ISINT (count_of x) FROM 400 TO 990); let CounterTheorem = VOSS varmapl CounterGoal; let stagel = CONJUNCT BufferTheorem (AUTOTIME [] BufferTheorem CounterTheorem); let seg x = BWID ('Nbit) x; let kthBit k var = (BIT2 ('k) var) '= (BIT2 ( ' 1) C D ) ; letrec case_analysis var j = letrec case k = " k=l => Result ISBOOL (kthBit k var) WHEN (j '= (seg C k ) ) ) | (Result ISBOOL (kthBit k var) WHEN (j '= (seg ('k)))) _& (case (k-1) ) in case N; infix 3 ISBOOL_VEC; letrec ISBOOL_VEC [x] [y] = x ISBOOL y A ISBOOL_VEC (x:rx) (y:ry) = (x ISBOOL y) _&_ (rx ISBOOL_VEC ry); let ChooserGoal= ((CountNode ISINT j FROM 0 TO 400) _&_ (BufferNode2 ISINT x FROM 0 TO 400)) ==>> ( ( (case_analysis x j) _&. Appendix C. Program listing 240 (Error ISBOOL (seg('O) '= j ) ) ) FROM 300 TO 400); l e t ChooserTheorem = VOSS varmap2 ChooserGoal; l e t Proof = ALIGNSUB [] stagel ChooserTheorem; C.3 F L Code for Carry-Save Adder l e t A = Nnode "A"; l e t B = Nnode "B"; l e t C = Nnode "C"; l e t D = Nnode "D"; l e t E = Nnode "E"; l e t a = Nvar "a"; l e t b = Nvar "b"; l e t c = Nvar "c"; l e t bdd_order = o r d e r _ i n t _ l [b, c, a]; l e t l e t l e t l e t l e t range sum_lhs sum_rhs Antl Conl (bit_width-l)--0; (D+E) « r a n g e » ; (a+b+c) «range>> ; ((A == a)??) and ((B == b) ??) and ((C NextG 3 ( (sum_lhs == sum_rhs) ??); c)??) ; l e t T l = prove_voss bdd_order adder Antl Conl; C.4 FL Code for Multiplier // miscellaneous l e t high_bit = entry_width l e t max_time = 800; l e t out_time = 3; - 1; // 0..entry_width-l II- Node, va r i a b l e declarations l e t l e t l e t l e t l e t l e t l e t l e t l e t A = Nnode AINP; B = Nnode BINP; RS i = Nnode (R_S i ) ; RC i = Nnode (R_C i ) « (high_bit-l)--0» ; TopBit i = Nnode (R_C i) <>; / / BDD v a r i a b l e o r d e r i n g f o r e a c h s t a g e o f m u l t i p l i e r l e t m_bdd_order { n : : i n t } = n = 0 => o r d e r _ i n t _ l [b, a] | n = e n t r y _ w i d t h => o r d e r _ i n t _ l [ p a r t i a l n , d] | o r d e r _ i n t _ l [b<>, a , p a r t i a l n , d ] ; l e t z e r o _ c o n d i = ( ( T o p B i t i ) = = ( ' 0 ) ) ? ? ; l e t i n t e r v a l n = n <= e n t r y _ w i d t h => [ ( ' ( n * o u t _ t i m e ) , 'max_t ime)] | [ ( ' ( n * o u t _ t i m e + 2 * e n t r y _ w i d t h ) , ' m a x _ t i m e ) ] ; l e t I n p u t A n t s = A l w a y s ( i n t e r v a l 0) (( (A == a) ?? ) and ( (B == b) ? ? ) ) ; l e t O u t p u t C o n s = l e t l h s = RS e n t r y _ w i d t h i n l e t r h s = (a * b) « ( 2 * e n t r y _ w i d t h - l ) - - 0 » i n A l w a y s ( i n t e r v a l ( e n t r y _ w i d t h + l ) ) ( ( l h s = = r h s ) ? ? ) ; / / A n t e c e d e n t f o r row n o f t h e m u l t i p l i e r l e t MAnt { n : : i n t } n = 0 => A l w a y s ( i n t e r v a l 0) ( ( (A == a ) ? ? ) and ( ( B « n » == b « n » ) ? ? ) ) | A l w a y s ( i n t e r v a l n) (( (A == a ) ? ? ) and ( ( B « n » == b « n » ) ? ? ) and ( (RS (n-1) == ( p a r t i a l (n-1)))??) and ( (RC (n-1) == d ) ? ? ) and ( z e r o _ c o n d (n-1)) ); / / Consequent o f row n o f t h e m u l t i p l i e r l e t r e s _ o f _ r o w n = l e t power n = Npow ('2) ('n) i n l e t l h s = (RS n) + (power ( n + l ) ) * ( R C n) i n l e t r h s = n=0 => a * b < < 0 » | ( ( p a r t i a l (n-1)) +(power n) * d) + (power n) *a * (b « n » ) i n ( ( l h s == r h s ) ? ? ) ; Appendix C. Program listing 242 C o n _ o f _ s t a g e n = l e t p o w e r n = Npow ('2) ('n) i n l e t l h s = (RS n) + ( p o w e r ( n + l ) ) * ( R C n) i n l e t r h s = a * b « n - - 0 » i n A l w a y s ( i n t e r v a l (n+1)) ( ( l h s == r h s ) ? ? a n d ( z e r o _ c o n d n ) ) ; MCon { n : : i n t } = A l w a y s ( i n t e r v a l (n+1)) ( ( r e s _ o f _ r o w n ) a n d ( z e r o _ c o n d n ) ) ; Mthm n = l e t b d d _ o r d e r = ( m _ b d d _ o r d e r n) i n l e t a n t = MAnt n i n l e t c o n = MCon n i n p r o v e _ v o s s b d d _ o r d e r m u l t i p l i e r a n t c o n ; p r e a m b l e _ t h m = l e t s t a r t = Mthm 0 i n P r e c o n d i t i o n I n p u t A n t s s t a r t ; d o _ p r o o f _ m a i n _ s t a g e n m p r e v i o u s _ s t e p = l e t c u r r = Mthm n i n l e t c u r r ' = G e n T r a n s T h m p r e v i o u s _ s t e p c u r r i n l e t c u r r e n t = P o s t c o n d i t i o n ( C o n _ o f _ s t a g e n) c u r r ' i n n = m => c u r r e n t | d o _ p r o o f _ m a i n _ s t a g e (n+1) m c u r r e n t ; l e t m a i n _ s t a g e = d o _ p r o o f _ m a i n _ s t a g e 1 h i g h _ b i t p r e a m b l e _ t h m ; l e t a d d e r _ p r o o f = l e t p o s t _ a n t _ c o n d = (( (RS h i g h _ b i t ) == ( p a r t i a l h i g h _ b i t ) ) ? ? ) a n d (( (RC h i g h _ b i t ) == d ) ? ? ) a n d (( ( T o p B i t h i g h _ b i t ) == ('0))??) i n l e t p o s t _ a n t = A l w a y s ( i n t e r v a l e n t r y _ w i d t h ) p o s t _ a n t _ c o n d i n l e t p o w e r = Npow ('2) ( ' e n t r y _ w i d t h ) i n l e t r h s = ( ( p a r t i a l h i g h _ b i t ) + p o w e r * d ) < < ( b i t _ w i d t h - l ) - - 0 » i n l e t p o s t _ c o n _ c o n d = ( ( R S e n t r y _ w i d t h ) -= r h s ) ? ? i n l e t p o s t _ c o n = A l w a y s ( i n t e r v a l ( e n t r y _ w i d t h + l ) ) p o s t _ c o n _ c o n d i n p r o v e _ v o s s ( m _ b d d _ o r d e r e n t r y _ w i d t h ) m u l t i p l i e r p o s t _ a n t p o s t _ c o n ; l e t p r o o f = G e n T r a n s T h m m a i n _ s t a g e a d d e r _ p r o o f ; Appendix C. Program listing 243 C.5 F L Code for Matrix Multiplier Proof // miscellaneous let high_bit = entry_width - 1 ; // 0..entry_width-l let max_time = entry_width < 10 => 100 | 10*entry_width; let clock_time = max_time; // half a clock cycle let out_time = 3; / / let prove_result = prove_voss_fsm; let prove_result_static = prove_voss_static; // Node, variable declarations // global let Clock = Bnode CLK; // individual cells let A u v = Nnode (AINP u v); let B u v = Nnode (BINP u v); let IN_C u v = Nnode (C_Inp u v); let OUT_C u v = Nnode (C_Out u v); let M = make_fsm sys_array; let RS u v i = Nnode (R_S u v i ) ; let RC u v i = Nnode (R_C u v i)<<(high_bit-l)--0>>; let TopBit u v i = Nnode (R_C u v i) «high_bit>>; let a = (Nvar "a") « (entry_width-l)—0»; let b = (Nvar "b" ) « (entry_width-l)—0»; let c = Nvar "c"; let d = (Nvar "d")«(high_bit-l)—0»; let e = Nvar "e"; let partial {n :: int} = e «(n+high_bit)--0>>; // BDD variable ordering for each stage of multiplier let m_bdd_order {n::int} = n = 0 => order_int_l [b, a] | n=entry_width => order_int_l [partial n, d] | order_int_l [b<>, a, partial n, d]; // timings let Duringlnterval n f = During (n*out_time, max_time) f; letrec ClockAnt n = let range = 0 upto (n-1) in let false_range = map (\x.(('(2*x*clock_time), '(2*x*clock_time+clock_time-l)))) range in let true_range = map (\x.('(2*x*clock_time+clock_time), Appendix C. Program listing 244 '(2*(x+1)*clock_time-l))) (butlast range) in (Always false_range ((Clock == Bfalse)??)) and (Always true_range ((Clock == Btrue )??)); let InputAnts u v = Duringlnterval 0 ((A u v '= a) and (B u v '= b)); let zero_cond u v i = TopBit u v i '= ('0); // Antecedent for row n of the multiplier let MAnt u v {n::int} = n = 0 => Duringlnterval 0 ( ( A u v '= a ) and ( (B u v)<> '= b<>)) | Duringlnterval n (( A u v '= a) and ( (B u v)<> '= b<>) and ( RS u v (n-1) '= (partial (n-1))) and ( RC u v (n-1) '= d) and ( zero_cond u v (n-1)); // Consequent of row n of the multiplier let res_of_row u v n = let power n = Npow ('2) ('n) in let lhs = (RS u v n) + (power (n+l))*(RC u v n) in let rhs = n=0 => a * b <<0>> | ((partial (n-1)) +(power n) * d) + (power n) *a* (b « n » ) i n lhs '= rhs; let Con_of_stage u v n = let power n = Npow ('2) ('n) in let lhs = (RS u v n) + (power (n+l))*(RC u v n) in let rhs = a * b«n--0>> in Duringlnterval (n+1) ((lhs '= rhs) and (zero_cond u v n)); let MCon u v {n::int} = Duringlnterval (n+1) ((res_of_row u v n ) and (zero_cond u v n)); let Mthm u v n = let bdd_order = (m_bdd_order n) in let ant = MAnt u v n in let con = MCon u v n in prove_result bdd_order M ant con; let preamble_thm u v = print (nl^"Doing preamble"~nl) seq Appendix C. Program listing 245 l e t s t a r t = Mthm u v 0 i n ( s t a r t c a t c h s t a r t ) s e q P r e c o n d i t i o n ( I n p u t A n t s u v) s t a r t ; l e t r e c d o _ p r o o f _ m a i n _ s t a g e u v n m p r e v i o u s _ s t e p = l e t c u r r = Mthm u v n i n l e t c u r r ' = G e n T r a n s T h m p r e v i o u s _ s t e p c u r r i n l e t c u r r e n t = P o s t c o n d i t i o n ( C o n _ o f _ s t a g e u v n) c u r r ' i n ( p r i n t ( n l " " D o i n g M [ " " ( i n t 2 s t r u ) " " , n " ( i n t 2 s t r v ) " " ] ( " ~ ( i n t 2 s t r n ) ~ " ) " ~ n l ~ n l ) s e q ( c u r r e n t c a t c h c u r r e n t ) ) s e q ( n = m => c u r r e n t | d o _ p r o o f _ m a i n _ s t a g e u v (n+1) m c u r r e n t ) ; l e t m a i n _ s t a g e u v = d o _ p r o o f _ m a i n _ s t a g e u v 1 h i g h _ b i t ( p r e a m b l e _ t h m u v ) ; l e t a d d e r s _ p r o o f u v = l e t p o s t _ a n t _ c o n d = ( (RS u v h i g h _ b i t ) '= ( p a r t i a l h i g h _ b i t ) ) a n d ( (RC u v h i g h _ b i t ) '= d) a n d ( ( T o p B i t u v h i g h _ b i t ) '= CO)) i n l e t p o s t _ a n t = D u r i n g l n t e r v a l e n t r y _ w i d t h p o s t _ a n t _ c o n d i n l e t p o w e r = Npow ('2) ( ' e n t r y _ w i d t h ) i n l e t r h s = ( ( p a r t i a l h i g h _ b i t ) + p o w e r * d ) « ( b i t _ w i d t h - l ) - - 0 > > i n l e t p o s t _ c o n _ c o n d = (RS u v e n t r y _ w i d t h ) '= r h s i n l e t p o s t _ c o n = D u r i n g ( e n t r y _ w i d t h * ( o u t _ t i m e + 2 ) , c l o c k _ t i m e ) p o s t _ c o n _ c o n d i n l e t b d d _ o r d e r = m _ b d d _ o r d e r e n t r y _ w i d t h i n ( p r i n t " D o i n g a d d e r " s e q ( p o s t _ c o n c a t c h p o s t _ c o n ) ) s e q p r o v e _ r e s u l t b d d _ o r d e r M p o s t _ a n t p o s t _ c o n ; l e t c e l l _ o u t _ t i m e = [ ( ' ( 2 * c l o c k _ t i m e ) , ' ( 3 * c l o c k _ t i m e ) ) ] ; l e t r e g i s t e r _ p r o o f u v = l e t c _ a n t = ( ( ( R S u v e n t r y _ w i d t h ) '= ( p a r t i a l e n t r y _ w i d t h ) ) a n d ( ( I N _ C u v) '= c ) ) i n l e t c _ a n t ' = ( C l o c k A n t 2) a n d ( D u r i n g ( e n t r y _ w i d t h * ( o u t _ t i m e + 2 ) , c l o c k _ t i m e ) c _ a n t ) i n l e t c _ r h s = ( p a r t i a l e n t r y _ w i d t h ) + c i n l e t c _ c o n = (OUT_C u v) '= c _ r h s i n l e t c _ r e g = p r o v e _ r e s u l t ( o r d e r _ i n t _ l [ c , p a r t i a l e n t r y _ w i d t h ] ) M Appendix C. Program listing 246 c _ a n t ' ( A l w a y s c e l l _ o u t _ t i m e c _ c o n ) i n ( ( p r i n t " D o i n g r e g i s t e r " ) s e q c _ c o n c a t c h c _ c o n ) s e q c _ r e g ; // o n e _ p r o o f u v : p r o v e s t h a t t h e ( u , v ) - t h c e l l w o r k s // c o r r e c t l y l e t o n e _ p r o o f u v = // P r o v e t h a t m u l t i p l i e r p a r t s w o r k ( u n c l o c k e d ) l e t m _ s t a g e = m a i n _ s t a g e u v i n ( m _ s t a g e c a t c h m _ s t a g e ) s e q // t a k e i n t o a c c o u n t c l o c k i n g a n d t h e p a r t i a l sum i n p u t l e t n e w _ a n t s = I n p u t A n t s u v a n d ( C l o c k A n t 2) a n d ( D u r i n g l n t e r v a l 0 (IN_C u v '= c ) ) i n l e t new_thm = P r e c o n d i t i o n n e w _ a n t s m _ s t a g e i n // show t h e a d d e r p a r t o f t h e c e o l w o r k s l e t a _ p r o o f = a d d e r s _ p r o o f u v i n ( a _ p r o o f c a t c h a _ p r o o f ) s e q // A d d c l o c k i n g t o t h e a d d e r p r o o f l e t c o m p _ p r o o f = G e n T r a n s T h m new_thm a _ p r o o f i n // Show t h a t t h e r e g i s t e r s w o r k l e t r _ p r o o f = r e g i s t e r _ p r o o f u v i n ( ( r p r o o f c a t c h r _ p r o o f ) s e q // s t i c k t h e m a l l t o g e t h e r l e t r e s u l t = ( n o r m a l i s e C o n ( G e n T r a n s T h m c o m p _ p r o o f r _ p r o o f ) ) i n r e s u l t ) ; l e t r e c m a k e _ c e l l _ r o w _ l i s t p _ p r o c u v = v = a r r a y _ d e p t h => [] | l e t r e s = p _ p r o c u v i n p r i n t ( s n d ( t i m e r e s ) ) s e q ( r e s s e q ( r e s : ( m a k e _ c e l l _ r o w _ l i s t p _ p r o c u (v+1)))); l e t r e c m a k e _ p r o o f _ l i s t p _ p r o c u = u = a r r a y _ w i d t h => [] | ( m a k e _ c e l l _ r o w _ l i s t p _ p r o c u 0): ( m a k e _ p r o o f _ l i s t p _ p r o c (u+1)); l e t c e l l _ p r o o f _ l i s t = m a k e _ p r o o f _ l i s t o n e _ p r o o f 0; // Show t h a t t h e c e l l s a l s o p r o g a t e t h e i r A a n d B i n p u t s Appendix C. Program listing 247 l e t o n e _ p r o o f _ p r o p a g a t e A u v = l e t a n t s = ( D u r i n g l n t e r v a l 0 (A u v '= a ) ) a n d ( C l o c k A n t 2) i n l e t a b _ c o n = A u (v+1) '= a i n l e t a b _ r e g = p r o v e _ r e s u l t ( m _ b d d _ o r d e r 0) M a n t s ( A l w a y s c e l l _ o u t _ t i m e a b _ c o n ) i n a b _ r e g ; l e t o n e _ p r o o f _ p r o p a g a t e B u v = l e t a n t s = ( D u r i n g l n t e r v a l 0 ( ( B u v ) '= b ) ) a n d ( C l o c k A n t 2) i n l e t a b _ c o n = (B (u+1) v) '= b i n l e t a b _ r e g = p r o v e _ r e s u l t ( m _ b d d _ o r d e r 0) M a n t s ( A l w a y s c e l l _ o u t _ t i m e a b _ c o n ) i n a b _ r e g ; l e t A p r o p a g a t e _ p r o o f _ l i s t = m a k e _ p r o o f _ l i s t o n e _ p r o o f _ p r o p a g a t e A 0; l e t B p r o p a g a t e _ p r o o f _ l i s t = m a k e _ p r o o f _ l i s t o n e _ p r o o f _ p r o p a g a t e B 0; l e t c e l l _ p r o o f u v = e l (v+1) ( e l (u+1) c e l l _ p r o o f _ l i s t ) ; l e t A p r o p a g a t e _ p r o o f u v = e l (v+1) ( e l (u+1) A p r o p a g a t e _ p r o o f _ l i s t ) ; l e t B p r o p a g a t e _ p r o o f u v = e l (v+1) ( e l (u+1) B p r o p a g a t e _ p r o o f _ l i s t ) ; l e t em_thm = ( [ ] , [ ] , [ ] ) ; / / // T h e * _ p r o o f _ l i s t c o n t a i n s a l l t h e p r o o f s t h a t t h e i n d i v i d u a l // c o m p o n e n t s o f t h e h a r d w a r e w o r k c o r r e c t l y . T h e r e s t o f t h e // p r o o f shows t h a t when c o n n e c t e d t o g e t h e r t h e y p r o d u c e // t h e r i g h t m a t r i x m u l t i p l i c a t i o n r e s u l t l e t r e c I n s e r t A c t i v e T h e o r e m a d d f n ( { u : : i n t } , { v : : i n t } , { n e w _ t h m : : t h e o r e m } ) [] = [ ( u , [ ( v , a d d f n new_thm e m _ t h m ) ] ) ] A I n s e r t A c t i v e T h e o r e m a d d f n (u,v,new_thm) ( ( a u , a l i s t ) : b r e s t ) = l e t r e c P u t A c t i v e T h e o r e m l n ( { v : : i n t } , { n e w _ t h m : : t h e o r e m } ) [] = [ ( v , a d d f n new_thm em_thm)] A P u t A c t i v e T h e o r e m l n ( v , new_thm) ( ( a v , a v l i s t ) r v r e s t ) = v = a v => ( a v , a d d f n new_thm a v l i s t ) : v r e s t | ( a v , a v l i s t ) : ( P u t A c t i v e T h e o r e m l n ( v , new_thm) v r e s t ) i n u = a u => ( a u , P u t A c t i v e T h e o r e m l n ( v , new_thm) a l i s t ) : b r e s t | ( a u , a l i s t ) : ( I n s e r t A c t i v e T h e o r e m a d d f n ( u , v , n e w _ t h m ) b r e s t ) ; Appendix C. Program listing 248 l e t r e c R e t r i e v e T h e o r e m { u : : i n t } { v : : i n t } •[] = ( [ ] , [ ] , [ ] ) /\ R e t r i e v e T h e o r e m u v ( ( a u , a l i s t ) r b r e s t ) = l e t r e c G e t A c t i v e T h e o r e m v [] = ( [ ] , [ ] , [ ] ) A G e t A c t i v e T h e o r e m v ( ( a v , a v l i s t ) : v r e s t ) = v = a v => a v l i s t | G e t A c t i v e T h e o r e m v v r e s t i n u = a u => G e t A c t i v e T h e o r e m v a l i s t | R e t r i e v e T h e o r e m u v b r e s t ; l e t I n s e r t A c t i v e L i s t a d d _ f n t h m _ l i s t c u r r e n t = i t l i s t ( \ x A y . I n s e r t A c t i v e T h e o r e m a d d _ f n x y ) t h m _ l i s t c u r r e n t ; // V E R I F I C A T I O N CONDITION /// I n p u t s p e c i f i c a t i o n s l e t s e t l n p u t I n p N o d e {u :: i n t } {v :: i n t } { i : : i n t } { n _ v a l :: N} = l e t i n p u t = D u r i n g ( i * 2 * c l o c k _ t i m e , ( i + 1 ) * 2 * c l o c k _ t i m e - l ) ( I n p N o d e u v '= n _ v a l ) i n ( u , v . I d e n t i t y i n p u t ) ; l e t a l l = Nvar " a l l " l e t a l 2 = Nvar " a l 2 " l e t a l 3 = Nvar " a l 3 " l e t a l 4 = Nvar " a l 4 " l e t a21 = Nvar " a21" l e t a22 = Nvar "a22" l e t a23 = Nvar "a23" l e t a24 = Nvar "a24" l e t a31 = Nvar "a31" l e t a32 = Nvar "a32" l e t a33 = Nvar "a33" l e t a34 = Nvar "a34" l e t a41 = Nvar "a41" l e t a42 = Nvar "a42" l e t a43 = Nvar "a43" l e t a44 = Nvar "a44" l e t b l l = Nvar " b l l " l e t b l 2 = Nvar " b l 2 " l e t b l 3 = Nvar " b l 3 " l e t b l 4 = Nvar " b l 4 " l e t b21 = Nvar " b21" l e t b22 = Nvar "b22" l e t b23 = Nvar "b23" l e t b24 = Nvar "b24" l e t b31 = Nvar "b31" l e t b32 = Nvar "b32" l e t b33 = Nvar "b33" l e t b34 = Nvar "b34" l e t b41 = Nvar "b41" l e t b42 = Nvar "b42" l e t b43 = Nvar "b43" l e t b44 = Nvar "b44"; l e t t h e _ i n p u t s = // aO a l a2 a3 bO b l b2 b3 [ ([ '0, '0, '0, '0] , [ '0, '0, '0, '0] ) , //o ([ '0, '0, '0, '0] , [ '0, '0, '0, '0] ) , / / l ([ '0, '0, '0, '0] , [ '0, '0, '0, '0] ) , 7/2 ([ '0, '0, '0, '0] , [ '0, '0, '0, '0] ) , //3 ([ '0, a l l , '0, '0] , [ '0, b l l , '0, '0] ) , //4 ([ '0, '0, a21. '0] , [ '0, '0, b l 2 , '0] ) , //5 ( [ a l 2 , '0, '0, a31] , [b21, '0, '0, b l 3 ] ) , //6 ([ '0, a22, '0, '0] , [ '0, b22, '0, '0] ) , in (t '0, '0, a32, '0] , [ '0, '0, b23, '0] ) , //8 ([a23, '0, '0, a42] , [b32, '0, '0, b 2 4 ] ) , //9 ([ '0, a33, '0, '0] , [ '0, b33, '0, '0] ) , //10 ([ '0, '0, a43, '0] , [ '0, '0, b34, '0] ) , / / l l Appendix C. Program listing 249 ([a34, '0, '0, ([ '0, a44, '0, ([ '0, '0, '0, ([ '0, '0, '0, '0], [b43, '0, '0] , [ '0, b44, ' 0 ] , [ ' 0, , ' 0, '0], [ '0, '0, '0,- '0] ) , //12 '0, '0] ) , //13 •o,.. '0] ) , //14 '0, '0] ) ] •//15; // Output specifications let timeForOutputs = // 1 2 3 4 / / [ [ 6, 7, 8, 9] , // 1 [ 7, 9, 10, 11], // 2 [ 8, 10, 12, 13], // 3 [ 9, 11, 13, 15] // 4 ] ; . let outputFor row col = el col (el row timeForOutputs); let InputForCells = [ ] ; let addfirst x (a,b,c) = (x:a,b,c); let addsecond x (a,b,c) = (a,x:b,c); let addthird x (a,b,c) = (a,b,x:c); let InputAtStage n the_lists = val (avals, bvals) = el (n+1) the_inputs in let l e f t _ l i s t = map (\x.setlnput A {x::int} 0 n (el (x+1) avals)) (0 upto (array_depth-l)) in let r i g h t _ l i s t = map (\x.setlnput B 0 x n (el (x+1) bvals)) (0 upto (array_width-l)) in let down_list = (map (\x.setlnput IN_C (array_depth-l) {x::int} n ('0)) (0 upto (array_width-l)))@ (map (\x.setlnput IN_C x (array_width-l) {n::int} ('0)) (0 upto (array_depth-2))) in let resl = InsertActiveList addfirst l e f t _ l i s t the_lists in let res2 = InsertActiveList addsecond r i g h t _ l i s t resl in InsertActiveList addthird down_list res2; let start_step = InputAtStage 0 [] ; let this_step = start_step; let num_step = 0; let PropagateVal addfn row col okl {ok2::bool} res o l d _ l i s t = okl AND ok2 => InsertActiveTheorem addfn (row, col, res) o l d _ l i s t | o l d _ l i s t ; let PropagateRes row col a l l res res_l = Appendix C. Program listing 250 let c_index = "C"~(num2str(array_width-col-l+row)) in a l l AND (row*col = 0) => (c_index, res, (row, col)): res_l | res_l; letrec ProcessStageRow n {row::int} [] so_far = so_far A ProcessStageRow n row ((col, colthms):rest) (prop_list, res_l) = let make_step (a, b, c) = let ok a n = length a > n in let all_thms = (Identity(ClockAnt ((n+1)*2))):(a@b@c) in let ab_inps = (a@b) in let a l l = ok all_thms 3 in let curr_gen = a l l => Conjunct [cell_proof row col, Apropagate_proof row col, Bpropagate_proof row col] | length ab_inps = 2 => Conjunct [Apropagate_proof row col,Bpropagate_proof row col] | ok a 0 => Apropagate_proof row col | Bpropagate_proof row col in let curr_thm = Transform (TimeShift (2*n*clock_time)) curr_gen in let inps = Conjunct all_thms in let res = normaliseCon (GenTransThm inps curr_thm) in let new_l = PropagateVal addfirst row (col+1) (col<(array_width-l)) (ok a 0) res prop_list in let new_r = PropagateVal addsecond (row+1) col (row<(array_depth-l)) (ok b 0) res new_l in let new_d = PropagateVal addthird (row-1) (col-1) ((row*col) > 0) a l l res new_r in let new_rl= PropagateRes row col a l l res res_l in empty ab_inps => (prop_list, res_l) | (new_d, new_rl) in ProcessStageRow n row rest (make_step colthms); letrec ProcessStageProof n [] so_far = so_far /\ ProcessStageProof n ((row,rowthms):rest) so_far = let current = ProcessStageRow n row rowthms so_far in (print ("Doing row "~(int2str row)"nl)) seq (current catch current) seq ProcessStageProof n rest current; Appendix C. Program listing 251 let do_step n start_step = letrec perform m curr_step = let current = ProcessStageProof m (InputAtStage m curr_step) ([] , []) in (print ("Performing step ""(int2str m)~nl~nl)) seq (current catch current)'seq m = n => [snd current] | (snd current):(perform (m+1) (fst current)) in perform 0 start_step; • let output_list = do_step 15 []; // present results let ShowRes t r e s _ l i s t = el (t+1) r e s _ l i s t ; let Show t node = let res = ShowRes t output_list in find (\(x,y,a,b) . (x=node) AND ( (a* {b: : int}') = 0)) res; let OutputOfArray row col = let strip (Always r f) = f in val (a, th, b, c) = Show (outputFor row col) ("C"'(num2str(3+row-col))) in strip (con_of th) ; letrec PrintRowOutput row col = (col = array_width+l) => nl'nl | ("(""(int2str row)~" ,""(int2str col)~") :"~ (el2str (OutputOfArray row col))"nl) "(PrintRowOutput row (col+1)); letrec PrintOutput row = row = array_depth + 1 => nl I (PrintRowOutput row 1) " (PrintOutput (row+1)); Index =g>,71 = 0 , 71 C ,42 ET>,73 n,76 ^,47 abstract data type, 120 abstraction, 6, 38 antecedent, 70 assertions, 71, 83 £ , 4 8 B8ZS encoder, 143 BDD, 19 variable ordering, 20, 126 bilattice, 47 Binary decision diagrams, see BDD bottom element model, 42 truth domain, 48 branching time, 45 C, see circuit model carry-save adder, see CSA characteristic representation, 118 circuit model, 63 correctness, 89 satisfaction relation, 64 state space, 10 complete lattice, 7 composition of models, 223 compositional theory, 35, 185 inference rules TL, 92-104 TL„, 104-106 compositionality, 6, 35 completeness, 187 property, 91-113 structural, 222-230 conjunction rule, 94 consequence rules, 96 consequent, 70 CSA, 134, 143 defined,112 verification, 143 verification code, 240 A, A*, A f , see defining sequence set data representation, 120 De Morgan's Law Q.49 TL, 60, 207 defining pair, 53 defining sequence, 35 defining sequence set, 77-78 defining set, 53 defining trajectory, 35 defining trajectory set, 81 depth, 59 direct method, 131 disjunction rule, 95 domain information, 188 downward closed, 8 S, 85 FL, 116 future research, 186 generalised transitivity rule, 111 guard rule, 102 hand proof, 24 heuristic, 126 252 Index hidden weighted bit, 141, 239 identity rule, 93 IFIP WG10.5 benchmark matrix multiplier, 162 multiplier, 149 implication <2,50 TL, 57 inconsistency, 42, 70 inference rules implementation, 123-128 theory, 92-104 information ordering state space, 42, 183 truth domain, 48 integer, 120 interpretation, 61 interpretations representation, 117 join, 7 lattice, 7, 183 linear time, 45 logic quaternary, 184 definition, 47-51 motivation, 11 temporal, 21 mapping method, 134 matrix multiplier circuit, 162 meet, 7 min g, 72 modal logic, 21 model checking combined with theorem proving, 31 review, 27-31 model comparison, 23 model structure, 41 monotonic, 8 multipliers example verifications, 147 floating point, 148 IFIP WG10.5 benchmark, 149 other work, 160 verification code, 240 next state function, 43, 45-47 next state relation, 45^17, 187 non-determinism, 43, 187 notation sequences, 56 OBDDs, see BDD V, see power set parametric representation, 118 partial order, 7, 48, 183 partial order state space, 8 power set, 73 preorder, 7, 74 prototype, 15, 31, 123 Q, see logic,quaternary Q -predicate, 52 quaternary logic, see logic, quaternary TZ, see realisable states IZr, see trajectory, realisable range, 54 realisable fragment of TL„, 65, 89 states, 42-43 trajectory, 69 Sf, see trajectory satisfaction scalar, 56 symbolic, 62 simple, 54 specialisation definition, 102 discussion, 99-103 Index 254 heuristic, 127 rule, 103 state explosion problem, 5 state representation, 118, 183 strict dependence, 111 substitution, 100 substitution rule, 100 summary of results, 183-186 symbolic model checking, 30 symbolic simulation, 63 symbolic trajectory evaluation, 83-88 algorithm, 131, 132, 134 introduced, 11 original version, 33 T, T \ T f , see defining trajectory set temporal logic, 21 testing machines, 132 theorem prover, 25 combined with model checking, 31-33 combined with STE, 123 thesis goals and objectives, 12-15 outline, 15 time-shift heuristic, 127 time-shift rule, 93 TL algebraic laws, 60, 207 boolean subset, 85, 100 equivalence of formulas, 59 scalar, 52-59 semantics, 56, 62 symbolic, 60-63 syntax, 55, 61 T L n , 63—65 trajectory, 69 assertions, 35 _ defining trajectory set, 81 formulas, 34 minimal, 72 realisable, 69 trajectory evaluation algorithms, 128 transitivity rule, 98 truth ordering, 48 X,42 unrealisable behaviour, 42 until rule, 103 upward closed, 8 variable ordering, see BDD, variable order-ing variables, 60 verification condition, see assertions Voss, 31, 116 U,42 Y , 43 ~~