Kepler Formal now removes matching output logic from a sequential equivalence check before the proof engine spends time on it. Sequential equivalence checking compares two versions of a circuit across clock cycles, usually to prove that synthesis or an engineering change preserved behavior. The tool could previously return an inconclusive result even when a design was compared with itself, because it kept asking the solver to rediscover that wide, identical logic cones matched.
The new pass first proves which registers in the two designs always hold the same value. It then treats each proven pair as one register and rebuilds the logic feeding every observed output. When both sides reduce to the same expression, Kepler marks that output as proven without sending it through the expensive search. The 595-line change also fixes parameterized flip-flops whose optional enable or reset pins exist in the cell definition but are unused in a particular instance.
The practical gain will depend on how much structure the two designs share. A small source edit followed by synthesis often leaves most of the circuit unchanged, which is exactly the case this method targets. If Kepler's tests generalize to production netlists, teams should see fewer inconclusive runs and spend their proof budget on the logic an engineer actually changed.