Verification of fixed-point digital controllers using direct and delta forms realizations

The extensive use of fixed-point digital controllers demands a growing effort to prevent design errors that appear in the discrete-time domain. The present article describes a novel verification methodology, which employs bounded model checking (BMC) based on satisfiability modulo theories (SMT) to verify the occurrence of the design errors, because of the finite word-length (FWL) format, in fixed-point digital controllers. Here, the performance realizations of the digital controllers realizations that use delta operators are compared to those that use traditional direct forms. The experimental results show that the delta-form realization substantially reduces the digital controllers’ fragility when compared to the direct-form realization. Additionally, the proposed methodology can be very effective and efficient to verify real-world digital controllers, where conclusive results are obtained in nearly 98 % of the benchmarks.