Abdelouahab Arouche

FINITE REPRESENTATIONS OF THE BRAID GROUP COMMUTATOR SUBGROUP

Keywords: 2000 Mathematics Subject Classification. Primary 20F36, 20C40; Secondary 20E07 Braid group, commutator subgroup, representation, symmetric group, special linear group. 1

We study the representations of the commutator subgroup Kn of the braid group Bn into a finite group Σ. This is done through a symbolic dynamical system. Some experimental results enable us to compute the number of subgroups of Kn of a given (finite) index, and, as a by-product, to recover the well known fact that every representation of Kn into Sr , with n > r , must be trivial.

Introduction

In [START_REF] Silver | Augmented group systems and shifts of finite type[END_REF], D. Silver and S. Williams exploited the structure of the kernel subgroup K of an epimorphism χ : G → Z, where G is a finitely presented group, to show that the set Hom (K, Σ) of representations of K into a finite group Σ has a structure of a subshift of finite type (SFT), a symbolic dynamical system described by a graph Γ; namely, there is a one to one correspondence between representations ρ : K → Σ and bi-infinite paths in Γ.

We apply this method to the group B n of braids with n-strands, with χ being the abelianization homomorphism and Σ the symmetric group S r of degree r or the special linear group over a finite field SL 2 (F q ). The subgroup K n = ker χ is then the commutator subgroup of B n .

It is a well known fact that for a given group K, there is a finite to one correspondence between its subgroups of index no greater than r and representations ρ : K → S r . This correspondence can be described by ρ -→ {g ∈ K : ρ (g) (1) = 1} .

The pre-image of a subgroup of index exactly r consists of (r -1)! transitive representations ρ. (ρ is said to be transitive if ρ (K) operates transitively on {1, 2, ..., r}). This will allow us to draw some conclusions about the subgroups of finite index of K n , which motivates the choice of S r ; we motivate that of SL 2 (F q ) by the fact that any representation of K n into any group Σ has range in the commutator subgroup [Σ, Σ], for n ≥ 6.

We give an algorithm to compute Hom (K n , Σ), for n ≥ 5 . Some experimental results enable us to compute the number of subgroups of K n of a given (finite) index, and, as a by-product, to recover the well known fact that Hom (K n , S r ) is trivial for n ≥ 5 and r < n . Since every representation in Hom (B n , Σ) restricts to an element of Hom (K n , Σ), we enhance the given algorithm in order to compute Hom (B n , Σ).

Generalities

Let B n be the braid group given by the presentation:

σ 1 , ..., σ n-1 σ i σ j = σ j σ i ; |i -j| ≥ 2 σ i σ j σ i = σ j σ i σ j ; |i -j| = 1 ,
(see [BuZi] for additional background). Let β ∈ B n be a braid. Then β can be written as :

