Armin Biere, Katalin Fazekas, Dr., Mathias Fleury, Nils Froleyks,
"Clausal Equivalence Sweeping"
, in Nina Narodytska, Philipp Rümmer: PROCEEDINGS OF THE 24TH CONFERENCE ON FORMAL METHODS IN COMPUTER-AIDED DESIGN ? FMCAD 2024, Serie Formal Methods in Computer-Aided Design, Vol. Volume 5, Nummer ISSN (Online): 2708-7824, TU Wien Academic Press, Wien, 10-2024, ISBN: 978-3-85448-065-5
Original Titel:
Clausal Equivalence Sweeping
Sprache des Titels:
Englisch
Original Buchtitel:
PROCEEDINGS OF THE 24TH CONFERENCE ON FORMAL METHODS IN COMPUTER-AIDED DESIGN ? FMCAD 2024
Original Kurzfassung:
The state-of-the-art to combinational equivalence
checking is based on SAT sweeping. It recursively establishes
equivalence of internal nodes of two circuits to prove equivalence
of their outputs. The approach follows the topological order
from inputs to outputs and makes use of simulation to refine
the set of potentially equivalent nodes to reduce the number of
SAT solver queries. This non-uniform hybrid reasoning, using
both the circuit structure and a clausal encoding, is complex to
orchestrate. In earlier work, clausal encoding was avoided using
a dedicated circuit-aware SAT solver. Instead, we propose to
perform SAT sweeping directly on the clausal encoding of the
complete equivalence checking problem within the SAT solver, but
again relying on a second, dedicated, internal SAT solver. Both
SAT solvers work on a clausal representation. This allows to
transparently make use of all the advanced reasoning capabilities
of the SAT solver, particularly pre- and inprocessing techniques.
Index Terms?Equivalence Checking, SAT Sweeping, Miters,
Equivalence Reasoning, Conjunctive Normal Form, Backbones.
Forschungs-