从Gröbner基提取线性关系用于与逆变图的形式验证

基于计算机代数的形式验证技术已被证明对电路验证非常有效。电路以与逆变图形式给出,被编码为一组多项式,这些多项式在字典序项序下自动生成一个Gröbner基。电路的正确性可以通过计算规范的多项式余式来推导。然而,主要障碍是在规范重写过程中出现的单项式膨胀,这导致了专门启发式方法的发展以克服此问题。在本文中,我们研究了一种正交方法,将计算工作集中在重写Gröbner基本身。我们的目标是确保基中包含线性多项式,这些多项式可以有效地用于重写线性化的规范。我们首先证明了该技术的可靠性和完备性,然后展示了其实际应用。我们的实现在与乘法器验证相关的基准测试中显示出有前景的结果。