β = σ ε1 i1 • • • σ ε k i k , with i 1 , • • •, i k ∈ {1, • • •, n -1} and ε i = ±1.
Define the exponent sum of β (in terms of the σ i 's) denoted by exp(β), as:

exp(β) = ε 1 + • • • + ε k .
Then exp(β) is an invariant of the braid group, that is, it doesn't depend on the writing of β. Moreover, exp(β) : B n → Z is a homomorphism. Let H n denote its kernel. Then the Reidemeister-Schreier theorem [LySc] enables us to find a presentation for H n . We choose the set

• • •, σ -m 1 , σ -m+1 1 , • • •, σ -1 1 , 1, σ 1 , σ 2 1 , • • •, σ m 1 , • • • as a Schreier system of right coset representatives of H n in B n . Putting z m = σ m 1 σ 2 σ -1 1 σ -m 1 for m ∈ Z, and x i = σ i σ -1 1 for i = 3, • • •, n -1, we get the following presentation of H n : H n = z m , m ∈ Z x i , i = 3, • • •, n -1 x i x j = x j x i , |i -j| ≥ 2; x i x j x i = x j x i x j , |i -j| = 1; z m z m+2 = z m+1 , z m x 3 z m+2 = x 3 z m+1 x 3 , m ∈ Z; z m x i = x i z m+1 , i = 4, • • •, n -1; m ∈ Z.
Example 1. We have:

H 3 = z m |z m z m+2 = z m+1 ; ∀m ∈ Z is a free group on two generators z 0 = σ 2 σ -1 1 and z -1 = σ -1 1 σ 2 ,
and

H 4 = z m , t z m z m+2 = z m+1 , z m tz m+2 = tz m+1 t, m ∈ Z . Note that H 2 = {1}, since B 2 = σ 1 |-∼ = Z.
Now, every commutator in B n has exponent sum zero. Conversely, every generator of H n is a product of commutators. Hence, we have H n = K n , and exp is the abelianization homomorphism.

Each K n fits into a split exact sequence:

1 → K n → B n → Z → 0,
and there are "natural" inclusions B n ⊂ B n+1 and K n ⊂ K n+1 .

Remark 1. We have the following consequences of relations in K n :

(1) z m+1 = x -1 j z m x j , hence z m = x -m j z 0 x m j ; for j ≥ 4. where z 0 = σ 2 σ -1 1 .

(2) The z m 's are conjugate in B n for n ≥ 3 (by σ 1 ) and in K n for n ≥ 5.

(3) The restriction of conjugation by σ 1 in B n to K n induces an action of Z on K n . This presentation of K n is said to be Z-dynamical.

The representation shift

This work is essentially experimental. It aims to describe the set of representations of K n into finite group Σ. We start with n = 3 and describe Hom (K 3 , Σ) by means of a graph Γ that we will construct in a step by step fashion [START_REF] Silver | Generalized n-colorings of links[END_REF]. A representation ρ : K 3 → Σ is a function ρ from the set of generators z m to Σ such that for each m ∈ Z, the relation:

ρ (z m ) ρ (z m+2 ) = ρ (z m+1 )
holds in Σ. Any such function can be constructed as follows, beginning with step 0 and proceeding to steps

±1, ±2, • • • • • • (step -1) Choose ρ (z -1 ) if possible such that ρ (z -1 ) ρ (z 1 ) = ρ (z 0 ). (step 0) Choose values ρ (z 0 ) and ρ (z 1 ). (step 1) Choose ρ (z 2 ) if possible such that ρ (z 0 ) ρ (z 2 ) = ρ (z 1 ). (step 2) Choose ρ (z 3 ) if possible such that ρ (z 1 ) ρ (z 3 ) = ρ (z 2 ). • • •
This process leads to a bi-infinite graph whose vertices are the maps ρ : {z 0 , z 1 } → Σ, each of which can be regarded as an ordered pair (ρ (z 0 ) , ρ (z 1 )). There is a directed edge from ρ to ρ ′ if and only if ρ (z 1 ) = ρ ′ (z 0 ) and ρ (z 0 ) ρ ′ (z 1 ) = ρ (z 1 ). In such a case, we can extend ρ : {z 0 , z 1 } → Σ by defining ρ (z 2 ) to be equal to ρ ′ (z 1 ). Now if there is an edge from ρ ′ to ρ", we can likewise extend ρ by defining ρ (z 3 ) to be ρ" (z 1 ). We implement this process by starting with an ordered pair (a 0 , a 1 ) of elements of Σ, and computing at each step a new ordered pair from the old one, so that every edge in the graph looks like:

(a m , a m+1 ) → (a m+1 , a m+2 ) , with a m+2 = a -1 m a m+1 . In our case, since the group Σ is finite, the process must end, and the graph Γ we obtain consists necessarily of disjoint cycles. This gives an algorithm for finding Hom(K 3 , Σ). Observe that Hom(K 3 , Σ) is endowed with a shift map

σ : ρ -→ σ (ρ) defined by σ (ρ) : x -→ ρ σ 1 xσ -1 1 . If we regard ρ as a bi-infinite path in the graph Γ, then σ correspond to the shift map (a m , a m+1 ) -→ (a m+1 , a m+2 ), since z m+1 = σ 1 z m σ -1
1 . Any cycle in the graph Γ with length p corresponds to p representations having least period p. These are the iterates of some representation ρ ∈ Hom(K 3 , Σ) satisfying ρ (z m ) = a m and σ p (ρ) = ρ, since a m+p = a m .

Example 2. A cycle of length 2 has the form a, a 2 ⇆ a 2 , a , with a 3 = 1.

Remark 2. Since K 3 is a free group of rank 2, Hom (K 3 , Σ) has a simple description; namely, there is a one to one correspondence between Hom (K 3 , Σ) and Σ 2 . The interest of our approach, beside the dynamical structure, is that it allows to go further and describe Hom (K n , Σ), for n ≥ 3. As a consequence of the dynamical approach, we get a partition of Hom (K 3 , Σ) into orbits, hence the identity

|Σ| 2 = 1 + p≥2 p.n p ,
where n p is the number of orbits of (least) period p.

Proposition 1. If a cycle has length p, then the identity a 0 a 1 ...a p-1 = 1 holds.

In order to minimize calculations, we extract some foreseeable behaviour for various choices of the ordered pair (a 0 , a 1 ) in the previous algorithm.

First, the dynamics of ordered pairs (a 0 , a 1 ) such that a 0 = 1 or a 1 = 1 or a 0 = a 1 is entirely known. To be precise, we get a cycle of length 6 unless a = a -1 , in which case it is of length 3 (or 1 if and only if a = 1).

(

1, a) → (a, a) → (a, 1) → 1, a -1 → a -1 , a -1 → a -1 , 1 → (1, a) .
This sort of dynamics will be generalized later to representations into abelian groups. Second, when we proceed to a new step, we do not need to take a pair we have already got in a previous cycle, since we would get indeed the same cycle. The following dichotomy will prove useful in the sequel: Definition 1. If a vertex of a cycle in Γ has equal components, then the cycle is said to be of type I. Otherwise, it is of type II.

Note that a cycle is determined by any of its vertices. Furthermore, the type I cycles are determined by elements of Σ. Now let us proceed to compute Hom(K 4 , Σ). Since K 3 ⊂ K 4 , every representation ρ ∈ Hom(K 4 , Σ) restricts to a representation ρ | K3 ∈ Hom(K 3 , Σ), the latter being described by a cycle. All we have to do is then to check which representation in Hom(K 3 , Σ) does extend to K 4 . To this end, observe that K 4 is gotten from K 3 by adjunction of a generator x 3 subject to the relations

z m x 3 z m+2 = x 3 z m+1 x 3 ; m ∈ Z.
Hence we may proceed as follows. Take a cycle in Hom(K 3 , Σ) (by abuse of language, i.e. identify each representation with its orbit, since a representation in Hom(K 3 , Σ) extends to K 4 if and only if every element in its orbit does), and choose if possible a value b 3 ∈ Σ for ρ (x 3 ). This value must satisfy the relations

a m b 3 a m+2 = b 3 a m+1 b 3 ; for m = 0, • • •, p -1,
where p is the cycle's length and the indexation is modp. Observe that the choice b 3 = 1 is convenient, so all cycles extend to K 4 . However, this is the only possibility for type I cycles to extend, for if b 3 commute with some a m , then b 3 = 1. Before giving the general procedure, let us proceed one further step to show that all type I cycles will vanish for n ≥ 5. Take a cycle in Hom(K 3 , Σ), along with a convenient value b 3 of ρ (x 3 ). We look for an element b 4 ∈ Σ satisfying :

a m b 4 = b 4 a m+1 , m = 0, • • •, p -1;
a m b n-1 = b n-1 a m+1, m = 0, • • •, p -1; b n-1 b i = b i b n-1 i = 3, • • •, n -3; b n-1 b n-2 b n-1 = b n-2 b n-1 b n-2
The element b n-1 has to be non trivial, otherwise the representation is trivial.

Using the various relations between the a m 's and the b i 's, we get the following ones :

Proposition 3. Let ρ ∈ Hom(K n , Σ), n ≥ 5 be encoded by a type II cycle (a m ) p-1 m=0
of length p, along with elements b 3 , ..., b n-1 ∈ Σ as previously. Then we have the following relations :

(1) The b i 's are non trivial and conjugate for i = 3, ..., n -1 and

[b p i , a m ] = 1, for m = 0, ..., p -1; i = 4, ..., n -1. (2) [b i , b j ] = 1; |i -j| ≥ 2; [b i , b j ] = 1; |i -j| = 1. .
(3) b i = b j , for i, j = 3, ..., n -1 and i = j, except for the possibility b 3 = b 5 , in which case ρ doesn't extend to Hom(K 7 , Σ). As a consequence of the first relation, p divides the order of b i , i = 4, ..., n -1; hence that of Σ.

The abelian case

Starting with n = 3, we see that the relation betwen the a m 's, written additively, becomes :

a m+2 = a m+1a m . Implementing our algorithm gives a matix A :

(a, b) A -→ (b, b -a) ,
with A 3 = -I. All cycles have length dividing 6. More precisely, the length may be 1 (a = b = 0) or 2 (a = -b, with 3a = 0) or 3 (2a = 2b = 0) or 6 (otherwise). Moving to n = 4, we find that all cycles extend to K 4 with b 3 = 1 (only). No non trivial cycle extends to K 5 , that is Hom(K n , Σ) = 0, for Σ abelian and n ≥ 5. This latter fact can also be seen from :

K n [K n , K n ]
= 1; n ≥ 5.

Extension to the braid group

In this section, we address the question of extending representations

ρ ∈ Hom(K n , Σ)
to representations ρ ∈ Hom(B n , Σ). Applying [SiWi1 (3.5)], the extension is possible if and only if there is an element

c ∈ Σ such that a m c = ca m+1, m = 0, • • •, p -1; cb i = b i c i = 3, • • •, n -1;
Observe that such an element c must satisfy c = 1, unless ρ is trivial; and [c p , a m ] = 1, for m = 0, ..., p-1. In particular, p divides the order of c. Hence, if p ∤ |Σ|, then ρ doesn't extend to B n . Observe also that a necessary condition for a representation ρ ∈ Hom(K n , Σ) to extend to ρ ∈ Hom(B n , Σ) is that ρ ∈ Hom(K n , [Σ, Σ]). A sufficient condition is that ρ be the restriction of some representation ρ ∈ Hom(K n+2 , Σ) for if this is the case, the choice c = b n+1 will do. In this case, since ρ maps K n into [Σ, Σ]; it also maps K n+2 into [Σ, Σ], for the b i 's are conjugate (if n ≥ 4) and [Σ, Σ] is normal in Σ. As a result, we get the following Proposition 4. for n ≥ 6, Hom(K n , Σ) = Hom(K n , Σ (r) ), where r ≥ 0 is the smallest integer such that Σ (r+1) = Σ (r) .

As a consequence, we get the fact that n ≥ 6, Hom(K n , Σ) is trivial for any solvable group Σ. This generalizes the abelian case. In this case, every ρ ∈ Hom(B n , Σ) has a cyclic image generated by ρ (σ 1 ) = ... = ρ (σ 1 ), i.e. |Hom(B n , Σ)| = |Σ|.

Actually we can enhance our algorithm to one which gives for fixed n ≥ 5 the sets Hom(K n , Σ) and Hom(B n , Σ).

Step one: find all cycles of both types. This gives Hom(K 3 , Σ).

Step two: For the trivial cycle, take any c ∈ Σ to be arbitrary. For a type II cycle C (with length p dividing |Σ|), find c = 1 such that a m c = ca m+1 , for m = 0, • • •, p -1. This gives Hom(B 3 , Σ).

Step three: For a cycle of any type , take b 3 = 1.

3 , •••, b i-1 . if [C, b 3 , b 4 , • • •, b i-2 , c] occurs in Hom(B i-1 , Σ) with some convenient c then: if cb i-1 = b i-1 c , then the representation [C, b 3 , b 4 , • • •, b i-1 ] moves up to a rep- resentation [C, b 3 , b 4 , • • •, b i-1 , c] in Hom(B i , Σ); if cb i-1 c = b i-1 cb i-1 , then the representation [C, b 3 , b 4 , • • •, b i-1 ] moves up to a representation [C, b 3 , b 4 , • • •, b i-1 , b i ] in Hom(K i+1 , Σ) by taking b i = c.

Permutation representations

Our goal in this section is to study representations of K n into the symmetric group S r . Note that there is a natural homomorphism:

π : B n → S n ,
for all n ≥ 2, given by σ i -→ (ii + 1). This restricts to K n to give a non trivial homomorphism:

x i -→ (12) (ii + 1) i = 3, • • •, n -1 z m -→ (132) , (123) ,
m is even m is odd

We start, as usual, with n = 3, and describe Hom(K 3 , S r ). Note that it contains π | K3 , for r ≥ 3. Recall that a non trivial element a ∈ S r has order two if and only if it is a product of disjoint transpositions. Let n r be the number of such elements. This gives us a means to compute the number of type I cycles to be 1 2 (1 + n r + r!) and of representations coming from them to be 3r! -2.

Since S 2 = {1, (12)}, Hom (K 3 , S 2 ) consists only of the following type I cycle:

(1, (12)) → (( 12) , (12)) → ((12) , 1) → (1, ( 12)) , along with the trivial representation. So

Claim 1. |Hom (K 3 , S 2 )| = 4.
As for Hom (K 3 , S 3 ), there are three type I cycles of length 3 corresponding to transpositions and one type I cycle of length 6 corresponding to the 3-cycle (123) (and its inverse). Looking at type II cycles, we find two cycles of length 9 corresponding to the pairs (( 23), ( 12)) and (( 23) , (123)) and one cycle of length 2 corresponding to the pair (( 123) , (132)). This last one is exactly the orbit (under the shift map σ) of π | K3 . All by all, we have Claim 2. |Hom (K 3 , S 3 )| = 36.

In the last section, we present among other things, the results of computer calculations of type II cycles in the graph of Hom (K 3 , S 4 ) using Maple. Moving to n = 4, we find that all (type I) cycles in Hom (K 3 , S 2 ) extend to K 4 with b 3 = 1. So

Claim 3. |Hom (K 4 , S 2 )| = 4.
No cycle in Hom(K 3 , S 3 ) extends to K 4 with non trivial b 3 :

Claim 4. |Hom (K 4 , S 3 )| = |Hom (K 3 , S 3 )| = 36.
Out of 71 (type II) cycles in Hom(K 3 , S 4 ) only ten do extend to K 4 , each with three possibilities for b 3 (the same for all; see the last section). So

Claim 5. |Hom (K 4 , S 4 )| = |Hom (K 3 , S 4 )| + 30.
For n = 5, we find that no type I cycle and no type II cycle with b 3 = 1 extends to K 5 , and that Claim 6. |Hom (K 5 , S 2 )| = |Hom (K 5 , S 3 )| = 1.

As for type II cycles with b 3 = 1, none of the thirty cycles extends to K 5 :

Claim 7. |Hom (K 5 , S 4 )| = 1.
We also find :

Claim 8. |Hom (K 6 , S 5 )| = |Hom (K 7 , S 6 )| = 1.
Experimental results recover the well known fact that that the process given by Algorithm 1 will stop at step n = r. That is: Proposition 5. Hom(K n , S r ) is trivial for r ≥ 4 and n ≥ r + 1.

Proof. see Lin

It is obvious that a cycle (of any type) can not extend to K n if it doesn't extend to K n-1 , so Proposition 5 asserts exactly that Hom(K r+1 , S r ) is trivial. Recall that for n ≤ r, Hom(K n , S r ) is not trivial since it contains the homomorphism π | Kn : K n → S n . Proposition 6. for n ≥ 6, Hom(K n , S r ) = Hom(K n , A r ).

Proof. Apply Proposition 4 to Σ = S r .

Note that according to Proposition 5, for n ≥ r + 1 , every representation ρ : B n → S r factorizes through the abelianized group (B n ) ab , and has a cyclic image. Hence, there are r! possible choices for ρ.

Consequences

Regarding the correspondence between subgroups of finite index of a group K and its representations into symmetric groups, we investigate the subgroups of index r of K n for low degrees r. The general principle is to compute the number of transitive representatations of K into S r to deduce the number of subgroups of K with index exactly r. We start with K 3 as usual. Note that since K 3 is freely generated by z 0 and z -1 , it maps onto any symmetric group, and hence, has subgroups of every index. Now, if a representation in Hom(K 3 , S r ) is transitive, then so are the representations in its orbit. Consider a type I cycle in Hom(K 3 , S r ). Then the representations it defines are transitive if and only if the defining element a is (with respect to the action of S r on {1, • • •, r}). This exactly means that a is an r-cycle. If r > 2 then a 2 = 1 and the cycle has length 6. Claim 9. The number of transitive representations ρ ∈ Hom(K 3 , S r ), r ≥ 2 coming from type I cycles is 3 (r -1)!.

For r = 2, there are only type I cycles and there is only one 2-cycle, which has length 3; Hence, The number of transitive representations ρ ∈ Hom(K 3 , S 2 ) is 3. The kernels of these representations give rise to subgroups of K 3 with index 2.

Claim 10. There are three subgroups of K 3 with index 2. Now we compute the number of subgroups of K 3 with index 3. Among all representations we have seen in example 2, there are six transitive representations coming from the only type I cycle and all representations coming from type II cycles are transitive. Hence: Claim 11. The number of transitive representations in Hom (K 3 , S 3 ) is 26, consequently there are thirteen subgroups of K 3 with index 3.

We can proceed in this way for every degree r. To compute the number of transitive representations of K 3 into S r , we need only consider those coming from type II cycles, since we already know the number of those coming from type I cycles. This can be done using a computer algebra system, by taking any cycle C = (a 0 , •••, a p-1 ) and checking if the subgroup a 0 , •••, a p-1 of S r acts transitively on {1, • • •, r}. If so, this gives rise to p transitive representations in Hom (K 3 , S 3 ). Then we divide the total number by (r -1)! to find the number of subgroups of K 3 of index r. Now let us consider Hom (K 4 , S r ). For r = 2 we have, as previously:

Claim 12. There are three subgroups of K 4 with index 2.

As for transitive representations in Hom (K 4 , S 3 ), since all cycles in Hom (K 3 , S 3 ) extend to K 4 with only b 3 = 1, we have: Claim 13. There are twenty six transitive representations in Hom (K 4 , S 3 ), hence thirteen subgroups of K 3 with index 3.

For r ≥ 4, we have 3 (r -1)! transitive representations coming from type I cycles, and we must check which representation coming from a type II cycle is transitive. For a cycle C = (a 0 , • • •, a p-1 ) such that a 0 , • • •, a p-1 failed to be transitive, we check if a 0 , • • •, a p-1 , b 3 (with b 3 non trivial) is transitive. Indeed, if a 0 , • • •, a p-1 is transitive, then so is a 0 , • • •, a p-1 , b 3 . Finally, we divide the total number by (r -1)! to find the number of subgroups of K 4 of index r. Now, we consider n ≥ 5, where we get rid of type I cycles. Suppose we have found the transitive representations in Hom (K n-1 , S r ). We then take, for fixed r, We may enhance algorithm 1 by checking, each time we get a new type II cycle, if it is transitive, and if not, we re-check at each time the cycle extends from K i to K i+1 , i = 3, • • •, n -1, after having augmented it with b i . Dividing by (r -1)! the number of transitive representations in Hom (K n , S r ) we find the number of subgroups of K n with index r. As a consequence of Proposition 5, we get the following: Proposition 7. For n ≥ 5 and 2 ≤ r ≤ n -1, there are no subgroups of K n with index r. Moreover, every nontrivial representation ρ of K n into S n is transitive.

Remark 3. We can likewise investigate the number of subgroups of B n with a given index r by looking at transitive representations of B n into S r . Namely, according to Proposition 5, there is exactly one subgroup of index r in B n , for 1 ≤ r ≤ n -1. Moreover, if ρ : B n → S n is a representation, then ρ | Kn is either trivial or transitive, according to Proposition 7. In the first case, ρ has a cyclic image and we know when it is transitive. In the second case, ρ is transitive.

Proposition 2 .

 2 Let ρ ∈ Hom (K 4 , Σ) be encoded by a cycle (a m ) m=0,...,p-1 and an element b 3 ∈ Σ. Then b p 3 = 1.As a consequence, the order of b 3 divides p; hence, if gcd (p, |Σ|) = 1, then b 3 = 1.

  and b 3 b 4 b 3 = b 4 b 3 b 4 Hence, if b 3 b 4 = b 4 b 3 , then b 3 = b 4 . Using a m b 3 a m+2 = b 3 a m+1 b 3 , and a m b 4 = b 4 a m+1 , we get b 3 = b 4 = 1, and a m = a m+1 , ∀m = 0, • • •, p -1, so that the representation is trivial. So, except for the trivial cycle, only type II cycles with b 3 = 1 possibly extend to K 5 , with b 4 not commuting with b 3 , in particular, b 4 = 1. Note that b 3 and b 4 are conjugate. Algorithm 1. The general procedure for Hom(K n , Σ), n ≥ 5 is to consider only type II cycles along with convenient non trivial values b 3 , •••, b n-2 , which correspond to representations in Hom(K n-1 , Σ) and find a non trivial element b n-1 ∈ Σ such that the following relations are satisfied:

  For a type II cycle C (with length p such that gcd (p, |Σ|) = 1), find b 3 = 1 such that a m b 3 a m+2 = b 3 a m+1 b 3 , for m = 0, • • •, p -1. This gives Hom(K 4 , Σ). Step four: Beside the trivial cycle, take a type II cycle C along with a convenient b 3 (with length p dividing |Σ|). If this cycle occurs in Hom(B 3 , Σ) with some convenient c then : if cb 3 = b 3 c (which need not be checked if b 3 = 1), then the representation [C, b 3 ] moves up to a representation [C, b 3 , c] in Hom(B 4 , Σ); if cb 3 c = b 3 cb 3 (which is impossible if b 3 = 1), then the representation [C, b 3 ] moves up to a representation [C, b 3 , b 4 ] in Hom(K 5 , Σ) by taking b 4 = c. • • • Step i: take a representation ρ in Hom(K i , Σ), encoded by a type II cycle C along with convenient values b

  a type II cycle C = (a 0 , • • •, a p-1 ) along with values b 3 , • • •, b n-1 , such that a 0 , • • •, a p-1 , b 3 , • • •, b n-2 failed to be transitive and check if a 0 , • • •, a p-1 , b 3 , • • •, b n-1 is transitive.

Acknowledgement 1. I am grateful to Susan G. Williams for many helpful email discussions. I also wish to thank the students M. Menouer and Z. Ziadi for their help in computer search.


Dmitry Burlyaev

Pascal Fradet

Alain Girault

A static analysis for the minimization of voters in fault-tolerant circuits

Keywords: digital circuits, static analysis, fault-tolerance, triple modular redundancy, optimizations circuits numériques, analyse statique, tolérance aux fautes, redondance modulaire triple, optimisations

We present a formal approach to minimize the number of voters in triple-modular redundant (TMR) sequential circuits. Our technique actually works on a single copy of the TMR circuit and considers a large class of fault models of the form at most 1 Single-Event Upset (SEU) or Single-Event Transient (SET) every k clock cycles. Verication-based voter minimization guarantees that the resulting TMR circuit (i) is fault tolerant to the soft-errors dened by the fault model and (ii) is functionally equivalent to the initial TMR circuit. Our approach operates at the logic level and takes into account the input and output interface specications of the circuit. Its implementation makes use of graph traversal algorithms, xed-point iterations, and binary decision diagrams (BDD). Experimental results on the ITC'99 benchmark suite indicate that our method signicantly decreases the number of inserted voters, yielding a hardware reduction of up to 55% and a clock frequency increase of up to 35% compared to full TMR.

Introduction

Circuit tolerance towards soft (non-destructive, non-permanent) errors is an important research topic. As technology shrinks, the risk of system failures due to soft errors increases, which is especially dangerous in safety-critical industries (e.g., space, transport, nuclear, etc.). Natural radiation, such as neutrons of cosmic rays and alpha particles of packing or solder materials, is a common source of soft errors [START_REF] Shivakumar | Modeling the eect of technology trends on the soft error rate of combinational logic[END_REF][START_REF]Neutron-induced single event upset SEU[END_REF][START_REF] Ziegler | IBM experiments in soft fails in computer electronics (1978-1994)[END_REF][START_REF] Dodd | Neutron-induced soft errors, latchup, and comparison of SER test methods for SRAM technologies[END_REF]. There are two main types of soft errors: Single-Event Upsets (SEUs) (i.e., bit-ips in Flip-Flops (FFs)) and Single-Event Transients (SETs) (i.e. glitches propagating in the combinational circuit). Since an SET may potentially lead to several bit-ips, SETs are more general than SEUs.

Triple-Modular Redundancy (TMR) proposed by von Neumann [START_REF] Neumann | Probabilistic logic and the synthesis of reliable organisms from unreliable components[END_REF] remains the most popular fault tolerance technique in Field-Programmable Gate Arrays (FPGAs) to mask both types of soft-errors. Yet, manual introduction of TMR [START_REF] Habinc | Functional triple modular redundancy FTMR[END_REF] into a circuit design is often a tedious and error-prone process. Hence, several CAD tools automatically implement TMR for fault tolerant FPGA designs [START_REF] Bridgford | Single-event upset mitigation selection guide[END_REF][START_REF] Corporation | Xilinx TMRTool[END_REF][START_REF] Pratt | Improving FPGA design robustness with partial TMR[END_REF][START_REF] Sutton | Creating highly reliable FPGA designs[END_REF][START_REF] Do | New tool for FPGA designers mitigates soft errors within synthesis[END_REF].

In a triplicated sequential circuit, adding voters at the primary outputs is not sucient in general. Indeed, an error may remain in a memory cell long enough until another error corrupts a dierent redundant copy of the circuit. In that case, the nal vote may produce an incorrect output. Voter insertion after each memory cell is sucient to prevent errors from remaining in cells. However, it greatly increases both hardware overhead and the critical path, which directly inuences the circuit performance. Thus, the overall TMR throughpout is degrading whereas it should be the main advantage of TMR over time-redundant fault-tolerance techniques.

From the functional point of view, introducing a voter per cell is excessive in most cases.

Intuitively, this is because some voters are useless, either because faults at this stage will be captured by another voter later in the circuit, or because some faults are naturally masked by the logic. But, to the best of our knowledge, there is no tool dedicated to voter minimization in TMR that guarantees fault-tolerance according to a user-dened fault model. The main existing research trends in TMR have been providing probabilistic solutions and not absolute ones (see Section 9).

Our objective is to propose an automatic, optimized, and certied transformation process for TMR on digital circuits. In this paper, we focus on the optimization aspect of the automatic transformation: it should insert as few voters as possible, while guaranteeing to mask all errors of the considered fault-model.

We consider circuits described at the gate level (i.e., netlists of AND, OR, NOT gates plus FFs also called memory cells). This level has two main advantages: gate level netlists can be described by an elementary language, which simplies correctness proofs; it is easier to prevent synthesis tools from optimizing (undoing) our transformation at this late design stage.

Since the main contributors to Soft-Error Rate (SER) at frequencies below 1 GHz are the FFs [START_REF] Heijmen | Soft-error vulnerability of sub-100-nm ip-ops[END_REF],

we focus rst on errors caused by SEUs (i.e., bit-ips in FFs). We consider fault models of the form at most one bit-ip within K cycles denoted by SEU (1, K). However, SETs in high-speed Integrated Circuits (ICs) have become a growing concern [START_REF] Hass | Single event transients in deep submicron CMOS[END_REF][START_REF] Buchner | Single-event transients in fast electronic circuits[END_REF][START_REF] Nguyen | A systematic approach to SER estimation and solutions[END_REF]. In response, we expend our approach to SET fault-model in the form at most one transient fault within K clock cycles denoted by SET (1, K).

The proposed voter-minimization methodology is based on a static analysis that checks whether an error in a single copy of the TMR circuit may remain after K cycles. If not, protecting the primary outputs with voters is sucient to mask the error. If, for instance, the circuit is a pipeline without feedback loops, then any bit-ip will propagate to the outputs and will thus disappear before K cycles, where K is the length of the longest path. But if the state of the circuit is still erroneous after K cycles (in the form of an incorrect value stored in one of its memory cells), then there is a potential error accumulation since, according to the SEU /SET (1, K) models, another soft-error may occur in another copy of the circuit. It may lead to two incorrect redundant modules of the TMR circuit and the loss of its fault-tolerance properties. In this case, additional voters are needed to prevent an error accumulation and mask all errors circulating inside one redundant module before the next soft-error may occur.

Our static analysis consists of four steps. The rst step, described in Section 2, is purely syntactic and nds all loops in the circuit. Error accumulation can be prevented by keeping enough voters to cut all loops.

In many cases, a digital circuit resets (or overwrites) some memory cells, which may mask errors. Detecting such cases allows further useless voters to be removed. This second step is performed by a semantic analysis (Section 3) taking into account the logic of the circuit.

Circuits are also often supposed to be used in a specic context. For instance, a circuit specication may assume that a start signal occurs every x cycles and outputs are only read y cycles after each start. When such assumptions exist, taking them into account makes the semantic analysis more eective. Section 4 and Section 5 explain how to integrate such input and output specications respectively.

Our analysis has been implemented based on graph algorithms and xed point iterations using Binary Decision Diagrams (BDDs). We have tested several safe approximations and trade-os between cost and precision. The implementation and experiments are presented in Section 7.

Related work on TMR and voter insertion strategies are reviewed in Section 9. We summarize our contributions and sketch a few extensions in Section 10.

This article extends and revises the work presented in DATE'14 [START_REF] Burlyaev | Verication-guided voter minimization in triplemodular redundant circuits[END_REF]. Section 6, presenting the extension of the approach to SET, is new. Sections 3 and 7 present and assess respectively a new abstract domain; explanations and examples have been added throughout.

Syntactic Analysis

We consider triplicated circuits with voters but we actually work on a single copy of the circuits.

The eect of insertion or removal of voters can be represented and analyzed on a single copy of the TMR circuit. We model a sequential circuit C as a directed graph G C where each vertex represents a FF (memory cell or latch) and an edge x → y exists whenever there is at least one combinational path between the two FFs x and y in C. An error in a cell x may propagate, in the next clock cycle, to all cells connected to x by an edge in this graph. Note that this is an over-approximation since the error may actually be masked by some logical operation.

Under the fault model SEU (1, K), error accumulation is the situation where an error remains in the circuit K clock cycles after the SEU that caused it. Any circuit C without feedback loop will return, after an SEU, to a correct state before K clock cycles, provided that K is larger than the maximal length of the paths in G C . In environments with high levels of ionizing radiations (e.g., space, particle accelerators), K is bigger than 10 10 [10]. For comparison, Soft-Error Rate (SER) can be as small as 10 -10 bit-upset/day for Virtex FPGAs in terrestrial conditions [START_REF] Brinkley | SEU mitigation design techniques for the XQR4000XL[END_REF]. So, even if our approach can deal with any K, we can assume that K is larger than the max length of all paths in G C . It follows that error accumulation can only be caused by cycles in G C , which must therefore be cut by removing vertices. Removing a vertex in G C amounts to protecting the corresponding memory cells with a voter in the triplicated circuit.

The best solution to cut all cycles in G C is to nd the Minimum Vertex Feedback Set (MVFS), Inria i.e., the smallest set of vertices whose removal leaves G C without cycles. This standard graph problem is NP-hard [START_REF] Karp | Reducibility among combinatorial problems[END_REF]. While there exist good polynomial time approximations [START_REF] Even | Approximating minimum feedback sets and multi-cuts in directed graphs[END_REF], the exact algorithm was ecient enough to be used in all our experiments with relatively small circuits (< 200 FFs ).

Having a voter after each cell belonging to the MVFS prevents error accumulation. This simple graph-based analysis is very eective with some classes of circuits. In particular, it is sucient to remove all internal voters in pipelined architectures such as logarithm units and oating-point multipliers (see Table 1).

However, this approach is not eective for many circuits due to the extensive use of loops in circuit synthesis from Mealy machine representation. In such circuits, most cells are in self-loops (e.g., D-type ip-ops with Enable input). This entails many voters if the syntactic analysis is used alone. However, if the circuit functionality is taken into account, we can discover that such memory cells may not lead to erroneous outputs. Detecting such cases requires to analyze the logic (semantics) of the circuit. We address this issue in the following section.

Semantic Analysis

The semantic analysis rst computes the Reachable State Set (RSS) of the circuit with a voter inserted after each memory cell in the MVFS. Then, for each cell m ∈ MVFS, it checks whether its voter is necessary: (i) First, the voter is removed and all possible errors (modeled by the chosen fault-model in each state of RSS) are considered; (ii) If such an error leads to error accumulation, then the voter is needed and kept.

3.1

The precise logic domain D 1

Correct and erroneous values are represented by the four-value logic domain D 1 :

D 1 = {0, 1, 0, 1}
where 0 and 1 represent erroneous 0 and 1, respectively. The truth tables of standard operations in this four-value logic are given in Table 2. Note that AND and OR gates can mask errors:

x ∨ 1 = 1, x ∧ 0 = 0 , 0 ∧ 1 = 0, 1 ∨ 0 = 1. The err function models bit-ips: i.e., err(0)=1

and err(1)=0. The vot function models the eect of a voter on a single copy of the circuit and corrects an error: i.e., vot(1)=0 and vot(0)=1. Finally, for any x ∈ {0, 1}, vot(err(x))=x.

0 1 0 0 1 1 1 1 1 1 1 1 1 1 0 1 0 0 0 0 0 1 0 1 0 0 0 0 NOT err vot 0 1 0 1 0 1 1 𝟏 𝟎 1 0 𝟏 1 1 𝟎 0 0 𝟏 𝟎 1 0 𝟏 1 1 𝟎 0 0 1 0 1 𝟏 0 0 0 𝟎 1

OR AND

Semantic analysis with D 1

A sequential synchronous circuit with M memory cells and I primary inputs is formalized as a discrete-time transition system with the transition relation δ :

{0, 1} M × {0, 1} I -→ {0, 1} M .
We abuse the notation and use M (resp. I) to denote both the number and the set of memory cells (resp. inputs) of the circuit. The state of a circuit is the values of its cells and the initial state s 0 is obtained after the circuit reset. ∆(S) denotes the function returning the set of states obtained from the set S after one clock cycle. Formally ∆(S) = {s | ∃i. ∃s ∈ S. δ(s, i) = s } ∆ applies the transition function δ to all states of its argument set and all possible inputs. The set of reachable states RSS is dened by the following iteration:

S 0 = {s 0 } S i+1 = S i ∪ ∆(S i ) (1)
Starting from the initial state, we compute the set of reachable states by accumulating states obtained by applying iteratively ∆. The set of possible states being nite, the iteration reaches a xed point equal to the RSS and denoted

1 by {s 0 } * ∆ .
The second phase is to check whether the suppression of voters may lead to an error accumulation under the chosen fault-model. Let δ V be the transition relation of a circuit equipped with a voter after each cell in a given set V , and let ∆ V be its extension to sets. δ V is dened as:

δ V ((m 1 , . . . , m M ), i) = δ((m 1 , . . . , m M ), i) where ∀ 1 ≤ j ≤ M, m j = vot(m j ) if m j ∈ V m j
otherwise This checking process is described by Algorithm 1:

We start with the circuit equipped with a voter after each cell in the MVFS (line 1). For each such cell m, we check whether its voter suppression entails error accumulation. Bit-ips are V := V \{m}; 5:

S := ∆ K V ( mi∈M RSS [m i ← err(m i )]); 6:
if ErrAcc(S) then 7:

V := V ∪ {m};

8: return V
introduced in all possible cells and states of RSS according to the fault-model (line 5):

mi∈M

RSS [m i ← err(m i )]
The transition function corresponding to the circuit with the current set of voters (V ) is applied K times (∆ K V ), where K is the number of clock cycles in the fault model (SEU (1, K)).

The resulting set of states shows error accumulation if there exists an erroneous cell in at least one state of this set, which we capture with the predicate ErrAcc in line 6. ErrAcc is dened as: ErrAcc(S) ⇔ ∃s ∈ S. ∃m ∈ s. m = 0 ∨ m = 1

If the set S does not show error accumulation, the voter is useless and can indeed be suppressed.

Otherwise the voter is re-introduced (line 7).

In practice, ∆ is applied a small number of times dictated by the circuit functionality and available analysis time. It is always safe to stop the iterative computation before reaching K;

the only drawback would be to infer an error accumulation when there is none. The number of ∆ applications can be also adjusted to the available analysis time. In our experiments, the analysis time limit was set to 20 minutes and K to 50. Furthermore, the iteration is stopped: if the current set of states is errorless, then there cannot be error accumulation (no error can reappear); or, if the erroneous current set is the same as the previous one, a xed point is reached and there is an error accumulation.

The order in which the cells in the MVFS are analyzed (line 2, in Algorithm 1) may inuence the number of removed voters. We use the following heuristic to chose the ordering of voter selection: starting from the MVFS of memory cells with voters, we sort it rst according to the number of successive memory cells that each cell has in the circuit netlist (the number of successors in G C ). Then, we consider primarily the removal of voters that lead to the corruption of the smallest number of cells in the next clock cycle. The voters whose removal may lead to a large number of corrupted cells are considered last. We found out that following this ordering, we are able to suppress more voters than with a random ordering or the ordering relying on the number of preceding memory cells in the netlist.

More Abstract Logic Domains

The aforementioned method is precise but costly since it considers all possible inputs. In general, keeping track of the relations between indeterminate inputs is not very useful. Fortunately, our technique can be used as it is with other, more abstract, logic domains. There are several domains that retain enough precision and allow larger circuits to be analyzed.

The 4-value logic domain D 2 decreases the state space explosion that occurs with D 1 :

D 2 = {0, 1, U, U}
The abstract value U represents a correct value (either 0 or 1) and U represents any (possibly erroneous) value (i.e., 0, 1, 0 or 1). A vector of n inputs is represented as a unique vector (U, . . . , U) with D 2 whereas 2 n vectors had to be considered with D 1 . The truth tables of standard operations in D 2 are given in Table 3. NOT err(x) vot(x)

0 1 U 0 1 0 U 1 U U U U 𝐔 U U U 0 1 U 𝐔 0 0 1 U 1 1 1 1 U U 1 U U 𝐔 U 1 U U 1 U 𝐔 0 1 U 0 0 0 0 0 1 0 1 U U U 0 U U 𝐔 U U 0 U U x

OR AND

In contrast with D 1 , a gate with two erroneous values cannot produce a correct one. Logical masking of errors can only occur with two operations: 0 ∧ U and 1 ∨ U. This is sucient to take into account the masking performed by explicit signals (e.g., resets).

Typical examples where the semantic analysis with D 2 is more eective are circuits that use D-type FFs with an enable input driven by a Finite State Machine (FSM) encoded in the circuit. The syntactic approach would keep a voter for each such cell (they are in self-loops).

The semantic analysis can detect that such cells are regularly overwritten by fresh inputs. For example, the resource arbiter b03 in Section 7 is such a circuit. After initialization, its nite state machine forces 12 cells (f u1-f u4, ru1-ru4, grant_o[3:0]) to be overwritten with fresh values every other cycle. The semantic analysis (using D 1 or D 2 ) is able to show that those cells, although in self loops, do not need to be protected by voters.

Another approximate logic domain is the 16-values logic domain D 3 , where a memory cell is encoded as a subset of its four possible values. It is dened as the powerset of D 1 :

D 3 = P({0, 1,

0, 1})

A value A in D 3 is the set of all possible values that its memory cell can take at this stage of the analysis. For example, a fully determinate value is represented by a singleton (e.g., {0} for a correct 0 or {0} for a bit-ipped 1), an unknown but uncorrupted value by the set {0, 1}, and a completely unknown value by the set {0, 1, 0, 1}.

Inria

The operators of D 3 are the power set extensions of the operators of D 1 .

A ∧ 3 B = {x | x = a ∧ 1 b, a ∈ A, b ∈ B} A ∨ 3 B = {x | x = a ∨ 1 b, a ∈ A, b ∈ B} ¬ 3 A = {x | x = ¬ 1 a, a ∈ A} err 3 (A) = {x | x = err 1 (a), a ∈ A} vot 3 (A) = {x | x = vot 1 (a), a ∈ A}
where ∧ 1 ∨ 1 , ¬ 1 , err 1 , and vot 1 denote the and, or, not, err, and vot operators of D 1 as dened in Table 2.

That domain is a trade-o in terms of precision between D 1 and D 2 . The main advantage of D 3 over D 1 is the prevention of state explosion, since a vector of n unknown and uncorrupted inputs is represented as a unique vector ({0, 1}, . . . , {0, 1}). Contrary to D 2 , D 3 remains able to represent logical masking such as {0} ∧ 3 {0, 1} = {0} or {1} ∨ 3 {1, 0} = {1}. Domain D 3 can be seen as retaining precise information about the possible values and corruptions but ignoring the relationships between dierent inputs.

Inputs Specication

Circuits are often designed to be used in a specic context where some input signals must occur at denite timings. Taking into account assumptions about the context may make the semantical analysis much more precise, in particular, when the logical masking of corrupted cells depends on specic inputs (e.g., a start control signal). Our approach is to translate these specications into an interface circuit feeding the original circuit with the specied inputs. The analysis of the previous section can be applied to the resulting combined circuit. As a consequence, error accumulation is checked with the method described in Section 3.2, but under the constraints specied by the interface. The only small adjustment needed in Algorithm 1 is to make sure that errors are introduced only in the cells of the original circuit and not in the cells of the interface circuit.

We use ω-regular expressions to specify circuit interfaces. An ω-regular expression species constraints using vectors of {0, 1, }, which replace primary inputs by 0, 1, or leave them unchanged ( being the wild card). Consider, for instance, a circuit with two primary inputs [i 1 , i 2 ], then the expression ([1, 0] + [0, 1]).[ , ] ω species that the circuit rst reads either i 1 = 0 and i 2 = 1, or i 1 = 0 and i 2 = 1, and then proceeds with no further constraints.

In general, specications need non-determinism to describe a partially specied or a nondeterministic context. Hence, the aforementioned ω-regular expression can also be seen as a Non-deterministic Büchi Automaton (NBA) that reads inputs and replaces them by 0, 1, or leaves them unchanged ( ).

For instance, the expression ([1, 0] + [0, 1]).[ , ] ω can be represented as the two-state NBA of Figure 1 (a): in the rst state, it reads inputs and returns either the outputs [START_REF]Open Source Hardware IPs: OpenCores project[END_REF]0]

