SCA verification tools & topics


The paper introduces a verification method based on Symbolic Computer Algebra (SCA) and presents a new theory for the origin of vanishing monomials, redundant monomials which lead to an monomial explosion for non-trivial multipliers. The implemented SCA-verifier PolyCleaner is able to prove the correctness for non-trivial million-gate multipliers where the other state-of-the-art methods failed.

For PolyCleaner we received the Best Paper Award at the International Conference on Computer Aided Design (ICCAD) 2018.

How to get PolyCleaner


Created by
Group of
Computer Architecture, University of Bremen
University of Bremen
Institute for
Complex Systems, JKU Linz
Johannes Kepler University Linz

supported by SyDe