Word-Level Multi-Fix Rectifiability of Finite Field Arithmetic Circuits

Vikas Rao1, Irina Ilioaea2, Haden Ondricek1, Priyank Kalla1, Florian Enescu3
1University of Utah, 2Louisiana State University Shreveport, 3Georgia State University


Deciding whether a buggy circuit can be rectified at a given subset of nets to match its specification constitutes a critical problem in post-verification debugging and rectification. Contemporary approaches which utilize Boolean SAT and Craig Interpolation techniques are infeasible in proving the rectifiability of arithmetic circuits. This paper presents a novel approach using symbolic computer algebra to prove the rectifiability of a buggy finite field arithmetic circuit at a given set of m nets. Our approach uses a word-level polynomial model and an application of a Gröbner basis decision procedure. The finite fields corresponding to the datapath word-length (n) and the patch word-length (m) may not be compatible. We make new mathematical and algorithmic contributions which resolve this disparity by modeling the problem in an appropriate composite field. Experiments demonstrate the efficacy of our word-level approach to ascertain multi-fix rectifiability compared to contemporary approaches.