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
- The binary of PolyCleaner and the benchmarks are avialable at GitHub!