Embedding artificial intelligence onto low-power devices is a challenging task that has been partially overcome by recent advances in machine learning and hardware design. Currently, deep neural networks can be deployed on embedded targets to perform various tasks such as speech recognition, object detection or human activity recognition. However, it is still possible to optimize deep neural networks on embedded devices. These optimizations mainly concern energy consumption, memory and real-time constraints, but also easier deployment at the edge. In addition, there is still a need for a better understanding of what can be achieved for different use cases. This work focuses on the quantization and deployment of deep neural networks on low-power 32-bit micro-controllers. In this article, the quantization method used is based on solving an integer optimization problem derived from the neural network model and concerning the accuracy of the computations and results at each point of the network. We evaluate the performance of our quantization method on a collection of neural networks measuring the analysis time and time-to-solution improvement between the floating- and fixed-point networks, considering a typical embedded platform employing a STM32 Nucleo-144 microcontroller.

In this article, we present a new method for implementing a neural network whose weights are floating-point numbers on a fixed-point architecture. The originality of our approach is that fixed-point formats are computed by solving an integer optimization problem derived from the neural network model and concerning the accuracy of computations and results at each point of the network. Therefore, we can bound mathematically the error between the results returned by the floating-point and fixed-point versions of the network. In addition to a formal description of our method, we describe a prototype that implements it. Our tool accepts the most common neural network layers (fully connected, convolutional, max-pooling, etc.), uses an optimizing SMT solver to compute fixed-point formats and synthesizes fixed-point C code from the Tensorflow model of the network. Experimental results show that our tool is able to achieve performance while keeping the relative numerical error below the given tolerance threshold. Furthermore, the results show that our fixed-point synthesized neural networks consume less time and energy when considering a typical embedded platform using an STM32 Nucleo-144 board.

Over the past few years, neural networks have started penetrating safety critical systems to make decisions as, for example, in robots, rockets, and autonomous driving cars. Neural networks based on floating-point arithmetic are very time and memory consuming, which are not compatible with embedded systems known to have limited resources. They are also very sensitive to the precision in which they have been trained, so changing this precision generally degrades the quality of their answers. To deal with that, we introduce a new technique to generate a fixed-point code for a trained neural network. This technique is based on fixed-point arithmetic with mixed-precision. This arithmetic is based on integer operations only, which are compatible with small memory devices. The obtained neural network has the same behavior as the initial one (based on the floating-point arithmetic) up to an error threshold defined by the user. The experimental results show the efficiency of our tool SyFix in terms of memory saved and the accuracy of the computations.

The implementation of control algorithms typically starts with the development of executable models and prototype implementations, e.g. in C, running on desktop computers before being ported to the target embedded architecture. Often, this latter architecture uses fixed-point arithmetic that differs in terms of accuracy from the floating-point arithmetic used by the desktop computer. In this article, we show that our POPiX tool is capable of automatically transforming floating-point codes into fixed-point ones while preserving the functional properties of the original control algorithms and optimizing resources in terms of memory and power consumption. We experiment POPiX on two widely used algorithms: a PID controller and a Kalman filter. Our experimental results validate, at the functional level, the code generation performed automatically by POPiX.

Frugal computing is becoming an important topic for environmental reasons. In this context, several techniques have been proposed to reduce the storage of scientific data by dedicated compression methods specially tailored for arrays of floating-point numbers. While these techniques are quite efficient to save memory, they introduce additional computations to compress and decompress data before processing them. In this article, we introduce a new lossy, fixed-rate compression technique for 2D-arrays of floating-point numbers which allows one to compute directly on the compressed data, without decompressing them. We obtain important speedups since less operations are needed to compute among the compressed data and since no decompression and re-compression is needed. More precisely, our technique makes it possible to perform basic linear algebra operations such as addition, multiplication by a constant among compressed matrices and dot product and matrix multiplication among partly uncompressed matrices. This work has been implemented into a tool named blaz and we present a comparison with the well-known compressor zfp in terms of execution-time and accuracy.

Precision tuning or customized precision number representations is emerging, in these recent years, as one of the most promising techniques that make it possible to save the resources on the available processors. In contrast to the uni-form precision, mixed precision tuning assigns different finite-precision types to each variable and arithmetic operation of a program and offers many additional optimization opportunities. However, this technique introduces new challenge related to the cost of operations or type conversions which can overload the program execution after tuning. In this article, we extend our tool POP, with efficient ways to limit the number of drawbacks of mixed precision and to achieve best compromise between performance and memory consumption. The results of our evaluation are discussed on a well-known set of tests from the FPBench suite.

In this article, we introduce a new method for computing fixed points of a class of iterated functions in a finite time, by exponentiating linear multivalued operators. To better illustrate this approach and show that our method can give fast and accurate results, we have chosen two well-known applications which are difficult to handle by usual techniques. First, we apply the exponentiation of linear operators to a digital filter in order to get a fine approximation of its behavior at an arbitrary time. Second, we consider a PID controller. To get a reliable estimate of its control function, we apply the exponentiation of a bundle of linear operators. Note that, our technique can be applied in a more general setting, i.e. for any multivalued linear map and that the general method is also introduced in this article.