or [0, 1]
(regardless of the inputs). Then, the automaton goes (and stays) in the second state where inputs are read and produced as outputs. The indices in 1 and 2 allow to identify the inputs according to their position.

To generate a circuit from an ω-regular expression, we rst convert the corresponding NBA into a deterministic automaton as follows. Each nondeterministic edge is made deterministic using new inputs (sometimes referred to as oracles). If a vertex has n nondeterministic outgoing edges, adding log 2 (n) new inputs is sucient. For example, the specication ([1, 0] + [0, 1]).[ , ] ω can be made deterministic by adding a single additional input i. The automaton (see Figure 1 (b)) now reads three inputs: if i is 0 (resp. 1) it produces [START_REF]Open Source Hardware IPs: OpenCores project[END_REF]0] (resp. [0, 1]). The resulting deterministic automaton is then translated into an interface circuit using standard logic synthesis RR n°9004 (a)

1 2 techniques [23, p.118]. If the original circuit has I inputs, the resulting interface circuit will have I + a (a new inputs to make it deterministic) inputs and I outputs. It is then plugged by connecting its outputs to the inputs of the circuit to be analyzed.

[ 1 , 2 ]/[1, 0] [ 1 , 2 ]/[0, 1] [ 1 , 2 ]/[ 1 , 2 ] (b) 1 2 [0, 1 , 2 ]/[1, 0] [1, 1 , 2 ]/[0, 1] [ 0 , 1 , 2 ]/[ 1 , 2 ]
A typical example where an input specication is useful is the circuit b08 of Section 7. Such a circuit has a start input signal and 8-bit data input. Its input interface specication can be expressed as the following ω-regular expression:

