Digital circuits are custom-designed, which increases the likelihood of bugs. Despite efforts taken by engineers, a variety of unforeseen errors can occur. Formal verification is an approach that applies mathematical models and algorithms to prove or disprove that a design works as intended. An alternative to these methods is Symbolic Computer Algebra (SCA), which is a polynomial algebra-based model that can be used for arithmetic circuit verification. Computing a Grobner Basis utilizing these polynomials for ideal membership testing for verification has been found to work well for arithmetic circuits. Rectification for arithmetic circuits may be able possible by creating a modified Grobner Basis, which will be explored by this project.