The floating-point numbers used in computer programs are a finite approximation of real numbers. In practice, this approximation may introduce round-off errors and this can lead to catastrophic results. In previous work, we have proposed intraprocedural and interprocedural program transformations for numerical accuracy optimization. All these transformations have been implemented in our tool, Salsa. The experimental results applied on various programs either coming from embedded systems or numerical methods, show the efficiency of the transformation in terms of numerical accuracy improvement but also in terms of other criteria such as execution time and code size. This article studies the impact of program transformations for numerical accuracy specially in embedded systems on other efficiency parameters such as execution time, code size and accuracy of the other variables (these which are not chosen for optimization).

Floating-point numbers are used to approximate the exact real numbers in a wide range of domains like numerical simulations, embedded software, etc. However, floating-point numbers are a finite approximation of real numbers. In practice, this approximation may introduce round-off errors and this can lead to catastrophic results. To cope with this issue, we have developed a tool which corrects partly these round-off errors and which consequently improves the numerical accuracy of computations by automatically transforming programs in a source to source manner. Our transformation, relies on static analysis by abstract interpretation and operates on pieces of code with assignments, conditionals and loops. In former work, we have focused on the intraprocedural transformation of programs and, in this article, we introduce the interprocedural transformation to improve accuracy.

Summary Numerical programs with IEEE 754 floating‐point computations may suffer from inaccuracies because finite precision arithmetic is an approximation of real arithmetic. Solutions that reduce the loss of accuracy are available, such as compensated algorithms or double‐double precision floating‐point arithmetic. Our goal is to automatically improve the numerical quality of a numerical program with the smallest impact on its performance. We define and implement source code transformations in order to derive automatically compensated programs. We present several experimental results to compare the transformed programs and existing solutions. The transformed programs are as accurate and efficient as the implementations of compensated algorithms when the latter exist. Furthermore, we propose some transformation strategies allowing us to partially improve the accuracy of programs and to tune the impact on execution time. Trade‐offs between accuracy and performance are assured by code synthesis. Experimental results show that user‐defined trade‐offs are achievable in a reasonable amount of time, with the help of the tools we present in the paper. Copyright © 2016 John Wiley & Sons, Ltd.

In floating-point arithmetic, a desirable property of computations is to be accurate, since in many industrial context small or large perturbations due to round-off errors may cause considerable damages. To cope with this matter of fact, we have developed a tool which corrects these errors by automatically transforming programs in a source to source manner. Our transformation, relying on static analysis by abstract abstraction, concerns pieces of code with assignments, conditionals and loops. By transforming programs, we can significantly optimize the numerical accuracy of computations by minimizing the error relatively to the exact result. An interesting side-effect of our technique is that more accurate computations may make it possible to use smaller data-types. In this article, we show that our transformed programs, executed in single precision, may compete with not transformed codes executed in double precision.

Many critical embedded systems perform floating-point computations yet their accuracy is difficult to assert and strongly depends on how formulas are written in programs. In this article, we focus on the synthesis of accurate formulas mathematically equal to the original formulas occurring in source codes. In general, an expression may be rewritten in many ways. To avoid any combinatorial explosion, we use an intermediate representation, called APEG, enabling us to represent many equivalent expressions in the same structure. In this article, we specifically address the problem of selecting an accurate formula among all the expressions of an APEG. To validate our approach, we present experimental results showing how APEGs, combined with profitability analysis, make it possible to significantly improve the accuracy of floating-point computations.

This article introduces a new program transformation in order to enhance the numerical accuracy of floating-point computations. We consider that a program would return an exact result if the computations were carried out using real numbers. In practice, roundoff errors due to the finite representation of values arise during the execution. These errors are closely related to the way formulas are evaluated. Indeed, mathematically equivalent formulas, obtained using laws like associativity, distributivity, etc., may lead to very different numerical results in the computer arithmetic. We propose a semantics-based transformation in order to optimize the numerical accuracy of programs. This transformation is expressed in the abstract interpretation framework and it aims at rewriting pieces of numerical codes in order to obtain results closer to what the computer would output if it used the exact arithmetic.

Digital Signal Processors are widely used in critical embedded systems to pilot low-level, often critical functionalities. We describe a static analyzer based on abstract interpretation and designed to validate industrial assembler programs for a DSP. The validation consists of guaranteeing the absence of runtime errors such as incorrect memory accesses and of tracking the sources of inaccuracies introduced by floating-point computations. Our first contribution is a new static analysis for relocatable assembler programs able to cope with dynamically computed branching addresses. Our second contribution is the analyzer itself and its graphical interface which helps the user to understand the numerical inaccuracies.

In this paper, we are interested in self-applicable partial evaluation for the pi-calculus, a language which models the concurrent behavior of communicating processes. We use the classic three-steps methodology. First, we write a meta-interpreter for the language. Second, we introduce an abstract analysis that determines which operations (communications) can be executed at compile-time. The notion of well-annotatedness of terms is defined. Finally, we exhibit the self-applicable partial evaluator which is applied to well-annotated terms, and we prove its correctness with respect to the interpreter. This approach is compatible with Futamura's projections. Proofs of correctness are baaed on the notion of weak reduction equivalence.