System level verification of digital signal processing applications based on the polynomial abstraction technique

Polynomial abstraction has been developed for data abstraction of sequential circuits, where the functionality can be expressed as polynomials. The method, based on the fundamental theorem of algebra, abstracts a possibly infinite domain of input values, into a much smaller and finite one, whose size is calculated according to the degree of the respective polynomial. The abstract model preserves the system´s control and data properties, which can be verified by model checking. Experiments show that our approach does not only allow an automatic verification, but also gives considerably better results than existing methods.