In this paper we present a word-level RTL rewriting framework based on equality saturation which facilitates
exploration of equivalent designs. By applying rewrites to a single data structure containing the given specification and
implementation, we can automatically bridge the gap between the two designs. In the case where the given designs are equivalent, the framework can be leveraged to automatically decompose the proof, greatly simplifying the equivalence checking problem. If there is a bug in the implementation, the framework can be used to automatically propose a minimal fix, without substantially modifying the optimized implementation. Our experiments have demonstrated valuable results, converting inconclusive equivalence checking problems to conclusive ones, and speeding up the run-time of converging cases by up to 6x. For cases when a bug is identified in the implementation, the framework produces a variant of the design containing a candidate fix.