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

Iury V. Bessa, Hussama I. Ismail, Lucas C. Cordeiro, Joao E. C. Filho

Research output: Contribution to journalArticlepeer-review


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.
Original languageEnglish
Pages (from-to)95-126
JournalDesign Automation for Embedded Systems
Issue number2
Publication statusPublished - 10 Mar 2016


  • Fixed-point digital controllers
  • Direct and delta forms
  • Formal methods
  • Bounded model checking


Dive into the research topics of 'Verification of fixed-point digital controllers using direct and delta forms realizations'. Together they form a unique fingerprint.

Cite this