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

Daniela Kaufmann, Jérémy Berthomieu

Formal verification techniques based on computer algebra have proven highly effective for circuit verification. The circuit, given as an and-inverter graph, is encoded as a set of…