Detecting circuit that's similar in functionality and implementation
This is only an extended comment that came to my mind immediately after reading the question:


suppose you have a 3SAT formula $\phi$ with $n$ variables $x_1,...,x_n$ and let $C$ be the corresponding circuit;
build a new circuit $C'$, adding $m = n^k$ variables $y_1, y_2, ...,y_{n^k}$, and enough gates to AND the $m$ new variables with the output of the original $C$ ($C' = \phi \land y_1 \land ... \land y_m$);
build a new circuit $D'$ from $C'$ that simply forces its output to 0 using an AND and NOT gate ($D' = C' \land \neg C'$)


If $\phi$ is not satisfiable then $D'$ and $C'$ are equivalent, otherwise they differ when the $x_i$ satisfy the formula AND all $y_i = 1$, but you can choose $m$ large enough to make the probability that $\bigwedge y_i =  1$ very small.

So if you have an efficient algorithm for your problem, you can afficiently solve the 3SAT instance.