Module fraig 

Combinational equivalence by incremental SAT sweeping, certified by one derivation.

crate::sweep puts each candidate to a fresh solver over a formula of its own and certifies each lemma by an LRAT refutation of that formula. Here every question is a solve under assumptions on one solver, so what one query learns later ones keep (Mishchenko, Chatterjee, Brayton & Een, Improvements to combinational equivalence checking, ICCAD 2006, the scheme of ABC’s &cec). The solver holds the clauses of the miter’s formula (formula: the Tseitin clauses of every And node, node k the variable k) only for the cones its queries have asked about, encoded as each query needs them, and decides only on those nodes, so a query’s search stays in its cone. Its variables are numbered as it meets them, so a solver is as large as what it was asked, and once it has Options::recycle of them a fresh one replaces it. It holds the reduced graph, not the miter: each node defined over its fan-ins’ representatives (n ↔ rep(x) ∧ rep(y), logged the first time a solver needs it), so the logic two sides share once merged is one variable to it and no chain of equalities.

The sweep runs in node order, each node with a representative literal. A node whose fan-ins’ representatives make a constant, a copy of one of them, or the pair an earlier node has, is that constant, copy or node, with no solver call (structural hashing over representatives). Any other node is put against the earlier node whose simulation signature it shares: n ∧ ¬r, then ¬n ∧ r, under assumptions, within a conflict budget; a model is a counterexample, added to the simulation to split the class. The budget starts small, since a query that runs out is mostly one the merges around it would make easy: when a round leaves an output pair open, the next sweeps afresh at ten times the budget (Options::rounds).

Every clause made goes into one log with its LRAT hints, in the order made, each hint the id of a clause of the formula or of the log before it: a clause a solver learns with the chain its conflict analysis resolved, a solved merge (¬n ∨ r), (n ∨ ¬r) with the chain of the refutation of its assumptions, and a structural merge or a reduced definition with the chain unit propagation finds through the definitions and merges it rests on. A solver’s learned clauses that no clause made in its time rests on go with it when it is replaced, since no later clause can name them. An output pair proven equal adds its own two clauses, the claims, and the derivation is the steps the claims reach back through their hints, in order. Report::check rebuilds the formula from the miter and replays it (crate::lrat::check_derivation). A difference is a model whose inputs, evaluated, separate the pair.

Structs

Options

How decide searches.

Progress

A report of a long search: report is handed the cost so far once every every nodes swept, once the sweep is done, and once the output pairs are, before the derivation is taken from the log.

Report

A decided miter: a verdict per output name, the derivation behind the equalities, and the search’s cost.

Stats

What a decision cost.

Functions

decide

Decide a ≡ b for every pair of literals of aig, latches read as free values: a verdict per pair, the derivation of every equality from formula, and the cost.

equivalent

Pair left and right by output name and decide every pair.

formula

The miter’s formula: for each And node in order its three Tseitin clauses, and node 0 false.