text: #include <dsverifier.h>
  
            digital_system ds = {
              .b =  { 0.000109690591321,   0.001316287095853,   0.007239579027191,   0.024131930090637,   0.054296842703932,   0.086874948326292, 0.101354106380674,   0.086874948326292,   0.054296842703932,   0.024131930090637,   0.007239579027191,   0.001316287095853, 0.000109690591321 },
              .b_size = 13,
              .a = {1.000000000000000,  -2.393643991551106,   4.113621058366342,  -4.594707860177270,   3.987520576986952,  -2.604377026937114, 1.340805025908970,  -0.530071941777575,   0.161061450057486,  -0.036049397170938,   0.005664193637792,  -0.000555145649249, 0.000025720356837 },
              .a_size = 13
           };
  
  
  implementation impl = { 
      .int_bits = 4,
      .frac_bits = 10,
      .min = -1.6,
      .max = 1.6,
  };
  
  
  filter_parameters filter = {
      .Ac =  0.707945784384138, 
      .Ap =  0.707945784384138, 
      .Ar =  0.707945784384138, 
      
      .wp = 0.39, 
      .wc = 0.4,
      .wr = 0.41, 
      .type = 1
  };