Verification of Fixed-Point Digital Controllers
Using Direct and Delta Form Realizations
(Benchmark Results)

Properties:  Overflow  Limit Cycle  Stability  Minimum Phase  Timing

Test Case Numerator Denominator Gain Input Range Bits
1 {0.15f, 0.05f, 0.4f} {1.0f, 0.0f, 0.3f} x10^6 [ -1, 1 ] < 3, 4 >
2 {2.000000f, -4.000000f, 2.000000f} {1.000000f, 0.000000f, -0.250000f} x10^6 [ -1, 1 ] < 2, 6 >
3 {0.2f, -0.4f, 0.2f} {1.0f, 0.0f, -0.25f} x10^7 [ -1, 1 ] < 3, 4 >
4 { 1.0f, -2.819f, 2.637f, -0.8187f} {1.0f, -1.97f, 1.033f, -0.06068f} 50 [ -1, 1 ] < 2, 13 >
5 {0.0937f, -0.3582f, 0.5201f, -0.3482f, 0.1003f, -0.0078f} {1.0000f, 9.1122f, -2.2473f, -8.6564f, 0.6569f, 0.1355f} x10^9 [ -1, 1 ] < 2, 13 >
6 {0.00937f, -0.03582f, 0.05201f, -0.03482f, 0.01003f, -0.00078f} {1.0000f, 9.1122f, -2.2473f, -8.6564f, 0.6569f, 0.1355f} x10^10 [ -10, 10 ] < 2, 13 >
7 {0.1f, -0.2819f, 0.2637f, -0.08187f} {1.0f, -2.574f, 2.181f, -0.6068f} 500 [ -4, 4 ] < 2, 13 >
8 {0.10f, -0.28f, 0.26f, -0.08f} {1.0f, -2.57f, 2.18f, -0.60f} 500 [ -5, 5 ] < 2, 8 >
9 {0.1f, -0.28f, 0.26f, -0.08f} {1.0f, -2.57f, 2.18f, -0.60f} 500 [ -6, 6 ] < 4, 11 >
10 {0.2f, -0.4f, 0.2f} {1.0f, 0.0f, -0.25f} - [ -1, 1 ] < 3, 12 >
11 {0.10f, -0.30f, 0.30f, -0.10f } {1.000f, 1.800f, 1.140f, 0.272f } x10^7 [ -2, 2 ] < 2, 13 >
12 {0.100f, -0.250f, 0.200f, -0.050f } {1.000f, 1.500f, 0.680f, 0.096f } x10^7 [ -2, 2 ] < 2, 13 >
13 {0.0937f, -0.3582f, 0.5201f, -0.3482f, 0.1003f, -0.0078f} {1.0000f, 9.1122f, -2.2473f, -8.6564f, 0.6569f, 0.1355f} x10^9 [ -10, 10 ] < 2, 13 >
14 {0.010f, -0.030f, 0.030f, -0.010f } {1.000f, 1.800f, 1.140f, 0.272f } x10^7 [ -3, 3 ] < 3, 10 >
15 {0.100f, -0.250f, 0.200f, -0.050f } {1.000f, 1.500f, 0.680f, 0.096f } x10^7 [ -5, 5 ] < 4, 11 >
16 {0.1f, -0.28f, 0.26f, -0.08f} {1.0f, -2.57f, 2.18f, -0.60f} 500 [ -10, 10 ] < 5, 10 >
17 { 7.936f, -2.919f } { 1.00000000f, 0.3890000f } - [ -9, 9 ] < 5, 10 >
18 { 0.9411f, -0.4229f } { 1.00000000f, 0.2480000f } 10 [ -3, 3 ] < 3, 5 >
19 { 1.1000f, -0.6039f } { 1.00000000f, 0.0340000f } 10 [ -3, 3 ] < 3, 5 >
20 { 1.2670f, -0.8493f } { 1.0000000f, -0.2543000f } 10 [ -3, 3 ] < 3, 5 >
21 { 1.4340f, -1.174f } { 1.0000000f, -0.6080000f } 10 [ -3, 3 ] < 3, 5 >
22 { 1.5000f, -1.357f } { 1.0000000f, -0.8010000f } 10 [ -3, 3 ] < 3, 5 >
23 { 1.5610f, -1.485f } { 1.0000000f, -0.9000000f } 10 [ -3, 3 ] < 3, 5 >
24 { 1.5840f, -1.553f } { 1.0000000f, -0.9600000f } 10 [ -3, 3 ] < 3, 5 >
25 { 2.81300000f,-0.0163f, -1.8720000f } { 1.000f, 1.068f, 0.1239f } - [ -5, 5 ] < 4, 5 >
26 { 1.611f, 3.079f, -3.794f } { 1.00000000f, 1.0840000f, 0.1289f } - [ -5, 5 ] < 4, 5 >
27 { -1.692f, 10.43f, -7.915f } { 1.00000000f, 1.0460000f, 0.08148f } - [ -12, 12 ] < 6, 7 >
28 { -1.099f, 2.978f, -1.812f } { 1.00000000f, 0.9068000f, -0.06514f } 10 [ -4, 4 ] < 4, 5 >
29 { -0.4603f, 1.006f, -0.5421f } { 1.00000000f, 0.5949000f, -0.3867f } 100 [ -3, 3 ] < 3, 7 >
30 { -1.239f, 2.565f, -1.323f } { 1.00000000f, 0.3423000f, -0.6468f } 100 [ -4, 4 ] < 4, 5 >
31 { -2.813f, 5.719f, -2.905f } { 1.00000000f, 0.18330f, -0.8107f } 100 [ -6, 6 ] < 4, 5 >
32 { -0.753f, 1.519f, -0.766f } { 1.00000000f, 0.0762700f, -0.9212f } 1000 [ -3, 3 ] < 3, 5 >
33 { -1.553f, 3.119f, -1.566f } { 1.00000000f, 0.0387300f, -0.96f } 1000 [ -3, 3 ] < 3, 5 >

http://dsverifier.org