MultiLinG - Extracting Linear Relations from Gröbner Bases for Formal Verification of And-Inverter Graphs (Artifact)

MultiLinG is a formal verification tool implemented in C++ designed for efficiently verifying And-Inverter Graphs (AIGs). It leverages algebraic techniques by encoding the circuit as a set of polynomial equations and computing Gröbner bases to extract linear relations that facilitate correctness verification. Unlike traditional approaches that focus on rewriting the specification polynomial, MultiLinG shifts the computational effort towards manipulating the Gröbner basis itself. By employing degree-based term orderings and local Gröbner basis computations using the computer algebra library msolve, MultiLinG minimizes intermediate complexity and enhances scalability when handling large, complex circuits. MultiLinG demonstrates its practical effectiveness through formal verification of arithmetic circuits, particularly multipliers.MultiLinG是一款基于C++实现的形式化验证工具，专为高效验证与反相器图（And-Inverter Graphs，简称AIGs）而设计。该工具借助代数技术，将电路编码为一组多项式方程，并通过计算格罗贝纳基（Gröbner basis）提取可助力正确性验证的线性关系。与传统方法侧重重写规范多项式不同，MultiLinG将计算重心转移至格罗贝纳基本身的操作。通过采用基于度数的项序（term orderings），并借助计算机代数库msolve执行局部格罗贝纳基计算，MultiLinG可在处理大型复杂电路时最小化中间复杂度并提升可扩展性。MultiLinG通过对算术电路（尤其是乘法器）的形式化验证，证明了其实际应用有效性。