N Dornic

S H Tran

Z Khatir

A Ibrahim
email: ali.ibrahim@ifsttar.fr

R Lallemand
email: richard.lallemand@ifsttar.fr

J P Ousten

J Ewanchuk
email: j.ewanchuk@fr.merce.mee.com

THIS LINE WITH YOUR PAPER IDENTIFICATION

Keywords: Power cycling, lifetime model, finite element modeling, stresses, strains, IGBT, power module, wire-bonds, accelerated ageing, junction temperature

In this paper, a lifetime model for bond wire contacts of Insulated Gate Bipolar Transistors (IGBT) power modules is reported. This model is based on power cycling tests obtained under accelerated conditions and a finite element model taking into account the electrical, thermal and mechanical coupling. It allows to estimate the bond-wires lifetime for a large scale of junction temperature swing amplitudes (∆𝑻 𝒋 ) and stress durations (𝒕 𝒐𝒏 ). To build it, a numerical design of experiment was performed in both high and low stress values (∆𝑻 𝒋 ). Then, a strain-life curve has been constructed where average strain values on a defined volume around the contact areas between top-metallization and the most exposed bond-wires to fatigue and lift-off have been used. As result, it has been shown that the total strain is linearly dependent with ∆𝑻 𝒋 and power law dependent with 𝒕 𝒐𝒏 . The combination of the strain-life relation and the strain dependency with stress parameters leads to the lifetime relationship. The obtained lifetime model has been satisfactorily validated with some additional experimental points obtained from literature and with a large range of values for 𝒕 𝒐𝒏 . This methodology can easily be replicated to other structures and is quite generic.

I. INTRODUCTION

OWER semiconductor devices are the key components of power electronic systems. They are also the weak point of these systems in terms of reliability. During operations, they undergo high stresses (ambient temperature, temperature cycling, humidity, etc…). As commonly known, due to temperature cycling and differences in the coefficient of thermal expansion of materials, these devices are subjected to thermo-mechanical damage accumulation, which affects their lifetime and therefore impacts the reliability of the power modules [START_REF] Smet | Ageing and Failure Modes of IGBT Modules in High-Temperature Power Cycling[END_REF][START_REF] Lutz | Packaging and Reliability of Power Modules[END_REF][3][START_REF] Morozumi | Reliability of Power Cycling for IGBT Power Semiconductor Modules[END_REF].

Manufacturers are faced with the need to provide devices that are not only reliable but also compatible with a predictable maintenance schedule. Indeed, from an economic point of view, it is less detrimental to perform a planned maintenance with the replacement of these systems than to undergo a sudden stop due to a failure. It is therefore necessary to develop diagnostic tools in order to predict the remaining lifetime of equipment for maintenance purpose before any failure occurrence. To this end, numerous lifetime models of power electronic devices have been developed. They can be divided in three categories: empirical models [START_REF] Held | Fast power cycling test of IGBT modules in traction application[END_REF][START_REF] Bayerer | Model for power cycling lifetime of IGBT modules -various factors influencing lifetime[END_REF][START_REF] Scheuermann | A new lifetime model for advanced power modules with sintered chips and optimized Al wire bonds[END_REF], physics-based models [START_REF] Drofenik | Multi-domain simulation of transient junction temperatures and resulting stress-strain behavior of power switches for long term mission profiles[END_REF][START_REF] Steinhorst | Approach of a physically based lifetime model for solder layers in power modules[END_REF][START_REF] Schilling | Power cycling testing and FE modelling focussed on Al wire bond fatigue in high power IGBT modules[END_REF][START_REF] Riedel | Reliability of large area solder joints within IGBT modules: Numerical modeling and experimental results[END_REF][START_REF] Yang | A time-domain physicsof-failure model for the lifetime prediction of wire bond interconnects[END_REF][START_REF] Yang | Physics-of-failure lifetime prediction models for wire bond interconnects in power electronic modules[END_REF][START_REF] Deplanque | Lifetime prediction of SnPb and SnAgCu solder joints of chips on copper substrate based on crack propagation FE-analysis[END_REF][START_REF] Matsunaga | Thermal Fatigue Life Evaluation of Aluminum Wire Bonds[END_REF][START_REF] Sasaki | Thermal and structural simulation techniques for estimating fatigue life of an IGBT module[END_REF][START_REF] Huang | A lifetime estimation technique for voltage source inverters[END_REF] and datadriven or stochastic models [START_REF] Zio | Particle filtering prognostic estimation of the remaining useful life of nonlinear components[END_REF][START_REF] Celaya | Prognostics of Power MOSFETs under Thermal Stress Accelerated Aging using Data-Driven and Model-Based Methodologies[END_REF][START_REF] Saha | Towards prognostics for electronics components[END_REF][START_REF] Alghassi | Prognostics and Health Management of Power Electronics[END_REF][START_REF] Astigarraga | D Analysis of the Results of Accelerated Aging Tests in Insulated Gate Bipolar Transistors[END_REF][START_REF] Chen | PHM Application of Power Converters Using Health Precursor of Power MOSFETs[END_REF].

Empirical lifetime models have been built from numerous accelerated power cycling tests. However, these models based on low cycle fatigue results do not have predictive capabilities outside the explored test conditions and an extrapolation must be done when applying the models from accelerated tests to field conditions, i.e. under high cycle fatigue conditions.

Physics-based lifetime models are driven by physics-offailure (PoF) analyses and can provide a promising alternative to empirical models [START_REF] Kovacevic-Badstuebner | Modelling for the Lifetime Prediction of Power Semiconductor Modules[END_REF]. These models can be split in two main categories: stress-based models [START_REF] Drofenik | Multi-domain simulation of transient junction temperatures and resulting stress-strain behavior of power switches for long term mission profiles[END_REF][START_REF] Steinhorst | Approach of a physically based lifetime model for solder layers in power modules[END_REF][START_REF] Schilling | Power cycling testing and FE modelling focussed on Al wire bond fatigue in high power IGBT modules[END_REF][START_REF] Riedel | Reliability of large area solder joints within IGBT modules: Numerical modeling and experimental results[END_REF] and degradation-based models [START_REF] Yang | A time-domain physicsof-failure model for the lifetime prediction of wire bond interconnects[END_REF][START_REF] Yang | Physics-of-failure lifetime prediction models for wire bond interconnects in power electronic modules[END_REF][START_REF] Deplanque | Lifetime prediction of SnPb and SnAgCu solder joints of chips on copper substrate based on crack propagation FE-analysis[END_REF][START_REF] Matsunaga | Thermal Fatigue Life Evaluation of Aluminum Wire Bonds[END_REF][START_REF] Sasaki | Thermal and structural simulation techniques for estimating fatigue life of an IGBT module[END_REF][START_REF] Huang | A lifetime estimation technique for voltage source inverters[END_REF]. Both types can be used for remaining lifetime prediction and extrapolation from accelerated to the field operating conditions. In the first type, lifetime is related to the stress experienced, e.g. junction temperature swings (∆𝑇 𝑗 ) and stress durations (𝑡 𝑜𝑛 ), through mechanical or physical quantities such as strains and energy densities. In the latter, the lifetime is related to the stress undergone through material degradation, cracking, crack propagation, recrystallization.

The aim of this paper is to propose a stress-based lifetime modeling approach applied to top-side interconnection (wirebond contact) of an IGBT power module. The approach consists in carrying out accelerated aging tests in order to obtain the corresponding number of failure cycles. At the same time, simulations are performed in order to reproduce experimental loads and stresses as accurately as possible using electricalthermal and mechanical coupled finite element models. From simulation results, inelastic and elastic strains will be extracted in same accelerated conditions as in experience and will be related to the lifetime (𝑁 𝑓 ) obtained experimentally. The main assumption is to say that the obtained relationship between strains and lifetime can be extended to low stress (∆𝑇 𝑗 ), in nonaccelerated conditions. This hypothesis can be made because the modules used were chosen to present only one mode of degradation, i.e. the bond-wire lift-off. In this paper, the temperature swing amplitude (∆𝑇 𝑗 ) and the time duration (𝑡 𝑜𝑛 ) of the applied stress, i.e. the heating time, have been considered for the lifetime model. Nevertheless, the 𝑡 𝑜𝑛 effect has been assessed thanks to experimental results. Taking into account this parameter in the finite element model requires the consideration of specific time-dependent behavioral laws, such as creep, for top-side metallization and wire-bond materials. This will be the subject of a future paper.

II. POWER CYCLING TESTS METHODOLOGY AND RESULTS

A. Test circuit and protocol

