Verification of Delta Form Realization in Fixed-Point Digital Controllers Using Bounded Model Checking

The extensive use of fixed-point digital controllers demands a growing effort to prevent design´s errors that appear in the discrete-time domain. This paper presents a novel verification methodology that employs Bounded Model Checking (BMC) based on the Satisfiability Modulo Theories to verify the occurrence of design´s errors, due to the finite word-length format, in fixed-point digital controllers. Here, the performance of 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 reduces substantially the digital controllers´ fragility. Additionally, the proposed methodology can be very effective and efficient to verify real-world digital controllers, where conclusive results are obtained in nearly 95% of the benchmarks.