@inproceedings{cox-san-cha-12-aa-bitprec,
  author = {Cox, Arlen and Sankaranarayanan, Sriram and Chang, Bor-Yuh Evan},
  title = {A Bit Too Precise? {Bounded} Verification of Quantized Digital Filters},
  booktitle = {Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS},
  series = {Lecture Notes in Computer Science},
  volume = {7214},
  year = 2012,
  month = mar,
  location = {Tallinn, EE},
  pages = {33-47},
  doi = {10.1007/978-3-642-28756-5_4},
  comment = {Concerned with validating digital processing circuits for overflows, wasted bits, non-convergence (loops), ect.  Wants to get ``bit-precise'' results. Mentions AA as improvement but in the end does not use it? Instead uses satisfiability-modulo-theories (SMT) solvers?},
  abstract = {Digital filters are simple yet ubiquitous components of a wide variety of digital processing and control systems. Errors in the filters can be catastrophic. Traditionally digital filters have been verified using methods from control theory and extensive testing. We study two alternative verification techniques: bit-precise analysis and real-valued error approximations. In this paper, we empirically evaluate several variants of these two fundamental approaches for verifying fixed-point implementations of digital filters. We design our comparison to reveal the best possible approach towards verifying real-world designs of infinite impulse response (IIR) digital filters. Our study reveals broader insights into cases where bit-reasoning is absolutely necessary and suggests efficient approaches using modern satisfiability-modulo-theories (SMT) solvers.}
}