In order to build the lifetime model, accelerated aging tests have been performed on IGBT power modules. These latter are commercially available SKIM63 (1200V-300A) from Semikron. These devices are six-pack modules with three individual phase legs on separated DBC substrates. These power modules were chosen for their robust die attach in order to concentrate the degradations only in the topside interconnections. The chips are all sintered with a nanoparticle silver paste, making the connections stronger than with classical solders. Hence, the degradations observed concern only the metallization and the bonds contacts. The power modules are mounted in a water-cooler heat-sink device with a thermal grease interface. In order to reach high temperature swing levels, a 5-mm-thick aluminum plate is inserted between the module and the cooling device with a second thermal grease layer. As shown in the circuit schematic in fig. 2, the power cycles are performed on 3 modules at a time for which only the central leg is tested (see fig. 1). This constitutes 2 DUTs respectively high side and low side switches per power module.

The aging consists on repetitive cycles of self-heating and cooling phases. As test parameters, the minimum junction temperature (𝑇 𝑗𝑚𝑖𝑛 ) was set to 35°C, two stress durations (𝑡 𝑜𝑛 ) have been tested: 3s and 20s. The cooling duration (𝑡 𝑜𝑓𝑓 ) is twice as long as the heating duration (𝑡 𝑜𝑛 ) in order to reach the reference temperature of the cooling system at the end of each cycle, i.e. 6s and 40s respectively. The power devices undergo thermal stresses due to temperature swings ∆𝑇 𝑗 between a maximum (𝑇 𝑗𝑚𝑎𝑥 ) and a minimum junction temperature (𝑇 𝑗𝑚𝑖𝑛 ) depending on the setting parameters. The DC current load (IL) is set in order to reach the targeted temperature swings (110°C, 90°C and 70°C), see table I.

All electrical and thermal measurements are monitored and recorded with a data acquisition system (Dewetron). The switching sequence is controlled by auxiliary power MOSFETs (fig. 2). A permanent low current (𝐼 𝑠𝑒𝑛𝑠𝑒 =50mA) is flowing through the devices under test (DUTs) in order to get the junction temperature (𝑇 𝑗 ) by a thermo-sensitive electrical parameter (TSEP), i.e the collector-emitter voltage (𝑉 𝐶𝐸 @𝑉 𝐺𝐸 =15V). The case temperature, below each IGBT chip of the central leg, and inlet water temperature are measured by close thermocouples for evaluating junction-to-case (𝑅 𝑡ℎ𝑗𝑐 ) and junction-to-water (𝑅 𝑡ℎ𝑗𝑤 ) thermal resistances. The chosen ageing indicators are collector-emitter voltage drop (𝑉 𝐶𝐸 ) and junction-to-water thermal resistance (𝑅 𝑡ℎ𝑗𝑤 ). These parameters are always measured in the same conditions before, during and after the aging in a static characterization phase. During the power cycling, the aging is automatically and regularly interrupted and the characterizations of ageing indicators are performed.

The measured voltage 𝑉 𝐶𝐸 may possibly include a thermal contribution due to any increase in thermal resistance from possible delamination of the die attach. So, this latter possible contribution needs to be removed from the measured 𝑉 𝐶𝐸 in order to detect only the contribution due to top-die interconnection degradations. Thus, a correction on the measured 𝑉 𝐶𝐸 is done to get only the degradations related to topmetal and bonding wires contacts. This correction consists in subtracting the part of 𝑉 𝐶𝐸 which can possibly be due to an increase of temperature related to an increase of thermal resistance, if any solder delamination occurs.

For that purpose, a thermal calibration is carried out at the beginning of aging tests, before any degradation. During this calibration, the drop voltage 𝑉 𝐶𝐸 is recorded and plotted in a temperature range from 75°C to 90°C after reaching thermal equilibrium. This variation in temperature is obtained by modifying the inlet water flow to change the cooling performance. The obtained dependence between the junction temperature (𝑇 𝑗 ) and the drop voltage (𝑉 𝐶𝐸 ) is linear and offers an average corrective coefficient of 𝑉 𝐶𝐸 with temperature. This enables a correction in 𝑉 𝐶𝐸 to account for the possible difference between the measured junction temperatures at initial and actual characterizations. As expected, all tests have led to insignificant 𝑅 𝑡ℎ increase.

B. Test results

As results, all tested devices have failed by bond-wire liftoff. As an illustration, it can be seen in fig. 3 the evolution during aging of the relative variation of 𝑉 𝐶𝐸 for the 3 modules tested at ∆𝑇 𝑗 = 90°C. No variation in thermal resistance was detected, indicating that no delamination has occurred in the structure. This result is confirmed by scanning acoustic microscopy (SAM) analyses performed after the ageing for both long (Fig. 4a) and short cycling (Fig. 4b). Hence, the degradation of wire bonds is the only failure mode. The full test conditions and results in number of cycles to failure (𝑁 𝑓 ) are given in table I for 𝑡 𝑜𝑛 = 3 s and in table II for 𝑡 𝑜𝑛 = 20 s. In these tables, the load DC current, the 𝑁 𝑓 value for each tested devices and the averaged 𝑁 𝑓 value for each test condition are given. As expected, lifetime is reduced when 𝑡 𝑜𝑛 is increased.

III. FINITE ELEMENT MODEL AND RESULTS

Finite element modelling is required in order to compute stress and strain development within the power module assembly during power cycling. However, obtaining correct stress and strain maps inside the structure requires : i) detailed knowledge of the geometry as well as material properties and behavior laws and ii) the thermal stresses the more accurately as possible, i.e. the correct maps of temperatures and temperature gradients. For this purpose, the electro-thermomechanical coupling problem must be taken into account. In particular, a special attention must be kept for the top-metal layer in the active areas of the dies and the bond-wires.

A. Description of the finite element model geometry

We recall that only the central leg has been tested and only bond-wire lift-off of IGBT chips occurred in experimental tests. So, as expected, the results of interest are at the level of metallization and contacts with the bonding wires of the corresponding substrate. The lateral substrates therefore have no thermomechanical influence and can be avoided in the numerical model for simplification reasons.

The model is shown in figs.5 and 6. The power module is made-up of the central substrate which is mounted on an aluminum heat-sink. An aluminum plate is inserted between the heat-sink and the power module as for experimental tests to reach high temperature variations. Two thermal interface materials (TIM) layers are used as shown in fig. 5 to ensure the thermal contact between the substrate and aluminum plate and between the aluminum plate and the heat-sink.

The geometrical model of the substrate is shown in fig. 6. All the IGBT dies are taken into account with their thin top-metal layers. The four diodes are not considered in the model. The metallization layers cover the active areas of the dies. A direct copper bond (DCB), with an aluminum nitride (AlN) ceramic, is used as substrate where the eight chips are attached on copper patterns (copper1 and copper2).

B. Material nature and properties

All materials, with their dimensions, are given in table III. These are ranked from top to bottom, from the wire-bonds to the heat-sink. The material properties of the power assembly, used for the finite elements model, are given in table IV. Fragile materials, like silicon and ceramic, exhibit deformation limited to elastic domain only, i.e. linear properties are used for them. In the temperature range of active cycling tests, aluminum is modeled by elastoplastic behavior laws as visible in fig. 7. The Ag sintering layers are generally considered as viscoplastic materials. Nevertheless, they have been considered here as elastic. This simplifying assumption is justified by the high rigidity of the silicon chips preventing the lower material layers, including the die-attach, from having an impact on the deformations of the metallization and the wires in the top-side. The mechanical behavior of the die-attaches therefore has no impact on the mechanical quantities on the top-side of the chips. Their consideration is only justified for solving the electrothermal problem and not the mechanical problem.

Concerning the electrical behavior of IGBTs, since the power cycling is in DC mode, only Joule effects is considered. Moreover, it is only necessary to have representative power losses within the dies. Thus, these ones are considered as conductive layers with anisotropic resistivities. Since IGBT chips can be considered as multiple elementary IGBT cells in parallel, the current flows only in the vertical axis (i.e. through the thickness of the dies). So, in order to simulate such "vertical" conduction, the in-plane resistivities data input for IGBTs are supposed high enough 𝜌 𝑥-𝑖𝑔𝑏𝑡 = 𝜌 𝑦-𝑖𝑔𝑏𝑡 = 10 6 𝛺𝑚, whereas the vertical resistivity is fitted in order to have the same on-state voltage as in experiments. This is to have the same dissipated power in the heating phase than in experiments. Static I-V characteristics are plotted for different temperatures with a curve tracer, so that the temperature effect on the 𝑉 𝐶𝐸 is also taken into account : In these relations, 𝑇 𝒋 is in °C and 𝑉 𝐶𝐸 in Volts.