([1, , , , , , , , ].[0, , , , , , , , ] 17 ) ω (2)
A start signal is rst raised and the input data is read. For the next 17 cycles, data is processed and start is kept to 0. This process is repeated over and over. Since start is raised every 18 clock cycles, the internal data registers are rewritten periodically with new data, as they can keep erroneous data only until the next start signal. The circuit also has an internal FSM which can be corrupted but the periodic start ensures that it returns to its initial state every 18 cycles. Consequently, error accumulation is impossible for any K > 18, and no voters (except implicit voters at primary outputs) need to be inserted.

Outputs Specication

Consider another example, similar to the previous one, with 2 inputs, 1 output, and where some waiting can occur before raising the start signal. Formally, the input interface would be:

([0, ] * .[1, ].[0, ] 17 ) ω (3)
This interface does not guarantee that start will be raised before K clock cycles. Since the analysis must consider the case where start is not raised, it may detect error accumulation even though start would ensure logical masking. However, if it is known that the primary outputs are not read before some useful computation triggered by the start signal completes, a better analysis can be performed.

We specify the output interface by adding to each vector of the input interface a vector of {0, 1} indicating whether the corresponding outputs are read [START_REF]Open Source Hardware IPs: OpenCores project[END_REF] or not read (0). For instance, the output interface of the previous example, where the single bit output is read only after start Inria is raised, can be specied as

