Entwicklung. Implementierung und Anwendung mathematisch-algebraischer Algorithmen bei der formalen Verifikation digitaler Systeme mit Arithmetikblöcken

• Applicants: Professor Dr. Gert-Martin Greuel; Professor Dr.-Ing. Wolfgang Kunz
• Subject Area: Security and Dependability, Operating-, Communication- and Distributed Systems
• Term: from 2006 to 2011
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 16728219

• Final Report Year: 2011

Final Report Abstract

In diesem interdisziplinären Projekt zwischen Informationstechnik und Mathematik haben wir einen grundsätzlich neuen Ansatz zur formalen Verifikation von Datenpfaden mit komplexer Arithmetik erforscht. Den im Vorgangerprojekt gefundenen Ansatz, arithmetische Komponenten einer digitalen Schaltung effizient durch Polynome zu modellieren, haben wir systematisch weiterentwickelt. Durch Kombination mit dem klassischen SAT-Ansatz haben wir einen neuartigen SAT Modulo Theory (SMT)-Solver für Formeln der SMT-Klasse QF-BV (Quantifier-free logic of bitvectors) geschaffen. Die dabei entstandene Software STABLE ist ein universell einsetzbares Werkzeug, das es ermöglicht, die Formalismen der Computeralgebra in eine allgemeine Verifikationsumgebung einzubinden, die sowohl den Kontroll- als auch den Datenfluss eines Designs verifiziert. Es stellt eine ideale Ergänzung zu bestehende Verifikationstechniken dar, die vorwiegend auf die Verifikation des Kontrollflusses zugeschnitten sind. Wir nutzen dabei aus, dass die aufwendigen Berechnungen von Gröbnerbasen durch geschickte Formulierung der digitalen Komponentenmodelle auf arithmetischer Bitebene (ABL) (engl.: arithmetic bit level) vermieden werden kann. Die Routinen zur Berechnung der algebraischen Normalform haben wir dabei von Grund auf neu konzipiert, um mit Polynomsysteme mit mehrere tausend Variable, wie sie aus ABL-Modellen hervorgehen, robust und effektiv umgehen zu können. Interessanterweise konnten wir feststellen, dass die Datenstrukturen weniger wichtig für die Gesamtperformance waren als ursprünglich gedacht. Vielmehr brachte eine geschickte Vorverarbeitung letztlich den Durchbruch. Das Projekt ist aus Sicht der Antragsteller ein Beispiel für gelungene, interdisziplinäre Zusammenarbeit zwischen einer ingenieurwissenschaftlichen und einer mathematischen Arbeitsgruppe. Die wesentliche Innovation des Projektes besteht darin, einen Ansatz für die formale Eigenschaftsprüfung auf Basis algebraischer Methoden entwickelt zu haben, der einen völlig neuen Zugang zu diesem Problemfeld verschafft. Durch Experimente mit zahlreichen industriellen Beispielen aus aktuellen Prozessorentwicklungen konnten wir zeigen, dass STABLE als erstes Tools dieser Art erfolgreich SAT-basierte Beweistechniken mit Methoden der Computeralgebra kombiniert. Während die besten der bislang vorhandenen Solver beispielsweise bei arithmetischen Operationen versagen, können wir diese vollständig verifizieren. Zukünftig ist es geplant sowohl die Techniken zur Generierung von ABL- und Polynommodellen zu verbessern, als auch neue Datenstrukturen und Algorithmen für die Basisbeweistechniken zu entwickeln. Im Rahmen des Projektes „Industrielle Algebra" wollen wir außerdem einen neuen Zweig der Computeralgebra begründen, um die breite Anwendbarkeit unserer Techniken im industriellen Umfeld weiter zu verfolgen.

Publications

• An algebraic approach for proving data correctness in arithmetic data paths. Proc. International Conference Computer Aided Verification (CAV), July 2008, Princeton, NJ. USA (2008), pp. 473-486
  O. Wienand, M. Wedler, G.-M. Greuel, D. Stoffel and W. Kunz
  
• Modeling of Custom-Designed Arithmetic Components in ABL Normalization. In: Proc. Forum on Specification & Design Languages (FDL), Stuttgart, Germany, 2008
  E. Pavlenko, M. Wedler, D. Stoffel, O. Wienand, E. Karibaev and W. Kunz
  
• A New Verification Technique for Custom-Designed Components at the Arithmetic Bit Level, pp. 257-272. In: Martin Radetzki (Ed.), Languages for Embedded Systems and their Applications, Lecture Notes in Electrical Engineering 36, Springer Netherlands, 2009
  E. Pavlenko, M. Wedler, D. Stoffel, W. Kunz, O. Wienand and E. Karibaev
  
• New developments in the theory of Gröbner bases and applications to formal verification. Journal of Pure and Applied Algebra, 213(8). pp. 1612—1635, 2009
  Michael Brickenstein, Alexander Dreyer, Gert-Martin Greuel, Markus Wedler and Oliver Wienand
  
• PolyBoRi: A framework for Gröbner-basis computations with Boolean polynomials. Journal of Symbolic Computation, 44(9), pp. 132—1345, 2009
  Michael Brickenstein and Alexander Dreyer
  
• Normalization of Rings. Journal of Symbolic Computation, 45(9), pp. 887-901, September 2010
  Gert-Martin Greuel, Santiago Laplagne, Frank Seelisch
  
• Solving hard instances in QF-BV combining Boolean reasoning with computer algebra. In: Bernd; Bertacoo Becker, Ed., Algorithms and. Applications for Next Generation SAT Solvers 09461 of Dagstuhl Seminar Proceedings Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Dagstuhl. 2010
  Markus Wedler, Evgeny Pavlenko, Alexander Dreyer, Frank Seelisch, Dominik Stoffel, Gert-Martin Greuel and Wolfgang Kunz
  
• Algorithms for Symbolic Computation and their Applications - Standard Bases over Rings and Rank Tests in Statistics. PhD thesis, TU Kaiserslautern, Germany, April 2011
  Oliver Wienand
  
• STABLE: A new QF-BV SMT Solver for hard Verification Problems combining Boolean Reasoning with Computer Algebra. In: Proc. International Conference on Design, Automation and Test in Europe (DATE), 2011
  Evgeny Pavlenko, Markus Wedler, Dominik Stoffel, Wolfgang Kunz, Frank Seelisch, Gert-Martin Greuel and Alexander Dreyer
  
• The Gröbner basis of the ideal of vanishing polynomials. Journal of Symbolic Computation, 46(5), pp. 561-570, May 2011
  Gert-Martin Greuel, Frank Seelisch and Oliver Wienand