𝑉 𝐶𝐸 (𝑇 𝑗 ) = 𝑘 1 (𝑇 𝑗 ) 𝐼 𝑐 𝑘 2 (𝑇 𝑗 ) + 𝑘 3 (𝑇 𝑗 ) (1

C. Boundary conditions

As electrical boundary conditions, the reference for voltage (V=0) is applied to copper3 pattern and the load current (IL) is injected into copper1 pattern (see fig. 6).

As thermal boundary conditions, a convective condition is assumed at the bottom face of the heat-sink, with a convective coefficient of h = 4000 W/m 2 .K and a bulk temperature of 35°C. All other boundaries are considered as adiabatic.

As mechanical boundary conditions, three among the four corners of the heat-sink are fixed with no displacement allowed.

D. Simulation Results

Table VI gives the numerical experimental design carriedout in DC mode. The simulated values in ∆𝑇 𝑗 are: 15, 25, 55, 70, 90 and 110°C. For an effective comparison with the tests, the ∆Tj values here are the junction temperature mean values calculated over the IGBT chip active area that can be compared with the TSEP measurements.

Concerning loads, a succession of 5 cycles of power current is simulated as schematically shown in fig. 8. The heating durations (𝑡 𝑜𝑛 ) are set to 3s and the cooling durations (𝑡 𝑜𝑓𝑓 ) to 10s to allow the temperature to reach 𝑇 𝑗𝑚𝑖𝑛 . Load currents (IL) are then determined to reach the desired ∆𝑇 𝑗 values. In table VI, simulated load currents are given for comparison to experimental ones (see tables I and II). It can be seen that for ∆𝑇 𝑗 = 110°C, 90°C and 70°C, currents used as input in the model are almost the same as the experimental DC ones, the small difference being probably the result of an inexact definition in the geometry or the material properties used in the model. It is necessary to simulate a few cycles for the mechanical results, e.g. strain variation per cycle, to reach stabilized values from one cycle to another. As illustration, fig. 9 gives the temperature distribution over the substrate at the end of a power cycle for the first simulated case (IL = 272 A and 𝑡 𝑜𝑛 = 3s). The average temperature over the IGBT active area is 145°C. This is consistent with a minimum junction temperature of 35°C and a 𝑇 𝑗 temperature swing of 110°C.

As outputs, some physical quantities averaged over a defined volume have been computed. Among them, a focus is made on the elastic and inelastic strain variations per cycle at the metallization layer of the IGBT chip near the bond contacts where lift-off occur experimentally. The concerned bond contacts are shown in fig. 10 inside the white rectangle. This figure shows the plastic strain distribution at the end of a heating phase over the metallization layer of one of the four central IGBTs. In order to avoid singular values of such quantities, averaged values of elastic and plastic strains over a defined volume of this metallization is considered:

Δ𝑥 = ∑ Δ𝑥 𝑖 •𝑣 𝑖 𝑖 ∑ 𝑣 𝑖 𝑖 (3)
The considered volume is shown by the white rectangle in fig. 10 and consists on a number of finite element volumes. In relation (3) Δ𝑥 stands for the averaged value, i.e. elastic variation per cycle (Δ𝜀 𝑒𝑙 ) or plastic variation per cycle (Δ𝜀 𝑝𝑙 ); Δ𝑥 𝑖 is the mean value of quantity ∆𝑥 over the elementary volume 𝑖 and 𝑣 𝑖 is the volume of the corresponding volume element. The summation is done over the volume elements contained in the defined volume.

As results, it can be seen in fig. 11, the evolution during some cycles of junction temperature of the high side IGBT (average value over the active area), the plastic strain and elastic strain for IL = 272 A and 𝑡 𝑜𝑛 = 3s conditions. Concerning strain variations, the von Mises representation has been chosen. During the power cycle, the top-metal material successively undergoes cyclic tensile and compressive forces so that it undergoes plastic deformations in compression then in traction. Almost the same amount of elastic strain occurs during the heating and cooling phases, the elastic strain variation during a full cycle is the sum of the corresponding values during "on" and "off" phases. In table VII, it is given the values of Δ𝜀 𝑒𝑙 and Δ𝜀 𝑝𝑙 respectively for ∆𝑇 𝑗 =110, 90 and 70°C from simulation results for test condition 𝑡 𝑜𝑛 = 3s: These calculated values in ∆𝜀 𝑒𝑙 and ∆𝜀 𝑝𝑙 obtained for ∆𝑇 𝑗 = 70, 90 and 110°C can be plotted in a graph ∆𝜀 𝑒𝑙 = 𝑓(𝑁 𝑓 ) and ∆𝜀 𝑝𝑙 = 𝑔(𝑁 𝑓 ), where corresponding 𝑁 𝑓 are given in table I. Theoretically, it is expected linear curves in log-log axes [START_REF] Manson | Thermal Stress Low-cycle Fatigue[END_REF]. This is visible in fig. 12 with the segments of solid lines (blue for elastic strains and red for plastic strains).

So, from these three points in ∆𝑇 𝑗 , the following relationships can be identified :

∆𝜀 𝑒𝑙 = 𝐴. 𝑁 𝑓 -𝑎 (4)
∆𝜀 𝑝𝑙 = 𝐵. 𝑁 𝑓 -𝑏 [START_REF] Kovacevic-Badstuebner | Modelling for the Lifetime Prediction of Power Semiconductor Modules[END_REF] with: 𝐴 = 7.48 × 10 -4 ; 𝑎 = 2.11 × 10 -2 ; 𝐵 = 3.66 × 10 -2 ; 𝑏 = 0.221.

It must be kept in mind that this model does not take into account the duration of stress, the behavior laws used for aluminum (metallization and bond-wires) being time-independent. To this end, it would have been necessary to introduce creep laws for these materials. These data are extremely difficult to characterize and literatures does not provide them for the considered geometries (thin films and wires bond). Since the lifetime is assumed to be unequivocally related to the strain variations, the relationships between strain and 𝑁 𝑓 , i.e. eq.( 4) and ( 5), remain valid whatever the 𝑡 𝑜𝑛 . Thus, the strain values obtained for 𝑡 𝑜𝑛 =3s can be considered as a relative reference and the results in 𝑁 𝑓 obtained for 𝑡 𝑜𝑛 = 20s allows to get the new corresponding strains (for 𝑡 𝑜𝑛 = 20s), see table VIII. Furthermore, in fig. 13 are plotted the dependences in ∆𝑇 𝑗 of elastic and plastic strains variations per cycle as well as total strain, where:

Δ𝜀 𝑡𝑜𝑡𝑎𝑙 = Δ𝜀 𝑒𝑙 + Δ𝜀 𝑝𝑙 = 𝐴. 𝑁 𝑓 -𝑎 + 𝐵. 𝑁 𝑓 -𝑏 (6)
Elastic strain should be theoretically zero at ∆𝑇 𝑗 = 0°C, then saturates almost to ∆𝑇 𝑗 = 30°C around a value of 5 × 10 -4 . Plastic strain begins to rise from ∆𝑇 𝑗 = 15°C and then varies almost linearly with ∆𝑇 𝑗 . We can note that plastic strain is equivalent to elastic strain at about ∆𝑇 𝑗 = 30°C.

Since no strains are expected for ∆𝑇 𝑗 = 0°C, we can write a linear relationship between total strain per cycle and ∆𝑇 𝑗 :

∆𝜀 𝑡𝑜𝑡𝑎𝑙 ≈ 𝑘 ∆𝑇 𝑗 (7)
For a given ∆𝑇 𝑗 , it is expected that the inelastic strain ∆𝜀 𝑝𝑙 should be 𝑡 𝑜𝑛 dependent. Indeed, longer stress durations, i.e. higher 𝑡 𝑜𝑛 values, lead to shorter lifetimes, resulting in larger deformations per cycle. Thus, the coefficient k depends on the value of the parameter 𝑡 𝑜𝑛 . Since for 𝑡 𝑜𝑛 = 0, the coefficient k must itself be zero, the relationship between k and 𝑡 𝑜𝑛 , should be of the form : 𝑘 ≈ 𝛼 𝑡 𝑜𝑛 𝛽 [START_REF] Scheuermann | A new lifetime model for advanced power modules with sintered chips and optimized Al wire bonds[END_REF] From results given in tables VII and VIII, the value of k can be obtained for 𝑡 𝑜𝑛 = 3s and 20s : 𝑘 3𝑠 ≈ 3.6 × 10 -5 𝐾 -1 and 𝑘 20𝑠 ≈ 3.8 × 10 -5 𝐾 -1 . From these values, 𝛼 and 𝛽 parameters can be identified: 𝛼 = 3.18 × 10 -5 ; 𝛽 = 6.6 × 10 -2 Fig. 13: Dependence with junction temperature swing (∆𝑇 𝑗 ) of the elastic, plastic and total strain variation per cycle for 𝑡 𝑜𝑛 =3s condition.

IV. LIFETIME ESTIMATION AND EXTRAPOLATION FOR LOW ∆𝑇 𝑗

The relations (4) and ( 5) can be plotted and extrapolated in fig. 14 (red and blue dashed lines) as well as the total strain per cycle (6), i.e. the black dashed curve.

By using relation [START_REF] Bayerer | Model for power cycling lifetime of IGBT modules -various factors influencing lifetime[END_REF], it is possible to place in the black dashed curve any total strain with its corresponding ∆𝑇 𝑗 and so to extrapolate for low ∆𝑇 𝑗 values, see fig. 14. In this figure, it can be noticed that for low 𝑁 𝑓 cycles, with high ∆𝑇 𝑗 values, plastic strains are dominant leading to a Coffin-Manson's law behavior [START_REF] Manson | Thermal Stress Low-cycle Fatigue[END_REF] whereas for high 𝑁 𝑓 values, corresponding to low ∆𝑇 𝑗 values, elastic strains are dominant and Basquin's law fatigue takes place [START_REF] Joadder | Fatigue Failure of Notched Specimen -A Strain-Life Approach[END_REF][START_REF] Basquin | The Exponential Law of Endurance Tests[END_REF].

By eliminating ∆𝜀 𝑡𝑜𝑡𝑎𝑙 between ( 6) and ( 7) we have a nontrivial relationship between ∆𝑇 𝑗 and 𝑁 𝑓 :

∆𝑇 𝑗 = 𝐴. 𝑁 𝑓 -𝑎 + 𝐵. 𝑁 𝑓 -𝑏 𝛼 𝑡 𝑜𝑛 𝛽 (9)
The relation [START_REF] Drofenik | Multi-domain simulation of transient junction temperatures and resulting stress-strain behavior of power switches for long term mission profiles[END_REF] gives the lifetime model (𝑁 𝑓 ) with a dependence on the stresses, i.e. junction temperature variations (∆𝑇 𝑗 ) and heating duration (𝑡 𝑜𝑛 ). From, this relation it can be seen that if only low cycle fatigue domain is considered (high ∆𝑇 𝑗 ), only the Coffin-Manson law will be taken into account leading to typical empirical lifetime models as in [START_REF] Held | Fast power cycling test of IGBT modules in traction application[END_REF][START_REF] Bayerer | Model for power cycling lifetime of IGBT modules -various factors influencing lifetime[END_REF].

For validation purpose, the model thus obtained has been tested on some additional experimental points from [3] where the same power modules were tested in power cycling conditions with different 𝑡 𝑜𝑛 values. The results used here are related to the wire bond failure only. As already said above, the finite element model does not take into account the stress duration, the behavior laws used for aluminum being time-independent. So, even if this model was constructed on the basis of experimental results (𝑁 𝑓 ) and calculated strains for 𝑡 𝑜𝑛 = 3s, relation (6) combined with [START_REF] Bayerer | Model for power cycling lifetime of IGBT modules -various factors influencing lifetime[END_REF] makes it possible to obtain a model which, even referenced to 𝑡 𝑜𝑛 = 3s, gives valid results for a large scale of 𝑡 𝑜𝑛 values.

Finally, additional tests under low ∆𝑇 𝑗 conditions must still be performed to validate the model in normal operative stress conditions. The first one is a relation between thermal stresses (∆𝑇 𝑗 , 𝑡 𝑜𝑛 ) and strain, the second one is a relation between strain and lifetime. The first relation, issued from a numerical design of experiment, leads to a linear dependency of the strain with the thermal stress (∆𝑇 𝑗 ) and a power law dependency with the stress duration (𝑡 𝑜𝑛 ). The second one is obtained from both the combination of experimental lifetime results from accelerated power cycling tests and strains from numerical results in same conditions than in testing. This last relation takes into account both Coffin-Manson's law and Basquin's law leading to a capability for the model to predict lifetime in high cycle conditions, i.e. low thermal stresses. The model has been tested and satisfactorily validated using additional power cycling test conditions from literature. Additional tests under low ∆𝑇 𝑗 conditions must still be performed to validate the model in normal stress conditions.

Fig. 1 :

 1 Fig. 1: Substrate of SKIM63 power module from Semikron.

Fig. 2 :

 2 Fig. 2: Schematic power cycling test circuit.

Fig. 3 :

 3 Fig. 3: Example of evolution of relative variation in 𝑉 𝐶𝐸 during aging test.

Fig. 5 :

 5 Fig. 5: The whole geometrical model, only the central leg is stressed.

Fig. 6 :

 6 Fig. 6: Details of the geometrical model of the central substrate.

  𝑇 𝑗 ) = 4.75 × 10 -5 𝑇 𝑗 + 0.01394 𝑘 2 (𝑇 𝑗 ) = 1.99 × 10 -4 𝑇 𝑗 + 0.7453 𝑘 3 (𝑇 𝑗 ) = -1.57 × 10 -3 𝑇 𝑗 + 0.8069 (2)