(([0, ] : [0]) * .([1, ] : [0]).([0, ] : [1]) 17 ) ω (4)
It states that the output is not read ([0]) until the start signal is raised. Then, the output is read ( [START_REF]Open Source Hardware IPs: OpenCores project[END_REF]) during 17 cycles.

The extended ω-regular expression is translated into an NBA as in Section 4, then made deterministic, and nally translated into a sequential circuit. The corresponding interface circuit will additionally produce 0 or 1 signals to lter the useless and needed outputs respectively. Each such signal is connected using an AND gate to the corresponding primary output of the original circuit. The nal conguration with the surrounding interface circuit is shown in Figure 2.

Input interface circuit oracles & free inputs

Interface circuit

Output interface circuit Original circuit The property to check must now be rened to allow error accumulation as long as no error propagates to the ltered primary outputs. Recall that when an error occurs, it is allowed to propagate to outputs (or nal voters) within the next K clock cycles since no additional softerror can occur during that time. If there is an error accumulation, the analysis must further ensure that no error can propagate to outputs after the K cycles i.e., when additional errors occur which could not be masked by nal voters. This is performed by lines 6-15 of Algorithm 2. If an error accumulation is detected in the reached state set S, K cycles after a fault occurrence (line 6), then we calculate all states S * ∆ V that can be reached after these K cycles (line 7). Then, we iteratively simulate the occurrences of additional errors (line 9-12) separated by at least K steps. E 0 (line 7) represents the circuit reachable state space with only one fault. E i represents the reachable state space after at most i + 1 errors separated from one another by at least K clock cycles. The global xpoint E i (line 13) represents the set of all possible states that can be reached after all possible sequence of errors allowed by the fault model. It can now be checked that none of these states leads to the propagation of an error to the (ltered) primary outputs (line 13).

Since this computation is done assuming that voters operate correctly, we must ensure that no error accumulate in a cell followed by a voter. Indeed, in that case, if a similar error occurs in a second copy of the circuit, the voter would fail to mask it. The function ErrP rop (line 13) detects if there is a reachable state where a memory cell with a voter or a primary output is corrupted and prevents the voter under consideration (m) to be removed. We assume that each primary output is represented by a new memory cell. Let out, vot and cor be predicates denoting whether a cell represents an output, a cell protected by a voter or is corrupted respectively, then ErrP rop is dened as:

ErrProp(E i ) ⇔ ∃s ∈ E i . ∃m ∈ s. (out(m) ∨ vot(m)) ∧ (cor (m))
These criteria are safe but sometimes too strict. Consider, for instance, a circuit with a sequence of two enabled ip-ops (i.e., with self loops) that produce signicant output only two cycles after the enable signal is set. Both cells may be protected by voters to break self loops and prevent error accumulation. However, no voter is necessary since error accumulation can occur only when no signicant output is produced. Indeed, when the enable signal is set, new input and intermediate results will overwrite the (possibly corrupted) cells and a correct output will be produced. If we rst try to remove the rst voter, our algorithm will detect that an error can remain in the rst cell after K steps. That cell will in turn corrupt the second one still protected by a voter. Hence, the condition ErrP rop will prevent removing the rst voter whereas starting with the second or removing both voters would have been possible. Therefore, a useful renement of Algorithm 2 is, whenever ErrP rop is true only because of error accumulation before some voters (and no error propagates to the output), to iterate and check whether all these voters can be removed. V := V \{m}; 5:

S := ∆ K V ( mi∈M RSS [m i ← err(m i )]); 6:
if ErrAcc(S) then i + +;

11:

E i := E i-1 ∪ (∆ K ( mi∈M E i-1 [m i ← err(m i )])) * ∆ V ; 12: until E i = E i-1 13:
if ErrProp(E i ) then 14:

V := V ∪ {m};

15: return V

Output interfaces are especially useful for circuits whose outputs are not read before some input signal is raised and some computation is completed. For instance, the shift/add multiplier (see Sec 7) waits for a start signal. During that time, errors may accumulate in internal registers and propagate to the outputs, which are not read. When start occurs, fresh input data is read and written to internal registers (which are thus reset). The outputs are read only after the multiplication is completed and a done signal is raised.

Note that output interfaces can model Transient Error Tolerance (TET) where all errors at outputs are not necessarily critical. For instance, if erroneous outputs are considered noncritical within a specied number of cycles, output interfaces may express it and allow further optimizations. In this case, the optimized TMR conguration is tuned to particular system requirements. Such quality-guided optimizations are investigated on MPEG decoding in [START_REF] Hayes | An analysis framework for transient-error tolerance[END_REF][START_REF] Polian | Low-cost hardening of image processing applications against soft errors[END_REF] to select gates whose hardening maximize fault-tolerance.

Inria 6 Extension to Single-Event Transients

In the previous sections, we considered single event upsets and the corresponding fault-models SEU (1, K), corresponding to at most one bit-ip every K cycles. Hereafter, we extend our approach to single event transients, in particular, the fault model SET (1, K) which can be read as at most one SET within K clock cycles.

An SET occurs when an energetic subatomic particle strikes a combinational logic element [START_REF] Hass | Single event transients in deep submicron CMOS[END_REF]. Such particle causes a transient voltage disturbance, which can propagate on wires and possibly be latched by several memory cells. Consequently, an SET can potentially lead to several bit-ips (i.e., several SEUs). In this section, we present the extension of our previous analysis to SET.

Precise modeling of SETs

As opposed to an SEU, the eect of an SET depends on the logical propagation (and possible logical masking) of the signal perturbation through the combinational part. Such signal perturbation or glitch is latched in a non-deterministic manner. From now on, a signal can take 3

values: a logical one, a logical zero, or a glitch written .

Signal := 0 | 1 | A glitch can
D t = {0, 1, 0, 1, 0 , 1 }
where 0 and 1 represent respectively a glitched 0 and 1. That is, 0 represents a glitch at one point of the circuit such that the value in the two other redundant copies is 0. A glitch on an incorrect signal with the value 0 (resp. 1) will be represented by the signal value 1 (resp. 0 ).

One example that illustrates the dierence between a glitch and a corrupted value is:

D 1 : 0 ∨ 1 1 = 1 D t : 0 ∨ t 1 = 1
While in the rst case, an or gate with corrupted but stable signals returns a correct value, in the second case, the glitch propagates.

While the precise domain D 1 requires the aforementioned extension to D t , the domains D 2 and D 3 can overapproximate such glitch behavior with no extension. In particular, a glitched signal, as well as any possibly wrong stable signal, takes the value U in D 2 . A glitched 1 (resp. 0) can be represented as {1, 0} (resp. {0, 1}) in D 3 .

A glitch propagated to a memory cell is non-deterministically latched as true or false. It follows that the precise glitch modelling in D t implies that any glitched signal 0 (resp. 1 ) is non-deterministically latched as a correct 0 or as an incorrect 1 (resp. as a correct 1 or as an incorrect 0). This non determinism may lead to a signicant state space growth in D 1 . The domains D 2 and D 3 avoid this inconvenience since glitched signals are expressed in the same logic as the latched values.

To take into consideration all possible eects of an SET, it is necessary to calculate the set of reachable states for all cases of SET injections. These cases include a fault injection either at the output of a logical gate/a memory cell or the mutually exclusive corruption of branches of a wire split. The union of the state spaces that can be reached in each of these corruption cases forms the reachable state set.

The precise SET modeling in D t imposes signicant computational overhead. Its two important bottlenecks are the need to consider all possible SET injection points and all possible non deterministic choices when a glitch is latched. Both points can been taken into account by a transition function that expresses a circuit state change during a clock cycle with an SET and returns a set of possibly corrupted states. In the next Section, we propose a safe approximation of the precise SET modeling in domains D 1 , D 2 , and D 3 .

Safe SET over-approximation

If a memory cell is connected by a combinational path to a component (wire or gate) where an SET occurs, this cell may be corrupted. We should nd all sets of cells that can be corrupted at the same clock cycle to nd the worst case. Each of these sets has a common combinational sub-circuit, in other words, a common combinational cone. The apex of such a cone is either the output of a memory cell or a primary input. A cone apex fully identies a cone and the memory cells belonging to this cone. In Figure 3, the cone with apex at c 1 includes both cells c 2 and c 3 . The cone with apex at p 1 also includes {c 1 , c 2 }. The cones with apexes at c 3 and c 2 contain {c 1 } and {c 2 } respectively.

As a result, the worst case scenario of any SET that happens inside a cone j is the union of all possible simultaneous corruptions of the memory cells ms(j) in this cone. The power set P (ms(j)) is the set of all possible memory cell corruption congurations.

As soon as all corruption congurations are found, a new error injection procedure can be dened and used in both Algorithms 1 and 2. In particular, instead of mutually exclusive bit-ips injection to a state space S, expressed for SEU as ( mi∈M S [m i ← err(m i )]), the corruption of the RSS by an SET is computed as the disjunction of possible simultaneous memory cells corruptions of the sets included in the cones after memory cells M or primary inputs I:

j∈(M ∪I)   p∈P (ms(j)) S mi∈p m i ← err(m i )  
where ms(j) is the subset of memory cells located in the cone with an apex at a memory cell or a primary input j.

Such corruption procedure is a safe over-approximation in the precise (D t ) and approximate (D 2 , D 3 ) domains. The complexity bottleneck of the approach is the power-set computation with a large number of memory cells in a single cone. However, in the case of the approximate logic domains D 2 and D 3 , we can consider only the worst case scenario: the simultaneous corruption Inria of all memory cells in a cone (without calculation of its powerset), computed as:

j∈(M ∪I) S   mi∈ms(j) m i ← err(m i )  
It may happen that the result of such SET insertion includes corrupted states that are not reachable because it does not take into consideration the internal error-masking capabilities of the combinational circuit. Nevertheless, we will see in the experiments that, for the analysis presented in this paper, such over-approximation is an appropriate choice.

Experimental results

The presented voter minimization technique has been implemented in Ocaml using the BDD library CUDD [START_REF] Cudd | CU Decision Diagram Package[END_REF] and the Ocaml interface MLCuddIDL [START_REF]MLCUDDIDL: An OCaml interface for the CUDD BDD library[END_REF]. Transition systems and set of states are expressed as BDD formulae [START_REF] Clarke | Mechanized reasoning and hardware design[END_REF].

The introduced logic domains (D 1 , D 2 , D 3 ) are encoded with multiple bits (two for D 1 and D 2 ; four for D 3 ) and the associated operators (e.g., Tables 2 and3) are expressed as logic formulae over those bits. For instance, the values of D 1 can be encoded with two bits (a, b) as:

1 as (1, 1) 0 as (1, 0) 0 as (0, 0) 1 as (0, 1)

In this encoding, the rst bit a is the correctness bit, and the second one b is the value bit. The N OT operator of D 1 can be represented by the function:

