International audience

Abstract Petri nets constitute a well-studied model to verify and study concurrent systems, among others, and computing the coverability set is one of the most fundamental problems about Petri nets. Using the proof assistant Coq, we certified the correctness and termination of the MinCov algorithm by Finkel, Haddad, and Khmelnitsky (FOSSACS 2020). This algorithm is the most recent algorithm in the literature that computes the minimal basis of the coverability set, a problem known to be prone to subtle bugs. Apart from the intrinsic interest of a computer-checked proof, our certification provides new insights on the MinCov algorithm. In particular, we introduce as an intermediate algorithm a small-step variant of MinCov of independent interest.

Dot products (also called sums of products) are ubiquitous in matrix computations, for instance in signal processing. We are especially interested in digital filters, where they are the core operation. We therefore focus on fixed-point arithmetic, used in embedded systems for time and energy efficiency. Common dot product algorithms ensure faithful rounding. For the sake of accuracy and reproducibility, we want to ensure correct rounding. This article describes an algorithm that computes a correctly-rounded sum of products from inputs whose format is known in advance. This algorithm relies on odd rounding (that is easily implemented in hardware) and comes with a careful proof and some cost analysis.

In this paper we target the Fixed-Point (FxP) implementation of Linear Time-Invariant (LTI) filters evaluated with statespace equations. We assume that wordlengths are fixed and that our goal is to determine binary point positions that guarantee the absence of overflows while maximizing accuracy. We provide a model for the worst-case error analysis of FxP filters that gives tight bounds on the output error. Then we develop an algorithm for the determination of binary point positions that takes rounding errors and their amplification fully into account. The proposed techniques are rigorous, i.e., based on proofs, and no simulations are ever used. In practice, Floating-Point (FP) errors that occur in the implementation of FxP design routines can lead to overestimation/underestimation of resulting parameters. Thus, along with FxP analysis of digital filters, we provide FP analysis of our filter design algorithms. In particular, the core measure in our approach, Worst-Case Peak Gain, is defined as an infinite sum and has matrix powers in it. We provide fine-grained FP error analysis of its evaluation and develop multiple precision algorithms that dynamically adapt their internal precision to satisfy an a priori absolute error bound. Our techniques on multiple precision matrix algorithms, such as eigendecomposition, are of independent interest as a contribution to Computer Arithmetic. All algorithms are implemented as C libraries, integrated into an open-source filter code generator and tested on numerical examples.

This article presents a word-length optimization problem under accuracy constraints for the hardware implementation of linear signal processing systems with fixed-point arithmetic. For State-Space systems (describing a linear filter or a controller), a complete error analysis is exhibited, where the final output error bound depends on the word-lengths and the fixed-point formats chosen for each variable. The Most Significant Bit of each one can be determined in order to guarantee that no overflow occurs. Thus, it is possible to obtain a hardware implementation minimizing resource use. This leads to a convex nonlinear integer optimization problem where the resources to minimize and the accuracy constraints depend on the internal word-lengths. This problem can then be solved with appropriate heuristics. Finally, a global approach is proposed and illustrated by some examples.

Linear Time Invariant (LTI) filters are often specified and simulated using high-precision software, before being implemented in low-precision fixed-point hardware. A problem is that the hardware does not behave exactly as the simulation due to quantization and rounding issues. This article advocates the construction of LTI architectures that behave as if the computation was performed with infinite accuracy, then converted to the low-precision output format with an error smaller than its least significant bit. This simple specification guarantees the numerical quality of the hardware, even for critical LTI systems. Besides, it is possible to derive the optimal values of all the internal data formats that ensure that the specification is met. This requires a detailed error analysis that captures not only the quantization and rounding errors, but also their infinite accumulation in recursive filters. This generic methodology is detailed for the case of low-precision LTI filters in the Direct Form I implemented in FPGA logic. It is demonstrated by a fully automated and open-source architecture generator tool, and validated on a range of Infinite Impulse Response filters.

Reliable implementation of digital filters in finiteprecision is based on accurate error analysis. However, a small error in the time domain does not guarantee that the implemented filter verifies the initial band specifications in the frequency domain. We propose a novel certified algorithm for the verification of a filter's transfer function, or of an existing finite-precision implementation. We show that this problem boils down to the verification of bounds on a rational function, and further to the positivity of a polynomial. Our algorithm has reasonable runtime efficiency to be used as a criterion in large implementation space explorations. We ensure that there are no false positives but false negative answers may occur. For negative answers we give a tight bound on the margin of acceptable specifications.We demonstrate application of our algorithm to the comparison of various finite-precision implementations of filters already fully designed.

The worst-case peak gain (WCPG) of a linear filter is an important measure for the implementation of signal processing algorithms. It is used in the error propagation analysis for filters, thus a reliable evaluation with controlled precision is required. The WCPG is computed as an infinite sum and has matrix powers in each summand. We propose a direct formula for the lower bound on truncation order of the infinite sum in dependency of desired truncation error. Several multiprecision methods for complex matrix operations are developed and their error analysis performed. A multiprecision matrix powering method is presented. All methods yield a rigorous solution with an absolute error bounded by an a priori given value. The results are illustrated with numerical examples.

The major contribution of this paper is the presentation of a general unifying description of distributed algorithms allowing to map local, node-based algorithms onto a single global, network-based form. As a first consequence the new description offers to analyze their learning and steady-state behavior by classical methods. A further consequence is the analysis of implementation issues as they appear due to quantization in computing and communication links. Exemplarily, we apply the new method on several different averaging algorithms: the Push-Sum protocol, average consensus as well as its quantized form and furthermore examine the effects of quantization noise which is introduced by the bandwidth limited communication links and finite precision computation ability of every node. Statistical properties of these quantization noises are provided and verified by simulations.