Fig. 7 :

 7 Fig.7: Elasto-plastic stress-strain behaviors for aluminum and copper.

Fig. 8 :

 8 Fig. 8: Schematic load current cycles for numerical simulations.

Fig. 9 :

 9 Fig. 9: Temperature map (in °C) within the substrate (IL = 272 A, 𝑡 𝑜𝑛 =3s).

Fig. 10 :

 10 Fig.10: Plastic strain distribution at the end of a heating phase over the metallization layer of the high side IGBT (IL = 272A, 𝑡 𝑜𝑛 =3s).

Fig. 11 :

 11 Fig.11: Evolution over some cycles of junction temperature (upper graph), plastic strain (central graph) and elastic strain (lower graph).

Fig. 12 :

 12 Fig.12: Elastic and plastic strains dependence with lifetime

Fig. 14 :

 14 Fig.14: Total strain with lifetime and ∆𝑇 𝑗 dependence As results, all experimental 𝑁 𝑓 values are given in fig.15 with the dependence in ∆𝑇 𝑗 . Experimental results from this paper (black circles and black disks) added to those from [3] (colored triangles) are visible in this figure. All the dotted curves in this figure are obtained by the model for the different indicated 𝑡 𝑜𝑛 values. It can be seen that the model (eq.9) is a fairly satisfactory representation of the experimental results as well as the test points used for the validation.As already said above, the finite element model does not take into account the stress duration, the behavior laws used for aluminum being time-independent. So, even if this model was constructed on the basis of experimental results (𝑁 𝑓 ) and calculated strains for 𝑡 𝑜𝑛 = 3s, relation (6) combined with[START_REF] Bayerer | Model for power cycling lifetime of IGBT modules -various factors influencing lifetime[END_REF] makes it possible to obtain a model which, even referenced to 𝑡 𝑜𝑛 = 3s, gives valid results for a large scale of 𝑡 𝑜𝑛 values.Finally, additional tests under low ∆𝑇 𝑗 conditions must still be performed to validate the model in normal operative stress conditions.

Fig. 15 :

 15 Fig.15: Power cycling test results and lifetime model validation V. CONCLUSION A stress-based lifetime model for bond wire contacts of Insulated Gate Bipolar Transistors (IGBT) power modules has been presented in this paper. The model is based on the

  This article has been accepted for publication in a future issue of this journal, but has not been fully edited. Content may change prior to final publication. Citation information: DOI 10.1109/JESTPE.2019.2918941, IEEE Journal of Emerging and Selected Topics in Power Electronics

	Stress-based Model for Lifetime Estimation of
	Bond-Wire Contacts using Power Cycling Tests
	and Finite Element Modelling

N. Dornic, Z. Khatir, S-H. Tran, A. Ibrahim, R. Lallemand, J.P. Ousten, J. Ewanchuk, S. Mollov P 2168-6777 (c) 2019 IEEE. Personal use is permitted, but republication/redistribution requires IEEE permission. See http://www.ieee.org/publications_standards/publications/rights/index.html for more information. > REPLACE THIS LINE WITH YOUR PAPER IDENTIFICATION NUMBER (DOUBLE-CLICK HERE TO EDIT) < 2

TABLE I TEST

 I CONDITIONS AND POWER CYCLING RESULTS (𝑡 𝑜𝑛 =3S)∆𝑇 𝑗 (°C) 𝑇 𝑗𝑚𝑖𝑛 (°C)

			IL (A)	𝑁 𝑓 (kcycles)	𝑁 𝑓 mean value (kcycles)
	110	35	260	[74, 66, 78]	73
	90	35	240	[207, 182,173]	187
	70	35	210	[934, 739, 904]	860

