  In safety-critical applications that rely on the solution of an optimization
problem, the certification of the optimization algorithm is of vital
importance. Certification and suboptimality results are available for a wide
range of optimization algorithms. However, a typical underlying assumption is
that the operations performed by the algorithm are exact, i.e., that there is
no numerical error during the mathematical operations, which is hardly a valid
assumption in a real hardware implementation. This is particularly true in the
case of fixed-point hardware, where computational inaccuracies are not
uncommon. This article presents a certification procedure for the proximal
gradient method for box-constrained QP problems implemented in fixed-point
arithmetic. The procedure provides a method to select the minimal fractional
precision required to obtain a certain suboptimality bound, indicating the
maximum number of iterations of the optimization method required to obtain it.
The procedure makes use of formal verification methods to provide arbitrarily
tight bounds on the suboptimality guarantee. We apply the proposed
certification procedure on the implementation of a non-trivial model predictive
controller on 32-bit fixed-point hardware.
