Divider Verification Using Symbolic Computer Algebra and Delayed Don’t Care Optimization

Recent methods based on Symbolic Computer Algebra (SCA) have shown great success informal 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). Where as the basic methods using SCA failed for divider verification, using those novel method sweareable to verify (formally and fully automatically) large gate level implementations of several divider architectures (with bit widths up to 512).