TABLE II TEST

 II CONDITIONS AND POWER CYCLING RESULTS (𝑡 𝑜𝑛 =20S)

	∆𝑇 𝑗 (°C) 𝑇 𝑗𝑚𝑖𝑛 (°C)	IL (A)	𝑁 𝑓 (kcycles)	𝑁 𝑓 mean value (kcycles)
	110	35	230	[35, 40, 35]	37
	90	35	205	[96, 97, 95]	96
	70	35	185	[485, 482, -]	483

TABLE VI NUMERICAL

 VI EXPERIMENTAL DESIGN (𝑡 𝑜𝑛 =3S)

	∆𝑇 𝑗 (°C)	110	90	70	55	25	15
	𝐼 𝐿 (A)	272	256	225	189	122	80

TABLE VII ELASTIC

 VII AND PLASTIC VARIATION PER CYCLE (𝑡 𝑜𝑛 =3s)

	∆𝑇 𝑗 (°C)	Δ𝜀 𝑒𝑙	Δ𝜀 𝑝𝑙
	110	5.93 × 10 -4	3.17 × 10 -3
	90	5.78 × 10 -4	2.46 × 10 -3
	70	5.62 × 10 -4	1.81 × 10 -3

TABLE VIII ELASTIC

 VIII AND PLASTIC VARIATION PER CYCLE (𝑡 𝑜𝑛 =20s)

	∆𝑇 𝑗 (°C)	Δ𝜀 𝑒𝑙	Δ𝜀 𝑝𝑙

> REPLACE THIS LINE WITH YOUR PAPER IDENTIFICATION NUMBER (DOUBLE-CLICK HERE TO EDIT) <


Oussama Ennafii

Clément Mallet

Arnaud Le Bris

Florent Lafarge
email: florent.lafarge@inria.fr

The necessary yet complex evaluation of 3D city models: a semantic approach

Keywords: 3D, modeling, buildings, quality, taxonomy, classification, error detection, geometry, VHR data

The automatic modeling of urban scenes in 3D from geospatial data has been studied for more than thirty years. However, the output models still have to undergo a tedious task of correction at city scale. In this work, we propose an approach for automatically evaluating the quality of 3D building models. A taxonomy of potential errors is first proposed. Handcrafted features are computed, based on the geometric properties of buildings and, when available, Very High Resolution images and depth data. They are fed into a Random Forest classifier for the prediction of the quality of the models. We tested our framework on three distinct urban areas in France. We can satisfactorily detect, on average 96% of the most frequent errors.

I. INTRODUCTION

Although automatic 3D urban modeling has been extensively studied for many years by academics and industrials alike, current algorithms fail to adapt to different urban settings [START_REF] Musialski | A survey of urban reconstruction[END_REF]. Output building models still have to be inspected by human operators for quality assessment and subsequent correction. Thus, scalability is not handled in the literature albeit being critical in operational contexts. In this work, we study the automation of 3D building model evaluation. We focus on assessing polyhedral structured models. They represent building roof architectures, which result from a given urban reconstruction method, unknown here. Each facet of the model corresponds to an architectural (post of the time planar) feature. Such 3D models do not correspond to triangle meshes. The latter ones exhibit higher data fidelity but lower compacity and no semantics. Depending on the spatial resolution of input data, the urban scene, and the intended use, the reconstituted model has a certain Level of Detail (LoD) [START_REF] Kolbe | CityGML: Interoperable access to 3D city models[END_REF].

Few works have addressed the quality assessment of 3D urban models at building level. Usually, visual inspection [START_REF] Durupt | Automatic building reconstruction from a Digital Elevation Model and cadastral data: an operational approach[END_REF] or comparison with field measurements [START_REF] Kaartinen | Accuracy of 3d city models: Eurosdr comparison[END_REF] are performed, void of structural information. Our work focuses on semantically evaluating the structural compliance of modeled buildings. We define an evaluation framework that can be used for building model correction, change detection, reconstruction method selection, and crowdsourcing evaluation. We ignore format/geometric issues [START_REF] Ledoux | val3dity: validation of 3D GIS primitives according to the international standards[END_REF]. Our framework targets to be independent from the Level of Detail and the modeling method. Quality metrics can be provided with the reconstruction process but lack of independence with the underlying method. This work proposes an adaptable and flexible framework. It is indifferent to input urban scenes and reconstruction methods (Figure 1). For that purpose, our contributions are three-fold:

• A new taxonomy of errors, hierarchical, adapted to all LoD, and independent from input models; • A supervised classification formulation of the problem, which predicts all errors affecting the building model; • A multimodal baseline of features, which are extracted both from the model and external data (Very High Resolution optical images and height data). Section II introduces the problem of the evaluation of 3D building models and discusses existing methods. Section III details the proposed approach, while data and results of experiments conducted over three urban areas are presented in Section IV. Main conclusions are drawn in Section V.

II. RELATED WORK

3D urban models qualification has been barely investigated in the literature despite plethora of modeling approaches. Methods can be classified based on the assessment criteria: geometric fidelity indices or semantic errors. Geometric fidelity metrics quantify the modeling accuracy relying on the precision of points of interest (e.g., intersection points), of surfaces or on the 3D model volume. These are usually compared to higher resolution reference data [START_REF] Kaartinen | Accuracy of 3d city models: Eurosdr comparison[END_REF], [START_REF] Zeng | A multicriteria evaluation method for 3D building reconstruction[END_REF]. These metrics fail to describe local modeling defects. Consequently, semantic errors are preferred for such a task, often following the traffic light paradigm. For instance, four levels of quality are defined in [START_REF] Boudet | A supervised classification approach towards quality selfdiagnosis of 3D building models using digital aerial imagery[END_REF]: Correct, Acceptable, Generalized, and False. However, these levels are not explicitly quantified and are ill defined: they depends on the end-user. The error taxonomy can also adopt the modeling method perspective. Errors can be grouped into footprint ones (e.g., erroneous outline, missing inner court) and modeling errors (under/over-segmentation, height inaccuracy). These are therefore method-dependent. The building model is therefore assessed owing to a supervised classification that takes these defined errors as labels. In order to represent input models, features are extracted from aerial images or Digital Surface Model (DSM) at very high resolution (20 cm to 25 cm), by 3D segments comparisons or texture correlation ratios [START_REF] Boudet | A supervised classification approach towards quality selfdiagnosis of 3D building models using digital aerial imagery[END_REF], [START_REF] Michelin | Quality evaluation of 3D city building models with automatic error diagnosis[END_REF]. Despite satisfactory results, this approach exhibits two main drawbacks: a taxonomy specific to some urban scenes or modeling methods and a complex feature computation step, preventing upscaling strategies. The main idea of our work is to propose an agnostic assessment approach that do not rely on reference data and complex features.

III. METHODOLOGY

Our method relies on predicting errors in order to qualify a 3D model at the scale of a building. Errors are defined in a hierarchical taxonomy, based on the assessment objectives. Handcrafted features of various kinds are computed (Figure 1). A supervised classifier is trained using annotated building models and tested later on unseen buildings for quality prediction based on the detected errors. This pipeline is modular: it takes into account geometric features, coming from the 3D model, which can be augmented by height features, from the DSM, or optical features, from a VHR orthoimage.

A. Error taxonomy

Two criteria are taken into account so as to build a generic and flexible taxonomy (Figure 2): the LoD and the semantic level, which we call henceforth finesse. An atomic error is one with maximal finesse: it corresponds, intuitively, to a unitary action that an operator should take in order to correct a model.

From an operational perspective, not all buildings are qualifiable. For instance, buildings can be occluded by vegetation or happen to show self-intersection problems. These pathological cases are outside the realm of our assessment framework. Thus, in the finesse level equal to 0, we discriminate between Qualifiable and Unqualifiable models. At the next level, models are classified being Valid or Erroneous. Based on the LoD, these last models are distinguished into error families at finesse equal to 2. Building errors correspond to defects at the building level (LoD-1 ∪ LoD-0). Errors related to building facets (LoD-2) are assembled into Facet errors. The last family, Superstructure errors, groups errors pertaining to LoD-3 errors. These families contain atomic errors that have a maximal finesse equal to 3.

This error arrangement does not depend on a particular modeling method or urban environment. Labels are not redundant as atomic errors are chosen to be independent from each other. They represent a particular topological or geometric defect. Topological errors relate to structural defects in the model, while geometrical ones address modeling imprecision. We propose the following atomic errors based on our comprehensive analysis on overhead aerial models.

-Building errors family (Figure 3i):

• Under segmentation (BUS): two or more buildings are modeled as one;