∧ 1 ((a 1 , b 1 ), (a 2 , b 2 )) = (a 3 , b 3 ) where a 3 = ((a 1 ∧ a 2 ) ∨ (a 1 ∧ ¬b 1 ) ∨ (a 2 ∧ ¬b 2 )∨ (¬a 2 ∧ (¬b 1 ∧ b 2 )) ∨ (¬a 1 ∧ (¬b 2 ∧ b 1 )) b 3 = b 1 ∧ b 2
And the OR operator is encoded as:

∨ 1 ((a 1 , b 1 ), (a 2 , b 2 )) = (a 3 , b 3 ) where a 3 = ((a 1 ∧ a 2 ) ∨ (a 1 ∧ b 1 ) ∨ (a 2 ∧ b 2 )∨ (¬a 1 ∧ (¬b 1 ∧ b 2 )) ∨ (¬a 2 ∧ (¬b 2 ∧ b 1 )) b 3 = b 1 ∨ b 2
BDDs proved to be quite ecient to express the data structures and the processing required by our technique. We made use of Rudell's sifting reordering [START_REF] Rudell | Dynamic variable ordering for ordered binary decision diagrams[END_REF] while building and applying the transition function. It allowed the semantic analysis of circuits up to 100 memory cells on a standard PC (Intel Core i5-2430M/2Gb-DDR3). For comparison, without reordering, the negative impact of big BDD structures on the algorithm performance was observed already for A '' denotes an out of time termination of the analysis (>20 mins).

circuits with 20-30 memory cells. We did not put much eorts in the optimization but we believe that there remain much opportunities for improvement.

We used both fault-models SEU (1, K) and SET (1, K) with K = 50, which allows K cycles/transitions to be computed eectively (∆ K ). The obtained results are a fortiori valid for any K ≥ 50. However, for non-restrictive trivial input/output specication and small circuits, it is not worth to choose higher K values since all reachable states might be visited within a small number of execution steps K, and no further optimization will be achieved even if we continue the execution. When all reachable states are visited the execution can be stopped even if K steps have not been fully performed. Thanks to the encoding of input/output specication into the circuit structure (Section 5), the reachable states also contain the information about the values of input signals and the relevance of primary outputs (for the error-propagation analysis). The number of steps K needed to explore the whole state space varies depending on the specication and circuit complexity. For small circuit (e.g., b02, b01) with simple input/output specication (e.g., only the reset at the very beginning), we visit all reachable states in K < 10 steps. On the other hand, for larger circuits (shift/add multipliers or the circuit b08) with explicit complex input/output interface specications (FSMs with 10 and more states), a higher value of K is rewarding and allows us to catch error masking behaviors that happen regularly (e.g., circuit restarts or returns to the initial state in cyclic FSMs within every 30-40 cycles).

Our analysis has been applied to common arithmetic units taken from the OpenCores project [START_REF]Open Source Hardware IPs: OpenCores project[END_REF] and from the ITC'99 benchmark suite [START_REF] Corno | RT-level ITC'99 benchmarks and rst ATPG results[END_REF]. For each circuit, we dened non-restrictive inputoutput specication for the sake of generality. For the majority of the circuits, the input pattern species only synchronous reset at its initialization phase and no further reset (b01, b02, b03, b04, b06, b09). Such non-restrictive patterns may reduce achievable optimizations, which could be signicantly increased if more details about the behavior of the surrounding circuit were provided. However, for the shift/add multiplier [START_REF] Kilts | Advanced FPGA Design: Architecture, Implementation, and Optimization[END_REF] the input-output specication is dictated by its functionality. The produced output is relevant only two cycle after the start signal has been raised (one cycle to fetch new data plus at least one cycle to process it). Since we should not Inria assume when the output is read out, we suppose that the data output may be read at any time two cycles after the last start and until the next start. As a result, our semantic analysis with this output specication shows that only the 8 product bits should be protected by voters.

Circuit b08 represents a group of self-stabilizing circuits that return to their initial state (and wait for the next start) within a bounded number of cycles (for b08, this period is 8 cycles). Additionally, by functionality, the circuit is supposed to be restarted periodically. The corresponding input and output specication allowed us to suppress all voters. We would like to highlight that any circuit with internal counters has a similar behavior of self-stabilization (the shift/add multiplier is another example). Table 4 summarizes the results of the analysis on those circuits in D 1 , D 2 , and D 3 , with the fault-model SEU (1, K). The column FFs shows the total number of memory cells in the original circuit, while the other columns show the number of remaining voters in the TMR circuit after the syntactic and semantic steps (without, with input, with input and output interfaces). In each case, we give the results obtained with the three logic domains.

The syntactic step eliminates all voters in circuits with a pipelined architecture such as adders, multipliers, or logarithmic units. With rolling pipelined architectures, a control part and a looped dataow circuit may require voter protection (e.g., none of the 28 voters of the shift/add multiplier are removed with only the syntactic analysis).

In general, control intensive circuits require a protection of their FSMs. Almost all memory cells of the serial ow comparator (b01) or the serial-to-serial converter (b09) have to be protected.

Nevertheless, our analysis is capable of suppressing a signicant amount of voters in many control intensive circuits. A circuit is usually composed of data and control ow parts and we can expect that most voters in the data ow part can be suppressed.

The logic domain D 2 is, most of the time, precise enough. However, correcting a bit-ip in D 2 (e.g., 0 → U → U) looses information. In some circuits, like b03 and b08, substantial logical error masking is performed by an FSM and the analysis fails to detect it.

The precision of the domain D 3 allows us to achieve better optimizations than the domain D 2 in circuits b03 and b08 (see Table 4). With D 3 , the corrupted FSM will recover to a precise state, while with D 2 its cells will recover to the correct unknown value U. This precise state plays a crucial role to show that the rest of the circuit, that depends on this FSM, will be cleaned up too.

The results for SET (1, K) are shown in Table 5. The number of suppressed voters did not change with D 2 . However, even the proposed approximations in Section 6.2 does not help to resolve the complexity problem for some circuits when analyzed with D 1 and D 3 . The bottleneck results from the large number of corruption combinations if a single combinatorial cone includes many memory cells. For example, in the circuit b03, there is an FSM of 2 cells where each cell is connected through a combinatorial circuit to 26 memory cells (mainly controlling their enable signals). As a result, to approximate the impact of an SET in this FSM, we have to calculate all possible corruption combinations of 26 cells, which is 2 26 congurations. The circuits that could not be analysed are marked by * in Table 5.

The scalability of logic domains D 1 , D 2 , and D 3 has also been compared. Figure 4 presents the growth of the RSS S i after i iterations (see Section 3) for the b03 and b06 circuits. The xed point is reached with less iterations in D 2 , and the number of states grows exponentially for D 1 versus linearly for D 2 . The same behavior is observed in all considered circuits.

The logic domain D 3 reaches the xed-point as fast as D 1 while keeping the same precision.

This fact is demonstrated in Table 6 where we measured the number of cycles to calculate the RSS for each domain (the column # iterations). The column seconds gives the execution time spent to calculate the RSS, and the last column ,# BDD nodes, gives the complexity of the RSS BDD representation in terms of allocated BDD nodes. On the one hand, the number of BDD nodes allocated to represent the RSS in larger circuits (b03, b08, b09) is much smaller with D 3 than with D 1 . On the other hand, the BDD structures in D 3 require more variables and are more time consuming to manipulate. The domain D 3 overapproximates the RSS (see Section 3.3) which leads to less allocated nodes in the larger circuits. While it allows us to keep the necessary precision for optimizations comparable to the ones allowed by D 1 , our existing implementation of D 3 would require further optimizations to be considered as an interesting compromise.

The bar graph of Figure 5 shows the ratio of the size of the RSS in D 1 to the corresponding size in D 2 . The RSSs in D 1 are several orders larger than the corresponding ones in D 2 . The most computation demanding step of the whole analysis is checking error propagation (see Section 5).

A prohibiting growth of BDD structures representing the set of states E i was observed with D 1

D 3 >1000 - - -
for circuits of around 30 memory cells. The logic domain D 2 allows the analysis (with input and output interfaces) of much larger circuits, up to 100 cells.

In order to evaluate the benets of our analysis, TMR has been applied to the benchmarks with the minimized set of voters. The inserted voters are triplicated following the practice in the existing industrial tools to avoid a single-point of failure and to protect against SETs. The ). As a case study, we have chosen Flash-based ProASIC3 FPGA as a synthesis target. Its conguration memory is immune to soft-errors [START_REF]Neutron-induced single event upset SEU[END_REF] and data memory is protected with voters. Table 7 compares the size and maximum frequency of the circuit with full TMR (i.e., voters after each FF) versus TMR with the optimized number of voters. The gains are presented in terms of the required FPGA hardware Core Cells (hw column) and maximum synthesizable frequency (MHz column). The gain in the maximum frequency depends on the location of the removed voters (in the circuit critical path or not). The reduction in area directly depends on the number of suppressed voters (up to 55%).

Application to time-redundancy

In this article, we have only considered hardware redundancy (TMR) but our approach also applies to time redundancy. Time-redundant schemes mask errors by voting on re-computed data. Such schemes reuse the combinational part of the circuit and have a much lower hardware overhead. We present one of our time redundant techniques [START_REF] Burlyaev | Design, optimization, and formal verication of circuit fault-tolerance techniques[END_REF] and sketch how our minimization analysis can be used in that context.

The Triple-Time Redundant Transformation (TTR) [START_REF] Burlyaev | Design, optimization, and formal verication of circuit fault-tolerance techniques[END_REF] takes a sequential circuit and returns a triple time-redundant version fault-tolerant to SETs. The transformed circuit is obtained by substituting each original memory cell with a sub-circuit, called a voting memory block (Figure 6).

Inria

These blocks introduce ve cells (d, d , d d, kA, kB ) and two voters (votA, votB ) to record and vote on the recomputed bits. Two new control wires fA and fB are used to organize voting; they are set by a small centralized FSM (the control block not shown here). The former input and output of the replaced memory cell are denoted by si and so. The input stream must be upsampled (x3) (e.g., from i 1 i 2 ... to i 1 i 1 i 1 i 2 i 2 i 2 ...) and the transformed circuit produces an upsampled (x3) output stream (e.g., from o 1 o 2 ... The advantage of TTR is to trade-o throughput for a low hardware overhead. For the benchmarks used in Section 7, TTR circuits are 1.6 to 2.1 times smaller than their TMR alternatives; they are also three times slower. The TTR scheme can be rened to allow dynamically changes of the level of time redundancy [START_REF] Burlyaev | Time-redundancy transformations for adaptive faulttolerant circuits[END_REF] (e.g., to use redundancy only in critical situations). Further, combining dynamic redundancy with micro-checkpointing it is possible to mask faults with only double-time redundancy [START_REF] Burlyaev | Automatic time-redundancy transformation for fault-tolerant circuits[END_REF].

to o 1 o 1 o 1 o 2 o 2 o 2 ...). Q d D Q Q d' D Q Q d'' D Q V 1 0 C 1 0 C Q kA D Q Q kB D Q so fA fB si V muxA muxB votA votB Voting Mechanism
As in full TMR, voters are introduced for each original cell to prevent error accumulation and some of them may be useless. The same criteria apply in this context: if our voter minimization analysis suppresses the voters after memory cells {M } in a TMR circuit and guarantees its tolerance w.r.t. SET (1, K), the same analysis can also suppress the voting mechanisms in the TTR memory blocks that correspond to cells {M } in the TTR circuit. The resulting optimized TTR circuit is guaranteed to be tolerant w.r.t. SET (1, 3K + 1). Only the voting mechanism (the lower right part in Figure 6) is suppressed. The d,d ,d chain remains to record the three recomputed bits and to propagate them to so but without error-masking. Again, the simplest example is a pipelined architecture where all voters (except at the primary outputs) are suppressed by our analysis. If a pipeline has n stages and each original memory cell is replaced by a memory block without voting, the number of stages becomes 3n. With an upsampled input (x3) such circuit is tolerant w.r.t. SET (1, 3n + 1) because any erroneous bit reaches the primary outputs within at most 3n + 1 cycles where they are masked. For the 4-stage 32-bits oating-point multiplier [START_REF]Open Source Hardware IPs: OpenCores project[END_REF], the tolerable fault-model is weakened from SET [START_REF]Open Source Hardware IPs: OpenCores project[END_REF][START_REF]Proceedings 2003 International Test Conference (ITC 2003), Breaking Test Interface Bottlenecks[END_REF] to SET (1, 13) but the overall TTR circuit size is reduced by 37%.

Our voter minimization approach might also be used to optimize the rened time-redundant schemes [START_REF] Burlyaev | Automatic time-redundancy transformation for fault-tolerant circuits[END_REF] and [START_REF] Burlyaev | Time-redundancy transformations for adaptive faulttolerant circuits[END_REF] but this application needs further investigation.

Related work

Existing industrial tools for applying TMR into FPGA protect against both kinds of soft error, SEUs and SETs. They include the Xilinx XTMR tool [START_REF] Bridgford | Single-event upset mitigation selection guide[END_REF][START_REF] Corporation | Xilinx TMRTool[END_REF], BYU/Los Alamos National Laboratory B-TMR [START_REF] Pratt | Improving FPGA design robustness with partial TMR[END_REF], Synopsys's Synplify Premier [START_REF] Sutton | Creating highly reliable FPGA designs[END_REF], and Mentor Graphics Precision Hi-Rel [START_REF] Do | New tool for FPGA designers mitigates soft errors within synthesis[END_REF]. In these tools, TMR is applied to circuit parts chosen by the user and, thus, the resulting circuits might not be fault-tolerant unless voters are inserted after each memory cell and primary circuit outputs. [START_REF] Do | New tool for FPGA designers mitigates soft errors within synthesis[END_REF] proposes a protection technique against SEUs that requires only memory cells triplication with a majority voter insertion. But this approach relies on the assumption that only memory cells are inuenced by radiation particles and that no signal perturbations in a combinatorial circuit occur. Thus, unlike our technique, the technique of [START_REF] Do | New tool for FPGA designers mitigates soft errors within synthesis[END_REF] protects only against SEUs and not against SETs.

While our static analysis uses exclusively logical masking to tolerate transient errors, many other works rely on electrical and latching-window properties of hardware to estimate the chance that errors will not manifest in failures. This is the primary reason why a good part of research on voter insertion, Selective Triple-Modular Redundancy (STMR), and partial hardware redundancy mainly focus on probabilistic approaches [START_REF]Proceedings 2003 International Test Conference (ITC 2003), Breaking Test Interface Bottlenecks[END_REF][START_REF] Johnson | Voter insertion algorithms for FPGA designs using triple modular redundancy[END_REF][START_REF] Alagoz | Fault masking by probabilistic voting[END_REF][START_REF] Samudrala | Selective triple modular redundancy based single-event upset tolerant synthesis for FPGAs[END_REF]. Contrary to our approach, they are not interested in formal guarantees that the nal circuit tolerates a fault-model. [START_REF] Johnson | Voter insertion algorithms for FPGA designs using triple modular redundancy[END_REF] shows how selective voter insertion minimizes the negative timing impact of TMR. In [START_REF] Ruano | Automatic insertion of selective TMR for SEU mitigation[END_REF], probabilities are used to apply TMR on selected portions of the circuit (STMR). In [START_REF] Samudrala | Selective triple modular redundancy based single-event upset tolerant synthesis for FPGAs[END_REF], STMR of combinational circuits species input interfaces using input signal probabilities. The main advantage of STMR over TMR is that the area of the STMR circuit is roughly two-thirds of the area of the TMR circuit. An original probabilistic-based idea is given in [START_REF] Imagawa | A cost-eective selective tmr for heterogeneous coarse-grained recongurable architectures based on dfg-level vulnerability analysis[END_REF] that allows a certain level of degradation in output correctness in order to optimize TMR at a Data Flow Graph (DFG) abstraction level. While this technique is originally dedicated to heterogenous systems, it could be applied to Digital Signal Processing (DSP) hardware as well. Since the proposed methods are probabilistic, some errors may propagate to primary outputs. In our approach, the circuit is guaranteed to mask all possible errors of the considered fault model.

Other works use model-checking to guarantee user-dened fault-tolerance properties [START_REF] Seshia | Verication-guided soft error resilience[END_REF][START_REF] Baarir | Complementary formal approaches for dependability analysis[END_REF]. [START_REF] Seshia | Verication-guided soft error resilience[END_REF] investigates which memory cells in SpaceWire node have to be protected so that even under an SEU occurrence the circuit keeps its functional properties, expressed as 39 assertions in linear temporal logic. If a cell is protected (fabricated with a special technology), an SEU cannot corrupt it. On the other hand, a protected cell consumes more power than a non-protected memory cell. As a result of verication-guided replacement of protected cells by their nonprotected alternatives, a 4.45X reduction in power has been achieved. The work [START_REF] Baarir | Complementary formal approaches for dependability analysis[END_REF] formally proves that some system properties of ATM controller are kept if an SEU happens. The authors evaluate the probability to obtain the expected property under faults.

Another group of formal studies investigates sequential circuit robustness symbolically [START_REF] Baarir | Feasibility analysis for MEU robustness quantication by symbolic model checking[END_REF][START_REF] Fey | Computing bounds for fault tolerance using formal techniques[END_REF] or by interpolation [START_REF] Cabodi | Complete and Eective Robustness Checking by Means of Interpolation[END_REF]. Since robustness is introduced probabilistically these work combine both Inria formal and probabilistic worlds.

While the aforementioned formal studies do not address voter minimization, their approaches to fault-tolerance and robustness are related to our work.

It is worth to notice that the introduced reachability analysis with multi-value encoding can be also interpreted within the well-known tainting dataow-based analysis [START_REF] Denning | Certication of programs for secure information ow[END_REF] and path sensitisation theories [START_REF] Chiang | Path sensitization, partial boolean dierence, and automated fault diagnosis[END_REF]. The former assigns a security-related mark to each information bit and tracks its propagation, just like we tag some bits as erroneous. The later approaches check if there is a path so that a signal change along that path alters the output. In our case, the signal change corresponds to an error injection, e.g., a bit-ip, and we check whether this change can propagate to corrupt the output.

Conclusion

We proposed a logic-level verication-guided approach to minimize the number of voters in TMR circuits that guarantees a user-dened fault-model to be masked. Our approach is based on reachable state set computations and input/output interface specications. In order to avoid analyzing the triplicated circuit, we introduced three logic domains, which allowed us to perform the analysis on a single copy of the circuit. Our analysis shows that some voters are useless and can be safely removed from the TMR application. We have used as case studies several arithmetic circuits as well as the benchmark suite ITC'99. They show that our technique allows not only a signicant reduction in the amount of hardware resources (up to 35% for data ow intensive circuits and up to 55% for control ow intensive ones), but also a signicant increase in the clock rate, compared to the full TMR method that inserts a voter after each memory cell.

We demonstrated that the choice of the logic domain inuences the scalability of the analysis and its precision. We considered both SEU and SET fault-models and explained the modeling methodogy. As the experimental results show, the same level of optimization can be reached for both fault-models, but the SET model implies a potentially large number of corruption combinations to be examined, which can cause an analysis bottleneck.

Further research directions include the application of our approach to other fault-tolerance techniques, taking into account other optimization criteria like frequency and making the approach modular. We review these three topics in turn.

Frequency maximization

Voters ordering, discussed in Section 3.2, could also take into account other optimization criteria than voter minimization. For instance, we may increase the maximum synthesizable frequency by removing rst the voters on the critical path. However, removing a voter from the critical path may make another path critical. Thus, the choice of the next voter to remove depends not only on the existing ordering but also on the current critical path. However, the critical path strategy may not result in the minimal number of voters. In this sense, the two criteria number of voters and synthesizable frequency are orthogonal, and bi-criteria optimization must be studied.

Modularity

Applying our analysis in a modular manner can increase its scalability and, consequently, the applicability of the proposed technique to larger circuits. The hierarchical compositional design of today's circuits makes it natural to decompose a circuit to the IPs of its block-by-block structure.

Such structural partitioning requires the deep design understanding and has already been used RR n°9004 in the model checking of Intel CPUs [START_REF] Aagaard | Formal verication using parametric representations of boolean constraints[END_REF]. In our case, the presented analysis can be applied to circuit sub-components after the decomposition. After the minimization of internal voters in each sub-circuit, the components should be interconnected again to rebuild the whole design.

However, the interconnection wires should include voters to guaranty the fault-tolerance property of the nal optimized circuit. Such an approach is not optimal even if the local input/output specications are precise, because some of the interconnection voters may be redundant. Only a global analysis on the blocks containing such wire with a voter (as an input or output wire) can safely remove interconnection voters.

If a decomposition in sub-circuits is not known, the circuit netlist has to be automatically divided and the input-output specications of its parts have to be found. These steps by themselves present complex tasks and require deep investigation. Here, we sketch some preliminary ideas about how these problems can be solved. First, a circuit netlist can be separated according to some syntactic criteria, e.g., the circuit cuts should be performed at wires that are included in the biggest number of sequential loops. Such an approach eliminates as many sequential loops as possible by reducing the number of sequential loops in each sub-component. It limits the number of potential points where the voters have to be inserted.

After the circuit decomposition, our semantic analysis can be applied to each of its sub-parts.

The main diculty lies in the identication of input/output specication of each sub-circuit to perform the local semantic analyses. While the input/output specication for c 1 and c 2 sub-circuits can be extracted from the global specication in the parallel decomposition (case b, Figure 7), the sequential and feedback decompositions (cases a and c) create unknown internal specications (marked in red). They have to be found for each sub-part. Consider, for instance, the unknown input specication i 2 for the sequential decomposition (case a). The signals in i 2 are the outputs o 1 . Since the netlist c 1 and its input specication i 1 fully describe the behavior of c 1 , o 1 and i 2 can be described by the same NBA. In the worst case, such NBA could be as big as c 1 multiplied by the size of i 1 , which can be prohibitive for the following semantic analysis of c 2 sub-circuit. Consequently, the extracted NBA should be over-approximated to lower the complexity. Naturally, the overapproximation may inuence the precision of the further semantic voter minimization in c 2 .

The feedback decomposition is even more complex because of the mutual dependency between sub-components c 1 and c 2 . These modularity issues are complex but important and valuable since many other static analyses of circuits could benet from them. Inria

Figure 1 :

 1 Figure 1: Input interface as a NBA (a) and its deterministic version (b)

Figure 2 :

 2 Figure 2: Original circuit with the surrounding interface circuit.

  be masked in a combinatorial circuit by or( , 1) = 1 or and( , 0) = 0. The precise modelling of a glitched signal in a TMR circuit requires the knowledge of its correct value (present in the corresponding signals of the two other redundant modules). Consequently, the precise domain D 1 is extended as D t to model a glitch propagation in a combinatorial circuit of one redundant module:

Figure 3 :

 3 Figure 3: Combinational cones for SET modeling.

¬ 1

 1 (a, b) = (a, ¬b) We used the Quine-McCluskey algorithm to simplify the boolean functions corresponding to the AN D and OR operators of D 1 . The AN D operator is encoded as:

D 1 D 2 D 3 D 1 D 2 D 3 D 1 D 2 D 3 FP

 123123123 denotes an out of time termination of the analysis (>20 mins)

Figure 4 :

 4 Figure 4: Logic Domain Comparison: Reachable State Space Size.

Inria

Figure 5 :

 5 Figure 5: Logic Domain Comparison: Size Ratio of RSS.

Figure 6 :

 6 Figure 6: TTR voting memory block.

Figure 7 :

 7 Figure 7: a) sequential, b) parallel, and c) feedback circuit decomposition.

