EXPLOITING SYMBOLIC MODEL CHECKING FOR SENSING STUCK-AT FAULTS IN DIGITAL CIRCUITS Aleš Časar, Zmago Brezočnik, Tatjana Kapus University of Maribor, Faculty of Electrical Engineering and Computer Science, Slovenia Keywords: stuck-at faults, symbolic model checking, automatic test pattern generation, testing, CTL formulas, finite state machine, binary decision diagrams Abstract: This paper presents algorithms for automatic test pattern generation for discovering stuck-at faults in sequential digital circuits or proving that there are no stuck-at faults in the given circuit. A circuit is represented as a finite state machine. Properties for stuck-at faults expressed with CTL formulas which are valid in the circuit with stuck-at faults and generally not valid in the good circuit are generated. Validity of the formulas is checked by symbolic model checking, and for invalid formulas counterexamples are constructed which guide the circuit to the states which prove the absence of stuck-at faults. Test patterns guide the circuits exactly as the counterexamples. Experimental results for a set of benchmark circuits together with the time and space complexity analysis of the algorithms are also given. Uporaba simboličnega preverjanja modelov pri zaznavanju zatičnih napak v digitalnih vezjih Ključne besede: zatične napake, simbolično preverjanje modelov, avtomatsko generiranje testnih vzorcev, testiranje, formule CTL, končni avtomat, binarni odločitveni grafi Povzetek: V članku predstavljamo algoritme za avtomatsko generiranje testnih vzorcev, s pomočjo katerih pri sekvenčnih digitalnih vezjih odkrivamo zatične napake oziroma pokažemo, da zatičnih napak v danem primerku vezja ni. Vezje predstavimo kot končni avtomat. Za zatične napake generiramo lastnosti v obliki formul CTL, ki so veljavne v vezju z zatičnimi napakami in praviloma neveljavne v dobrem vezju. S simboličnim preverjanjem modelov preverimo veljavnost formul in za neveljavne formule skonstruiramo protiprimere, s katerimi vezje pripeljemo v stanja, ki dokažejo odsotnost zatičnih napak. Testni vzorci so sestavljeni tako, da izvajanje vezja vodijo po poti pro-tiprimerov. Teoretične raziskave so podkrepljene z eksperimentalnimi rezultati. Prikazana je tudi analiza časovne in prostorske zahtevnosti. 1 Introduction Testing of newly produced digital circuits is a necessity Since circuits are becoming larger and larger, it is impossible to perform exhaustive testing of the circuits nowadays. Therefore, a suitable trade-off between exhaustive testing and speed of testing (length of test patterns) should be made. We tend to discover (or prove their absence) as many circuit faults as possible but at moderate test pattern length. Many different faults can occur in a circuit, but stuck-at faults are the most common ones. Hence, we introduce the method which will find all possible single stuck-at faults in the circuit or prove that there is no stuck-at fault present in the circuit. Because enumeration methods [10] do not perform well with large circuits, we propose to use symbolic methods [5, 6]. A circuit is represented as a fi- nite state machine (FSM). FSMs are represented as Boolean functions and these with binary decision diagrams (BDDs). Properties of FSMs which are to be checked by symbolic model checking are expressed with CTL formulas. For every possible single stuck-at fault, a property which is valid in the circuit with that stuck-at fault and generally invalid in the good circuit can be generated. When the property is invalid, a counterexample can be found. If the test pattern guides the circuit exactly as the counterexample, the absence of the treated stuck-at fault is proved if testing with this test pattern ends successfully We neither deal with other types of possible faults nor with multiple stuck-at faults in this paper. Practice suggests that also multiple stuck-at faults can be discovered in most cases, but we did not prove that. A mentionable limitation of the proposed method is also the necessity of the insight into the circuits (logic values stored in flip-flops). In Section 2 we briefly show how to represent FSMs with BDDs, describe searching of reachable states, and symbolic model checking in CTL. Section 3 describes the methods of searching counterexamples and witnesses. The main part of the paper is Section 4 where we present algorithms for generation of properties for stuck-at faults. Experimental results for benchmark circuits with time and space complexity analysis are given in Section 5. We conclude with some discussion and plans for future work. 2 Preliminaries Binary decision diagrams (BDDs) are compact canonical representations of Boolean functions [2]. BDDs can be used for representing and manipulating sets if we represent sets by means of their characteristic functions [5, 6]. A deterministic finite state machine (FSM) M is a sixtuple M = (E, cS, Ö, 5, A, sq). where E is a finite set of input symbols, S a finite set of states, Ö a finite set of output symbols, <5 : 5 x E 5 a state transition function, A: cS X S -> O an output function, and sq e 5 an initial state. If we want to realize a FSM by a digital circuit, we have to encode the sets S, S, and 0 by binary symbols (e.g. 0 and 1). States are encoded by state variables. At least n = [logj icSj] state variables, m = [logs 1^11 input variables, and I = [logs l^^ll output variables are needed. Let y, Af, and Z represent the set of state variables, the set of input variables, and the set of output variables, respectively. Once the states and the input symbols of the circuit are encoded, next state variables are functions of present state variables and input variables. We denote next state variables by an added prime (') and write a transition function of a state variable y,; as y'i = Si{tJo,yi, ■ ■ . ,yn^l,Xo,Xi, . . .,X,n-l) (1) for« = 0,1,..., n " 1. We rather introduce transition relations Ti = y'i Si{tjo,yi, ■ ■ .,yn^i,xo,xi,.. (2) Namely, relations have much greater expressive power than functions [3]. Transition relations Ti can be combined by taking their conjunction to form the monoiithic transition reiation T = To • Ti • ... • T„_i. After the encoding, output variables are functions of present state variables and input variables. We write = Ai(?/0,2/l) ■ • ■ ,yn~-l,Xo,Xi, . . . ,X,n-l) (3) for? = 0,1,...,/-1. Let us very briefly show how we search reachable states of a FSM [1, 5, 6]. Let Si denote a set of states reachable in at most i steps. So represents a set of initial states. In our case we have = {so}. In general, a set of states reachable in at most i steps is represented by Si = 5i_iu|s' I 3a3s[a e SAs £ 5i_iA5(s,a) = s']| . (4) We continue with this procedure until in a step /c no new state is reached. In any case, this happens sooner or later, because we deal with FSMs, where the set of states S is finite. Then, Sk = Sk^i is a set of all reachable states. The logic which we use to specify properties of FSMs is a prepositional temporal logic of branching time, called Computation Tree Logic — CTL [9]. In this logic, each of the usual future time operators of linear-time temporal logic (G — giobaliyor invariantly, F — sometimes in the future, X — next time, U — untii) must be immediately preceded by path quantifier A (for all computation paths) or E (for some computational path). We thus obtain eight different CTL operators: AG, EG, AF, EF, AX, EX, AU, EU [1, 5, 6]. CTL formulas are constructed from atomic propositions using Boolean connectives and CTL operators. In the case of circuit verification, the set of atomic propositions is equal to the set y of state variables of the circuit. 3 Searching for Counterexamples and Witnesses One of the most important extensions of symbolic model checking is the ability to search counterexamples for some invalid and witnesses for some valid CTL formulas [8]. Counterexamples explain why a given CTL formula is invalid in a FSM, and witnesses show why a given CTL formula is valid. 3.1 Counterexamples Counterexample is a path in the computation tree which shows why a given CTL formula is invalid. Actually, this is evident from the last state on the path, but FSM must be guided to this state to demonstrate invalidity of the formula. It is impossible to find counterexamples for all invalid formulas. According to the definition of CTL formulas [5], they are constructed from atomic propositions. Boolean operators, and CTL operators. Let us look how these three constructs affect searching of counterexamples. Searching of a counterexample for an atomic proposition is a trivial task. Such a formula represents the characteristic function of the set of states where the formula is valid. Because counterexamples are searched only for invalid formulas, it suffices to check if the current state of the FSM is not in that set. Although there are 16 binary Boolean operators, all of them can be expressed by negation, conjunction, and disjunction. Searching for a counterexample for negation of a function means the same as searching for a witness for that (non-negated) function. Therefore, searching of a counterexample for / is equivalent to searching of witness for /. Searching of witnesses will be described in Section 3.2. When dealing with conjunction, a counterexample for a formula of the form / • g should be found. Because the formula is invalid (counterexamples are searched only for invalid formulas), at least one of the functions / or 5 is invalid. To find a counterexample for the whole function / • 3, it is enough to find either a counterexample for / or a counterexample for g. Of course, in the case one of the formulas / or g is valid, we should find a counterexample for the other one, which is invalid. It is not possible to find a counterexample for disjunction in all cases. If a formula of the form f + g \s invalid, then both formula / and formula g are invalid. To prove that, one should prove both simultaneously. Generally this is impossible to do with just one counterexample, but there are exceptions. If one of the formulas / or 5 is of such a kind that the counterexample for it is not a path but just a single state (this happens when a formula does not contain any CTL operators), then also a counterexample for disjunction can be found. We search a counterexample for the other formula and at the end also check that the current state is not in the set of states which our formula without CTL operators is the characteristic function for. Let us now look at another interesting exception. Triple Bodean operator ite{f,g,h) can be written also as f ■ g + J ■ h. If / represents a Boolean formula (without temporal operators) in such a construction, then exactly one of the disjunctives is invalid because of / in every state. There are two cases: 1. Formula / is valid in the given state. Operand / ■ h is invalid then and we have to show that operand /•(/is also invalid. It is known that factor / is valid, therefore we have to show that factor g is invalid. Actually we have to search for a counterexample for 5. 2. Formula / is invalid in the given state. In that case operand / ■ 5 is invalid because of /, and the only thing we have to prwe is that operand J ■ his also invalid. Because / is valid here, h is invalid accordingly. Therefore, a counterexample for h should be searched for. After explaining Boolean operators, let us devote now to CTL operators. Counterexamples can be searched only for CTL operators with universal path quantifier A. Namely, only these operators state that on every computation path a formula is valid, and a counterexample is one computation path where this formula is invalid. AX f states that formula / is valid in all successors of the present state. Problem of searching a counterexample for an invalid formula of such a kind is to find a successor of the present state where formula / is invalid. When an adequate successor is found, a counterexample for formula / should be found. According to formula AFf, every computation path from the present state should lead to a state where formula / is valid. If this is not true, we have to find a path where we will never reach a state where formula / is valid. Since computation paths are infinite, how at all can we show that something never happens along a given path? Paths are infinite indeed, but they lead over finite set of states. Therefore, at least one state on the path must occur repeatedly. When an already visited state is reached, the path from this state back to itself can safely be repeated infinitely often. Actually, the path ends with a cycle. It is not necessary that the initial part of the path is part of the cycle. In that case, the path is composed of the prefix and the cycle as shown in Fig. 1. It is enough to find a prefix o-a Figure 1: A path with prefix and cycle and a cycle to find such a path. When we return to an already visited state at traversing the states, we have found a counterexample as a proof that formula AFf is invalid indeed. Formula / must be invalid in every state along that path, therefore, counterexamples for itself should be found in every state on that path. However, those "nested" counterexamples must not go off the path, since our computation path would transform to a computation tree otherwise. To avoid such situations, formula / should not contain any CTL operators. Formula AG f says that on all the paths, formula / is valid all the time. In order to prove its invalidity, a path leading to a state where formula / is invalid has to be found. As with operator AX, from there on a counterexample for formula / has to be found in order to confirm its invalidity in the last state of the path for AGf. The last CTL operator containing the universal path quantifier \s A[f U g], which says that on all the paths, formula / is valid until a state where formula g is valid. In order to refute validity of formula A[f U g], either an infinite path on which formula g is never valid or a path which leads to a state where formula / is invalid and on which formula g is never valid has to be found. The case of the infinite path is similar to the counterexample construction with operator AF — only a prefix and a cycle terminating the infinite path have to be found. As in the case of AF, formula g must not contain any CTL operators. If one decides to search for a path leading to a state where formula / is invalid, one must. of course, continue with a counterexample for /. 3.2 Witnesses Witness is a path in the computation tree which indicates why a CTL formula considered is valid. In fact, the validity is evident from the last state of the path, but the FSM has to be led to that state in order for the path to demonstrate the validity As with counterexamples, witnesses cannot be found for every valid CTL formula. Since witnesses are in a sense dual to counterexamples, problems occur exactly with the CTL formulas dual to those CTL formulas, validity of which cannot be demonstrated by counterexamples. We now make an overview of the structural elements of CTL formulas and their influence on searching of witnesses. Searching of a witness for an atomic proposition is in fact the same as searching of a counterexample. The difference is that witnesses are searched for valid formulas. Therefore, it must be checked if the current state of the FSM is in the set determined by the characteristic function in the form of the given atomic proposition. Searching of a witness for negation of a function means the same as searching of a counterexample for the (non-negated) function. It follows that searching of a witness for / is equivalent to searching of a counterexample for /. Searching of the counterexamples is described in detail in Section 3.1. Another example is searching of a witness for a disjunction f + g. Since the formula is valid (as witnesses are searched only for valid formulas), at least one of the functions / and g is valid, in order to find a witness for function f + g, W therefore suffices to find either a witness for / or a witness for g. If one of the formulas is invalid, a witness for the valid one has to be found, of course. With counterexamples, there were some problems with disjunction, whereas due to duality of witnesses, similar problems now occur with conjunction, which is dual to disjunction. It is not always possible to find a witness for conjunction. If a formula of the form / ■ g is valid, then formula / and formula g must be valid. In order to demonstrate that, validity of both should be demonstrated simultaneously. As a witness must be a path, which must not have branches, this is generally not possible. Exceptions, however, exist also in this case. If one of the formulas / and g is such that its witness is a path containing just one state (this is the case when the formula does not contain any CTL operators), then a witness for the conjunction can be found as well. A witness for the other formula has to be found, and at the end, it has to be checked if the current state is also in the set of states whose characteristic function is the formula without CTL operators. Finally, let us look at the CTL operators and their influence on searching of witnesses. Witnesses can only be found for the CTL operators containing exis- tential path quantifier E. They say that there exists a computation path where a formula is valid, and a witness is simply one path which confirms the existence and validity of the formula. Formula EXf says that there exists a successor of the current state where formula / is valid. In order to find a witness for a valid formula of this form, a successor of the current state where formula / is valid has to be found. A witness for / must then be found from the successor state on. Formula EE f says that there exists at least one path leading to a state where formula / is valid. In order to prove its validity, a path leading to such a state has to be found and from there on, a witness for formula / has to be found. Formula EG f says that there exists an infinite path on which formula / is valid ail the time. We already know how to deal with infinite paths. A prefix and a cycle at the end of an infinite path have to be found, such that formula / is valid in every state of the path. When during passing from state to state, an already visited state is reached for the first time, the searching is finished. Since validity of formula / must be confirmed by the witness along the whole path, which must not be abandoned, the confirmation is possible only if formula / does not contain any CTL operators. We already know that E[fUg] says there exists a path where formula / is valid until a state is reached where formula g is valid. In order to find a witness, one of such paths must, therefore, be found. Formula / must again not contain any CTL operators, and starting from the last state, a witness for the validity of formula g in that state must be found. 3.3 Realization In order to implement symbolic model checking, we implemented only resolution of three CTL operators, EXf, E[fUg], and EGf, whereas the other five were expressed with them [5]. The same approach can be followed to realize searching of counterexamples and witnesses. For unrealized operators the searching can be realized as follows: • searching of a counterexample for AX f is replaced by searching of a witness for EX~f, • searching of a witness for EE f is replaced by searching of a witness for E[1U f], • searching of a counterexample for AFJ is replaced by searching of a witness for EGj, • searching of a counterexample for AG f is replaced by searching of a witness for E[lUj], • searching of a counterexample for A[f Ug] is replaced either by searching of a witness for E[gUj-g] or by searching of a witness for EGg. To find out if formula EXf is valid in a given state s using symbolic model checking, we start by the set Sf of states in which formula / is valid. This set will also be used to find a witness for validity of formula EXf in state s, which can be done if it is found that formula EXf is valid in state s. In order to find this witness, we have to find a successor of state s in which formula / is valid. In accordance with formula (4), the set of all successors of state s is calculated as follows: S' = |s' I 3a[a g S a<5(s,a) = s']| . (5) In the set S', we have to choose a successor of s in which formula / is valid, it follows that state s' must not only be in set S', but also in Sf, i.e. s' G n Sf must hold. This is illustrated in Fig. 2. The witness for In order to find a witness for formula E[f U g] In a state s, we must find a path from the state s in the set to a state in the set A path of the form (s,„,st„_i,..., so) will contain exactly w steps\ where for all states, Si e S^ and Syj = s. It is clear that states from the sets cannot be chosen arbitrarily. For any pair of states Si and Si-i, a transition from s,; to Si_i must exist. We, therefore, choose in each step a state Si_i which will also be in the set of all successors of state s^. If the set is denoted by S'', then we can write Si_i g n S^'. An example for w = 3 is shown in Fig. 4. Figure 2: Witness for EXf formula EXf In state s is, therefore, composed of two states, (s,s'), and is found in one step. When checking validity of formula E[fUg], we start with the set Sg of all states where formula g is valid. By gradually adding all such predecessors where formula / is valid, we obtain the set of all states where formula E[fUg] is valid. Let Sf be the set of all states where formula / is valid, and let S' denote the set of all states obtained until the i-th step of the procedure, the step included. Note that = Sg. The situation is shown in Fig. 3. The sets have the follow- s Figure 3: Set of states at checking formula E[f U g] ing characteristics: 1. CcS/U