B. Feature baseline

We propose a simple handcrafted set. We limit ourself to the validation of the semantic approach and taxonomy validation. We rely on three modalities. The first is the input 3D model. We extract statistics (maximum, minimum, mean, median and standard deviation) over attributes that describe the geometry of the building facets: number of nodes, area, angle between normals, distance between centroids and circumference. We add height attributes. These are represented by the histogram of the discrepancy between the rasterized model height map and the DSM at the same spatial resolution. It is chosen to be lower than building dimensions but higher than the modeling inherent planimetric uncertainty. Last comes optical features, computed by back-projecting the model on corresponding VHR orthoimage. For each facet edge, we compute

C. Classification process

The labels are organized into different classification problems. To account for the desired modularity and flexibility, a random forest classifier is chosen (1,000 trees, maximal depth of 4). The depth is kept shallow in order to avoid overfitting while the large number of estimators deals with the large feature space variability. The Multi-label setting is managed using a One vs All strategy on top of our classifier. We evaluate our approach on a dataset drawn from three French cities: Elancourt, Nantes and one district of Paris (Paris-13).

IV. EXPERIMENTS

Elancourt exhibits a high diversity of building types: residential areas (bilevel buildings) and industrial sections (flat roofs). Nantes represents a denser urban setting with lower diversity. In Paris-13, high towers coexist with Haussmann style buildings. Input 3D models were obtained using the algorithm described in [START_REF] Durupt | Automatic building reconstruction from a Digital Elevation Model and cadastral data: an operational approach[END_REF], out of existing footprints and an aerial VHR multi-view DSM. They were annotated according to the atomic errors list provided by our taxonomy. More details are reported in Table I. Labels are extracted from the taxonomy at finesse level of 3. In Table II, we report results over Elancourt using all four possible feature configurations performing a 10-fold cross validation. In Table III, we experimented training over buildings from one urban zone and testing on another.

From Table II, we can see that well represented errors are correctly detected. In fact, BOS (resp. FOS, FIB), with a 66.8% (resp. 64.16%, 59.08%) occurrence ratio, attains, in average across all configurations, a high recall ratio of 91.93% (resp. 98.93%, 79, 68%). In contrast, other atomic errors which are not frequently found in the dataset (a∼10% of the total) are naturally harder to detect. The ablation study reveals that, for most errors, geometric features yield sensibly the same results, except for BUS (where height and/or image based features add around 10% in recall while loosing at most 5% in precision), and for BImB (as image based features add around 4% in recall without a loss in precision). In Paris-13 and Nantes buildings are often more adjacent than Elancourt, this perfectly explains why classifiers trained over Paris/Nantes are better, regarding Building atomic errors, in recall and precision than the ones trained over Elancourt and tested on them. It achieves even close or better recall ratio over BimB if compared to classifiers trained on Elancourt itself. However, Facet atomic errors are much more easily detected if the classifiers are trained over Elancourt and tested on the other cities. It is also mostly stable compared to evaluation on Elancourt itself and even yields much better results for FIB and FIG. This can be explained by the fact that Haussmann style buildings and high flat towers offer less diverse facet geometries compared to bi-level hipped roofs, industrial buildings and other residential features that are present in the Elancourt scene.

Qualitative assessment is also performed in order to illustrate some failure cases. In the leftmost example of Figure 4, the similarity of the building outline to over segmented build- ings cases induces an overdetection. Sometimes, the VHR of the data does not suffice to detect all errors that are visually identifiable. In general, these samples help us devise more robust features so as to alleviate these issues. Dataset enrichment could be another option which provides more instances of underrepresented errors. In the end, we can also add the human in the loop through a manual interactive evaluation/classification mechanism which could adapt well to user-specific needs.

V. CONCLUSION

We proposed a framework to semantically evaluate 3D building models. Errors were hierarchically organized into a flexible and parametrizable taxonomy, handling the large diversity of urban environments and end users' requirements. Model quality was predicted using a supervised classifier using three modalities. Although being mitigated over underrepresented errors, results are satisfactory in the well balanced cases. As a next step, more structurally aware features (e.g., based on graph comparison) will be proposed, so as to be applied on a richer and more diverse dataset (potentially involving data augmentation) under a deep-based framework.

■

  Fidelity error. ■ Modeling error.

Fig. 1 :

 1 Fig. 1: The semantic evaluation paradigm proposal. Geometric structural features are first proposed (b), potentially augmented with attributes based on height map and color gradient com-parison (c-d). Semantic errors are eventually predicted using a pretrained classifier.

Fig. 2 :

 2 Fig.2:The proposed taxonomy structure. In the VHR overhead case, only two families of errors are depicted. At finesse level 2, a hierarchy exists and exclusivity may prevail.

  BInT i. Building errors family samples.

  FIG ii. Facet errors family samples.

Fig. 3 :

 3 Fig.3: Illustration of various errors of our taxonomy. One can see that geometric, spectral and height information are required for an accurate detection of all kinds of errors.

Fig. 4 :

 4 Fig. 4: Predicted (Pred.) errors compared to ground truth (G.T.) labels are illustrated in some pathological cases. Knowing how each error is represented in the dataset helps interpreting misclassifications.

TABLE I :

 I Dataset details.

TABLE II :

 II Ablation study (in %) at finesse = 3 on Elancourt.

		Elancourt → Nantes Recall Prec.	Elancourt → Paris-13 Recall Prec.	Nantes → Elancourt Recall Prec.	Paris-13 → Elancourt Recall Prec.
	BOS	100	42.05	78.71	42.97	86.47	64.99	82.14	69.59
	BUS	19.12	54.17	4.76	27.27	23.75	57.47	25.0	50.49
	BImB	0	-	1.85	33.33	15.65	46.75	19.89	48.05
	BInT	40.71	14.24	0	-	4.70	100	4.44	100
	FOS	100	69.38	98.80	96.47	98.76	98.92	99.06	97.14
	FUS	15.71	56.90	20.73	91.94	1.68	77.78	3.53	89.47
	FIB	83.54	43.08	39.58	64.04	23.75	73.96	21.86	70.11
	FIT	9.09	33.33	0	0	3.57	100	4.34	33.33
	FIG	100	64.45	90.86	86.14	86.35	67.97	82.38	73.08

TABLE III :

 III

	Errors	G.T.	Pred.	Errors	G.T.	Pred.	Errors	G.T.	Pred.	Errors	G.T.	Pred.
	BOS			BUS			BOS			BOS
	Valid			FIG			FUS			FOS
				FOS						BUS
										BImB

Transferability study (in %) at finesse = 3 over different urban scenes using all features. Compared to previous results in Table

II

, : a stable or better result, : a small drop and : a significant decrease in accuracy.

978-1-7281-0009-8/19/$31.00 ©2019 IEEE


Pierre Lermusiaux

Horatiu Cirstea

Pierre-Etienne Moreau

Pattern eliminating transformations

Program transformation is a common practice in computer science, and its many applications can have a range of dierent objectives. For example, a program written in an original high level language could be either translated into machine code for execution purposes, or towards a language suitable for formal verication. Languages often have a lot of dierent constructions, and thus, transformations often focus on eliminating some of these constructions, or at least processing some specic sequence of constructions. Rewriting is a widely established formalism to describe the mechanism and the logic behind such transformations. It relies mainly on the principle of rewrite rules to describe the dierent operations performed. Generally type-preserving, these rewrite rules can ensure that the transformation result has a given type and thus give syntactic guarantees on the constructions it consists of. However, we sometimes want the transformation to provide more guarantees on the shape of its result by specifying that some patterns of constructions does not appear. For this purpose, we propose in this paper an approach based on annotating transformation function symbols with (anti-)pattern in order for such transformation to guarantee stronger properties on the shape of its result. With the generic principles governing term algebra and rewriting, we believe this approach to be an accurate formalism to any language providing pattern-matching primitives.

Introduction

Rewriting is a widely established formalism for a number of applications in both computer science and mathematics and has been used, in particular, to describe program semantics [START_REF] Rosu | An overview of the K semantic framework[END_REF] and transformations [START_REF] Lacey | Imperative program transformation by rewriting[END_REF][START_REF] Bellegarde | Program transformation and rewriting[END_REF]. In general, compilation consists in several phases, also called passes, eventually obtaining a program in a dierent target language. These phases use some corresponding intermediate languages which generally contain less and less constructions of the original language.

Consider, for example, a very simple language allowing to express some form of λ-expressions: A rst step in the compilation of such expressions is to eliminate the Let constructor using the rewrite rule Let(name, e 1 , e 2 ) Apply(Lambda(name, e 2 ), e 1 ) to obtain pure λ-expressions.