Table

  1: Voter Minimization, Syntactic Analysis Step

			Circuit	FFs Syn.
	Data	Flow I.	Pipe.FP.Mult.8x8[1] 121 Pipe.log.unit[1] 41 Sh./A.Mult.8x8[36] 28	0 0 28
			ITC'99[21](subset)
	Control Flow	Intensive	b01 Flows Compar. b02 BCD recogn. b03 Resourc.arbiter 30 29 5 3 4 3 b06 Interrupt Hand. 9 3 b08 Inclus.detect. 21 21
			b09 Serial Convert.	28	21

Table 2 :

 2 Operators for 4-value logic domain D 1

1

  We will use this notation with other initial states and transition functions.

	Algorithm 1 Semantic Analysis Main Loop
	Input : MVFS ; // The minimum vertex feedback set;
	∆;	// The circuit transition function;
	s 0 ;	// The initial state;
	Output : V ;	// The subset of vertices (i.e., memory
		cells) after which a voter is needed
	1: V := MVFS ;
	2: RSS := {s 0 } * ∆ ;
	3: forall m ∈ MVFS
	4:
		Inria

Table 3 :

 3 Operators for 4-value logic domain D 2

  Algorithm 2 Semantic Analysis with Output Specication

	Input : MVFS ; // The minimum vertex feedback set;
	∆;	// The circuit transition function;
	s 0 ;	// The initial state;
	Output : V ;	// The subset of vertices (i.e., memory
		cells) after which a voter is needed

1: V := MVFS ; 2: RSS := {s 0 } * ∆ ; 3: forall m ∈ MVFS 4:

Table 4 :

 4 Voter Minimization, SEU model, Boolean domains D 1 | D 2 | D 3 . 1 D 2 D 3 D 1 D 2 D 3 D 1 D 2 D 3

		Circuit	FFs	Syn.		Semantic			Sem.Inp.		Sem.Out.
	Data Flow Int.	FP Multiplier 8x8[1] log.unit[1]	121 41	0 0	0 0	0 0	0 0	0 0	0 0	0 0	0 0	0 0	0 0
		Multiplier 8x8[36]	28	28	19	19	19	19	19	19	8	8	8
		ITC'99[21](subset)
	Control Flow Intensive	b01 Cmp. serial ows b02 BCD recognizer b03 Resource arbiter b06 Interrupt handler b08 Inclusion detector	5 4 30 9 21	3 3 29 3 21	3 2 17 3 21	3 3 29 3 21	3 3 17 3 21	3 2 17 3 0	3 3 29 3 21	3 3 17 3 0	3 2 17 3 0	3 3 29 3 21	3 3 17 3 0
		b09 Serial converter	28	21	20	20		20	20		20	20

D

Table 5 :

 5 Voter Minimization, SET model, Boolean domains D 1 | D 2 | D 3 .

	Circuit	FFs	Syn.	Semantic	Sem.Inp.	Sem.Out.
	Data Flow Int.

Table 6 :

 6 Time and memory resources to calculate the RSS.

			δ, sec # iterations seconds # BDD nodes
		D 1 0.037	9	0.01	156
	b01	D 2 0.037	6	0.01	78
		D 3 0.060	6	0.01	151
		D 1 0.020	9	0.005	81
	b02	D 2 0.020	9	0.04	66
		D 3 0.024	9	0.01	127
		D 1	0.42	17	2.53	1506
	b03	D 2	0.44	7	0.28	311
		D 3 875.670	7	235.13	668
		D 1 0.044	8	0.024	473
	b06	D 2 0.052	6	0.018	130
		D 3 0.056	6	0.02	256
		D 1 0.364	40	3.14	27813
	b08	D 2 0.356	5	0.02	324
		D 3 41.49	5	48.08	1222
		D 1 31.332	32	27.57	2919
	b09	D 2 0.852	20	1.04	446

Table 7 :

 7 Frequency and area gain of optimized vs full TMR.

		TMR circuit	voters MHz	gain	hw	gain
	Data Flow I.	Pipel.FP.Mult.8x8 Optimized Pipel.log.un. Optimized	121 0 41 0	60.5 71.0 17.4% 1831 21.7% 2338 128.3 693 184.1 43.5% 447 35.5%
		Shift/Add.Mult.8x8	28	106.0		537
		Optimized	8	108.0 1.9%	408 24.0%
		b01 Flows Compar.	5	162.6		126
		Optimized	3	162.6	0%	114	9.5%
	Control Flow Intensive	b02 BCD recogn. Optimized b03 Resourc.arbiter Optimized b06 Interrupt Hand. Optimized b08 Inclus.detect. Optimized	4 2 30 17 9 3 21 0	181.9 206.6 13.6% 81.6 109.0 33.6% 144.8 144.8 0% 115.4 142.4 23.4%	69 60 594 576 168 134 20.2% 13.1% 3.0% 484 216 55.4%
		b09 Serial Convert.	28	89.4		584
		Optimized	20	95.0	6.3%	565	3.3%
	nal circuits have been synthesized with Synplify Pro with no optimization applied (Resource
	Sharing, FSM Optimization, etc.

RR n°9004

RESEARCH CENTRE GRENOBLE -RHÔNE-ALPES