2025

 nach oben zur Jahresübersicht

• Alexander Konrad, Christoph Scholl
  FastPoly: An Efficient Polynomial Package for the Verification of Integer Arithmetic Circuits
  2025 Proceedings of the 25th Conference on Formal Methods in Computer-Adied Design - FMCAD 2025, TU Wien Academic Press
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  In recent years, methods based on Symbolic Computer Algebra (SCA) have become increasingly successful in the field of formal verification of arithmetic circuits. While several different approaches have been proposed to tackle this challenging task, most of them are based on the same mathematical operations. They perform ideal membership tests that reduce specification polynomials by a series of polynomial divisions. For integer arithmetic, under certain conditions, the polynomial divisions boil down to substitutions of variables in integer polynomials. In this context, the overall performance of an SCA verification tool is closely related to the efficiency of the steps manipulating integer polynomials. In this paper we present our tool FastPoly, a package for representing integer polynomials that provides efficient operations including variable substitution with integrated normalization steps. We also provide the sources of our tool, making it available for other research groups to support future progress in this field.

2024

 nach oben zur Jahresübersicht

• Alexander Konrad, Christoph Scholl, Alireza Mahzoon, Daniel Große, Rolf Drechsler
  Divider Verification Using Symbolic Computer Algebra and Delayed Don't Care Optimization: Theory and Practical Implementation
  2024 Formal Methods in System Design
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Recent methods based on Symbolic Computer Algebra (SCA) have shown great success in formal verification of multipliers and - more recently - of dividers as well. In this paper we enhance known approaches by the computation of satisfiability don't cares for so-called Extended Atomic Blocks (EABs) and by Delayed Don't Care Optimization (DDCO) for optimizing polynomials during backward rewriting. Using those novel methods we are able to extend the applicability of SCA-based methods to further divider architectures which could not be handled by previous approaches. We succesfully apply the approach to the fully automatic formal verification of large dividers (with bit widths up to 512).
• Alexander Konrad, Christoph Scholl
  Symbolic Computer Algebra for Multipliers Revisited - Its All About Orders and Phases
  2024 Proceedings of the 24th Conference on Formal Methods in Computer-Adied Design - FMCAD 2024, TU Wien Academic Press
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Using Symbolic Computer Algebra (SCA) enabled a huge progress in formal verification of arithmetic circuits in recent years. Several different approaches have been proposed showing great success especially for the verification of multipliers. Some of them are based on precomputing and simplifying polynomials for specific circuit structures like converging cones while others take advantage of known or detected hierarchy information to replace and simplify particular sub-circuits of the design. In this paper we propose a new method that avoids the use of such methods and applies only two dynamic approaches: (1) choosing a good substitution order for the backward rewriting process and (2) adjusting the phases of signals occuring in the intermediate polynomials during the verification process. Both methods are simply based on a greedy local search taking the the sizes of intermediate polynomials into account. Our experimental results show that this method is very competitive with already existing tools and it improves their robustness, e.g. against optimizations of the verified circuits using logic synthesis.

2023

 nach oben zur Jahresübersicht

• Alexander Konrad, Christoph Scholl, Alireza Mahzoon, Daniel Große, Rolf Drechsler
  Divider Verification Using Symbolic Computer Algebra and Delayed Don’t Care Optimization (extended abstract)
  2023 MBMV
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Recent methods based on Symbolic Computer Algebra (SCA) have shown great success in formal verification of multipliers and -- more recently -- of dividers as well. Here we give an overview of our work published in [1-3] which enhances SCA-based verification by the computation of satisfiability don't cares for so-called (Extended) Atomic Blocks (EABs) and by Delayed Don't Care Optimization (DDCO) for optimizing polynomials during backward rewriting. The optimization is reduced to Integer Linear Programming (ILP). Whereas the basic methods using SCA failed for divider verification, using those novel methods we are able to verify (formally and fully automatically) large gate level implementations of several divider architectures (with bit widths up to 512).

2022

 nach oben zur Jahresübersicht

• Alexander Konrad, Christoph Scholl, Alireza Mahzoon, Daniel Große, Rolf Drechsler
  Divider Verification Using Symbolic Computer Algebra and Delayed Don't Care Optimization
  2022 Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design (FMCAD), TU Wien Academic Press
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Recent methods based on Symbolic Computer Algebra (SCA) have shown great success in formal verification of multipliers and - more recently - of dividers as well. In this paper we enhance known approaches by the computation of satisfiability don't cares of so-called Extended Atomic Blocks (EABs) and by Delayed Don't Care Optimization (DDCO) for optimizing polynomials during backward rewriting. Using those novel methods we are able to extend the applicability of SCA-based methods to further divider architectures which could not be handled by previous approaches. We successfully apply the approach to the fully automatic formal verification of large dividers (with bit widths up to 512).

2021

 nach oben zur Jahresübersicht

• Christoph Scholl, Alexander Konrad, Alireza Mahzoon, Daniel Große, Rolf Drechsler
  Verifying Dividers Using Symbolic Computer Algebra and Don’t Care Optimization
  2021 DATE, IEEE
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Our experimental results show that this method is the key for enabling the verification of large and optimized non-restoring dividers (with bit widths up to 512).

2020

 nach oben zur Jahresübersicht

• Christoph Scholl, Alexander Konrad
  Symbolic Computer Algebra and SAT Based Information Forwarding for Fully Automatic Divider Verification
  2020 Design Automation Conf., Seiten: 1 - 6
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  the opposite direction. We successfully apply the method to the fully automatic formal verification of large non-restoring dividers.