The goal is to provide a formalism allowing to describe such transformations and to guarantee that some language constructs are eliminated by these transformations.

Existing works addressed this problem from dierent perspectives. In particular, a number of approaches rely on the use of automata to implement transformation. Such approach is particularly relevent as the input and output of the transformation can be viewed as a regular language [START_REF] Alur | Streaming transducers for algorithmic verication of single-pass list-processing programs[END_REF] or a tree [START_REF] Bahr | Programming macro tree transducers[END_REF]. While this approach focus on the decidability and complexity of some specic cases it does not handle the general problems we target here. Functionnal approaches to transformation [START_REF] Pottier | Visitors unchained[END_REF] focus on the simplicity and expressiveness of the formalism more than on verifying the elimination of constructs. This verication can be performed by using ne grained typing systems which combine overloading, subtyping and polymorphism through the use of variants [START_REF] Garrigue | Programming with polymorphic variants[END_REF] but is somewhat limited w.r.t. the type of constructs which can be eliminated.

We use rewriting to dene such transformations and annotate the function symbols in order to check that the associated transformation veries the desired elimination properties.

First, in the next section, we will introduce all the notions and notations used in the article. We will then, in the following section, give a formal denition to the property we want pattern eliminating transformation to guarantee: pattern-freeness. The 2 subsequent sections will be focused respectively on introducing a method to reliably verify such properties and on studying how they can be guaranteed by the considered transformations, using and extending notions of pattern semantics introduced in the notions of the next section.

Pattern matching and term rewriting systems

We dene in this section the basic notions and notations used in this paper; more details can be found in [START_REF] Baader | Term Rewriting and All That[END_REF][START_REF]Term Rewriting Systems[END_REF].

A many-sorted signature Σ = (S, F), consists of a set of sorts S and a set of symbols F.

We distinguish constructors symbols from functions symbols by partitioning the alphabet F into D, the set of dened symbols, and C the set of constructors. A symbol f with domain Dom (f ) = s 1 × . . . ×s n ∈ S * and co-domain

CoDom (f ) = s ∈ S is written f : s 1 × . . . ×s n → s.
Variables are also sorted and we write x : s or x s to indicate that variable x has sort s. The set X s denotes a set of variables of sort s and X = s∈S X s is the set of sorted variables. The set of terms of sort s ∈ S, denoted T s (F, X ) is the smallest set containing X s and such that

f (t 1 , . . . , t n ) is in T s (F, X ) whenever f : s 1 × . . . ×s n → s and t i ∈ T si (F, X ) for i ∈ [1, n].
We write t : s when the term t is of sort s, i.e. when t ∈ T s (F, X ). The set of sorted terms is dened as T (F, X ) = s∈S T s (F, X ). The set of variables occurring in t ∈ T (F, X ) is denoted by Var (t). If Var (t) is empty, t is called a ground term. T s (F) denotes the set of all ground rst-order terms of sort s and T (F) denotes the set of all ground rst-order terms, while members of T (C) are called values. A linear term is a term where every variable occurs at most once, and linear terms in T (C, X ) are called patterns.

A position of a term t is a nite sequence of positive integers describing the path from the root of t to the root of the sub-term at that position. The empty sequence representing the root position is denoted by ε. t |ω denotes the sub-term of t at position ω and t [s] ω denotes the term t with the sub-term at position ω replaced by s. We note Pos (t) the set of positions of t.

We call substitution any mapping from X to T (F, X ) which is the identity except over a nite set of variables called its domain; any substitution extends as expected to an endomorphism of T (F, X ). Given a sort s, a value v : s and a constructor pattern p, we say that p matches v

(denoted p ≺ ≺ v) if there exists a substitution σ such that v = σ(p). A constructor rewrite rule is of the form ϕ(l 1 , . . . , l n ) r ∈ T s (F, X ) × T s (F, X ) with s ∈ S, ϕ ∈ D, l 1 , . . . , l n ∈ T (C, X )
and such that Var (r) ⊆ Var (l). A constructor term rewriting system (CTRS) is a set of rewrite rules R inducing a rewriting relation over T (F), denoted by -→ R and such that t -→ R t i there exist l r ∈ R, ω ∈ Pos (t), and a substitution σ such that

t |ω = σ(l) and t = t [σ(r)] ω .
Starting from the observation that a pattern can be interpreted as the set of its instances, the notion of ground semantics was introduced in [START_REF] Cirstea | Generic encodings of constructor rewriting systems[END_REF] as the set of all ground constructor instances of a pattern p ∈ T s (C, X ):

p = {σ(p) | σ(p) ∈ T s (C)}. Proposition 1. Given a pattern p and a value v, v ∈ p i v = σ(p).
Note that the ground semantics of a variable x s is the set of all possible ground patterns:

x s = T s (C), and since patterns are linear we can use a recursive denition for the non variable patterns:

c(p 1 , . . . , p n ) = {c(t 1 , . . . , t n ) | (t 1 , . . . , t n ) ∈ p 1 × . . . × p n }, ∀c ∈ C. Moreover x s = {c(t 1 , . . . , t n ) | c ∈ C s.t. c : s 1 × . . . ×s n → s ∧ ∀i, t i ∈ x si } = c∈Cs c(x 1 , . . . , x n ) .
We consider also a special pattern ⊥ with ⊥ = ∅. Given two patterns p, q we can compute [START_REF] Cirstea | Generic encodings of constructor rewriting systems[END_REF] their complement p \ q, i.e. a set p 1 , . . . , p n of patterns s.t. p \ q = p 1 , . . . , p n .

Pattern free terms

The sort provides some information on the shape of the terms of the respective sort and in particular allows one to check if a given symbol may be present or not in these terms. In fact, the precise language of the values of a given sort is implicitly given by the signature. Sorts are less informative concerning the shape of the values obtained when reducing terms containing dened symbols since they strongly depend on the CTRS dening these symbols.

We want to ensure that the normal form of a term, if it exists, does not contain a constructor and more generally that no subterm of this normal form matches a given pattern. For this we annotate all dened symbols with the patterns that are supposed to be absent from the normal form and we check that the CTRS dening the corresponding functions are consistent with these annotations. We will see later on how this consistence can be veried and we focus rst on the notion of pattern-free term and the corresponding ground semantics.

We consider that every dened symbol f ∈ D is annotated with a pattern p ∈ T (C, X ) ∪ {⊥} and we use this notation to dene pattern-free terms. Intuitively, a term of the form f -p (t 1 , . . . , t n ) should ultimately be reduced to a value containing no subterms matched by p.

Denition 3.1 (Pattern-free). Given a pattern

p ∈ T (C, X ) ∪ {⊥}, • a value v ∈ T (C) is p-free i ∀ω ∈ Pos (v) , p ≺ ≺ v |ω ; • a ground term t ∈ T (F) is p-free i ∀ω ∈ Pos (t) such that t |ω = f -q (t 1 , . . . , t n ) with f ∈ D, q ∈ T (C, X ) ∪ {⊥}, CoDom (f ) = s, we have ∀v ∈ T s (C) q-free, t [v] ω is p-free; • a linear term t ∈ T (F, X ) is p-free i ∀σ such that σ(t) ∈ T (F), σ(t) is p-free.
A value is p-free if and only if p matches no subterm of the value. A ground term is p-free if and only if replacing (all) the subterms headed by a dened symbol f -q by any appropriate q-free value results in a p-free term. For general terms verifying the pattern-freeness comes to verifying the property for all ground instances of the term. While the pattern-freeness of a value can be checked by exploring all its subterms this is not possible for a general term since we potentially have to check the pattern-freeness of an innite number of values. We present in the next section an approach for solving this problem.

Extensions of ground semantics

The previously introduced ground semantics can be used to compare the shape of the root of a constructor pattern p 1 to another constructor pattern p 2 . Indeed, by denition, if

p 1 ∩ p 2 = ∅, then ∀σ, σ(p 1 ) / ∈ p 2 so p 2 ≺ ≺ σ(p 1 ).
Example 4.1. Consider the signature Σ with S = {s 1 , s 2 } and

F = C = {c 1 : s 2 , s 1 → s 1 , c 2 : s 2 → s 1 , c 3 : [] → s 1 , c 4 : s 2 → s 2 , c 5 : s 1 → s 2 }.
Using the transformation method proposed in [START_REF] Cirstea | Generic encodings of constructor rewriting systems[END_REF] the complement c4(c3()

) \ c4(x) is reduced to ⊥ indicating that c4(c3()) \ c4(x) = c4(c3()) \ c4(x) = ∅ and thus that c4(c3()) is redundant w.r.t. c4(x). Moreover c4(c3()) \ (c4(c3()) \ c4(x)
) is reduced to c4(c3()) \ ⊥ and then to c4(c3()) indicating now that c4(c3()) ∩ c4(x) = ∅ and thus that c4(c3()) is not c4(x) free. Similarly, c4(c3()) \ (c4(c3()) \ c5(x)) and c3() \ (c3() \ c5(x)) are both reduced to ⊥ and consequently we can deduce that c4(c3()) is c5(x)-free.

