Module seq_equiv 

Sequential equivalence by unrolling: a pipelined circuit proven equal to its combinational reference at its latency, or two pipelines of different depths proven to compute the same transaction.

at_latency unrolls a circuit’s transition relation latency + 1 times into one combinational graph. The inputs of clock 0 keep their names, the inputs of clock k ≥ 1 are named name@k, a latch with a free initial value becomes an input latch@init, and an initialized latch becomes its constant; the outputs read at clock latency keep their names. Equality of those outputs with a reference over the clock-0 inputs, for every initial state and every later input, says exactly that the circuit is a pipeline of that latency for that function: an output that leans on a stale state, on a later input, or on feedback is told apart by a witness. aligned does this for both sides at once, each side’s initial state its own (a state shared between two designs would hide a difference), and decides the pair with crate::sweep, certificate and all; aligned_by_fraig decides it by incremental SAT sweeping (crate::fraig), one derivation for every equality.

always_equal decides two sequential circuits for every clock from reset, by register correspondence (van Eijk, Sequential equivalence checking based on structural similarities, TCAD 2000): the two run side by side in one Product; simulated from reset, their registers fall into classes of equal (or complementary) values; the classes are refined until, assumed of a state, they hold of the next state for every input, each step a refuted difference with an LRAT proof (crate::sweep::query with the classes as its assumptions); and the outputs are proven equal under them. The InductionCertificate is that invariant, its steps’ proofs and the outputs’ proofs; check_always replays it, including the invariant’s truth at reset. When the correspondence is not strong enough, bounded model checking looks for the shortest difference from reset (Trace, replayed by replays); finding none, the verdict is unknown, never equal.

Structs

InductionCertificate

The proof that two circuits agree at every clock from reset: an invariant of register literal pairs true at reset, each pair’s next values proven equal assuming the invariant (one proof a pair, in order), and each output pair proven equal assuming it (one proof an output, in the product’s order, absent for an output pair that is one literal).

Product

Two sequential circuits run side by side: inputs of the same name shared, every register of each with its initial value, each named output of the left paired with the right’s, and an output a pair’s difference.

SeqOptions

How always_equal searches.

SeqReport

Trace

An assignment from reset under which a pair of outputs differs at the last clock: the registers that start free, by index of the product’s registers (the others are read from their initial values), and the inputs of each clock.

Enums

SeqVerdict

Functions

aligned

Whether left’s outputs at clock left_latency equal right’s at clock right_latency, as functions of the clock-0 inputs they share by name, for every initial state of each and every later input.

aligned_by_fraig

aligned, decided by crate::fraig.

aligned_pair

The two combinational circuits aligned decides between: each side at its latency, its free initial values named apart from the other’s ([email protected], [email protected]).

always_equal

Whether the two circuits’ outputs agree at every clock from reset.

at_latency

The outputs at clock latency as a combinational graph over the clock-0 inputs (by their own names), the later clocks’ inputs and the free initial values.

check_always

Whether cert proves the product’s outputs equal at every clock from reset.

latency_equivalent

Whether pipeline’s outputs at clock latency equal the combinational reference over the clock-0 inputs.

latency_equivalent_by_fraig

latency_equivalent, decided by crate::fraig.

product

The two circuits as one Product.

replays

Whether trace, run on the product from reset, ends at a clock where some output pair differs.

unroll

The graph unrolled over frames clocks, the latches’ starting values from their initial values, the outputs of every clock named name@k.