January 10, 2016

Overflow Example

Given the following digital controller:

Initially, If the digital controller described by the equation C1 is realizated using some direct form (e.g., DFI, DFII, and DFII) and implemented with <4,4> (i.e., 4 bits for integer part and 4 bits for precision), Its FWL format is able to represent values between -8.0 ~ 7.9375. However, checking this property using DSVerifier, the model checker found a counterexample (to get a violation) for the following inputs: x = {-3.9375, -0.5625, -5.0000, -0.3750, 3.7500, -0.4375 }.

The outputs generated by the digital controller are shown bellow.