The pattern-freeness properties in the above example could have been checked by trying to match all the subterms and we can see this method as a starting point for the generalisation to general terms. We rst introduce an extended ground semantics: Denition 4.1 (Extended ground semantics). Given s ∈ S and a pattern p ∈ T (C, X ) ∪ {⊥}

• x s -p = {v | v ∈ T s (C) ∧ v p-free}; • f -p (t 1 , . . . , t n ) = x s -p with CoDom (f ) = s; • c(t 1 , . . . , t n ) = c(v 1 , . . . , v n ) | v i ∈ t i with c : s 1 × . . . ×s n → s ∈ C, t i ∈ T si (F, X ).
The ground semantics of a term rooted by a dened symbol represents an over-approximation of all the possible values obtained by reducing the term with respect to a TRS preserving the pattern-freeness, this by taking into account the annotation of the respective dened symbol. When restricting to patterns we retrieve the original denition of ground semantics.

The extended ground semantics of a p-free variable of sort s can be also dened as:

x s -p = c∈Cs c(x s1 -p , . . . , x si -p ) \ p
and when p = ⊥ we retrieve the corresponding denition for the classical ground semantics. This observation allows us to easily adapt the method introduced in [START_REF] Cirstea | Generic encodings of constructor rewriting systems[END_REF] for computing constructor pattern complements to general annotated terms.

We can now establish pattern-free properties using this extended ground semantics and the reachable sorts w.r.t. a given sort s:

s = {s | ∃ t ∈ T s (C), ω ∈ Pos (t) s.t. t |ω : s } Proposition 2 (Pattern-free vs Extended Ground Semantics). Let p ∈ T (C, X ), t ∈ T s (F, X ): • if t = x s and ∀s ∈ s , x s ⊥ ∩ p = ∅ then t is p-free; • if t = f -q (t 1 , . . . , t n ) and ∀s ∈ s , x s -q ∩ p = ∅ then t is p-free; • If t = c(t 1 , . . . , t n ) with c ∈ C, t is p-free i t ∩ p = ∅ and ∀i ∈ [1, n], t i is p-free.
The extended semantics of annotated terms together with the corresponding transformation of complement patterns (corresponding to semantics intersections) into sets of constructor patterns over-approximating their semantics allows us to systematically check if a term is pattern-free. Unfortunately equivalent extended semantics do not guarantee the preservation of pattern-freeness: having u = v and u p-free does not necessarily mean that v is p-free.

We introduce the notion of deep semantics of a term t ∈ T (F, X ), denoted {[t] }, which can be seen as an over-approximation of the set of all subterms of all values of its ground semantics, i.e.

{u |ω | u ∈ t , ω ∈ Pos (u)} ⊆ {[t] }: Denition 4.2. Given the sorts s 1 , . . . , s n , s ∈ S and a pattern p ∈ T (C, X ) ∪ {⊥} • {[x s -p ] } = s ∈ s x s -p ; • {[f -p (t 1 , . . . , t n )] } = s ∈ s x s -p with f : s 1 × . . . ×s n → s ∈ D; • {[c(t 1 , . . . , t n )] } = c(t 1 , . . . , t n ) ∪ n i=1 {[t i ] } with c : s 1 × . . . ×s n → s ∈ C.
The deep semantics of a variable must not only take into account its own sort, but also the sorts of all the subterms of its instances. Similarly, for terms headed by a constructor we consider the semantics of terms and of all its subterms.

We can now identify terms that have such a shape that a given pattern p does not appear in any of their ground instances. In other words, we have an alternative method for establishing pattern-free properties for linear terms in T (F, X ):

Proposition 3 (Pattern-free vs Deep Semantics). Let p ∈ T (C, X ), t ∈ T (F, X ), if {[t] }∩ p = ∅ then t is p-free.
Example 4.2. Let's consider the signature from Example 4.1: We add dened symbols D = {f : s 1 → s 1 , g : s 2 → s 2 } such that f is supposed to eliminate the p 1 = c 1 (c 4 (x), y) and g eliminates p 2 = c 4 (x). We therefore have the following constructor TRS:

f (c 1 (c 4 (x), y)) c 1 (g(x), f (y)) f (c 1 (c 5 (x), y)) c 1 (c 5 (f (x)), f (y)) f (c 2 (c 4 (x))) c 2 (c 4 (g(x))) f (c 2 (c 5 (x))) c 2 (c 5 (f (x))) f (c 3 ()) c 3 () g(c 4 (x)) c 5 (c 1 (g(x), c 3 ()))
g(c 5 (c 1 (x, y))) c 5 (c 1 (g(x), g(c 5 (y))))

g(c 5 (c 2 (x))) c 5 (c 2 (g(x))) g(c 5 (c 3 ())) c 5 (c 3 ())
Let's consider the term c 1 (g -p2 (x), f -p1 (y)). f -p1 (y) and g -p2 (x) have respectively the same semantics has y s1 -p1 and x s2 -p2 . Therefore the deep semantics of the whole term is the union of the ground semantics of c 1 (x s2 -p2 , y s1 -p1 ), y s1 -p1 , x s2 -p1 , y s1 -p2 and x s2 -p2 . Similarily as in Example 4.1, we can thus compare c 1 (x s2 -p2 , y s1 -p1 ) to p 1 and prove that it is p 1 -free.

Semantics preservation for CTRS

Pattern-freeness properties rely on the symbol annotations and assume thus a specic shape for the normal forms of reducible terms. This assumption should be checked by verifying that the CTRSs dening the annotated symbols are consistent with these annotations, i.e. verifying that the semantics is preserved by reduction. Denition 5.1 (Semantics preservation). A constructor rewrite rule ϕ -p (l 1 , . . . , l n ) r is semantics preserving w.r.t. the extended semantics, resp. deep semantics, i r ⊆ l , resp. {[r] } ⊆ {[l] }. A CTRS is semantics preserving i all its rewrites rules are.

Since the semantics of the left-hand side of a rewrite rule is the set of p-free values then such a rule is semantics preserving i its right-hand side is p-free. It is easy to check that: Proposition 4 (Semantics preservation). Given a semantics preserving CTRS R we have that then, ∀t, u ∈ T (F): We want each of the rules of the constructor TRS to be pattern-free preserving, so that for all v 1 ∈ T s1 (C), f (v 1 ) is and stays c 1 (c 4 (x), y)-free through every reduction step, and for all v 2 ∈ T s2 (C), g(v 2 ) is and stays c 4 (x)-free through every reduction step.

t -→ R u =⇒ {[u] } ⊆ {[t] } Example
In terms of pattern-free preservation we have: Proposition 5 (Pattern-free preservation). Given a semantics preserving CTRS R we have that ∀t, u ∈ T (F), p ∈ T (C, X ): t p-free ∧ t -→ R u =⇒ u p-free

Conclusion and perspectives

We have proposed a method to statically analyse constructor term rewrite systems and verify the absence of patterns from the corresponding normal forms. We can thus guarantee not only that some constructors are not present in the normal forms but we can also be more specic and verify that more complex constructs cannot be retrieved in the result of the reduction.

We suppose the existence of normal forms but the formalism does not rely on the termination of the analysed rewriting systems; if the property is not veried a nal value is not obtained but the intermediate terms in the innite reduction verify nevertheless the pattern-freeness properties w.r.t. the specied annotations. Moreover, dierent termination techniques and tools [START_REF] Giesl | Automated termination proofs for Haskell by term rewriting[END_REF][START_REF] Krauss | Termination of Isabelle functions via termination of rewriting[END_REF] on termination analysis can be used to analyse the termination of the rewriting systems we addressed in this paper.

We believe this formalism opens a lot of opportunities for further developments. In particular, this method could be extended in the context of automatic rewriting rule generation techniques, such as the one introduced in [START_REF] Cirstea | A faithful encoding of programmable strategies into term rewriting systems[END_REF], in order to implement transformation approaches of passes such as in [START_REF] Keep | A nanopass framework for commercial compiler development[END_REF]. Indeed, the formalism considered here relies on the same pattern matching primitives as these techniques.

  Expr = V ar(String) | Apply(Expr, Expr) | Lambda(String, Expr) | Let(String, Expr, Expr)

5 . 1 .

 51 Let's consider the case presented in Example 4.2: