Detection of redundant boolean constraints
The simplification you're describing is called subsumption.  It's a standard technique and some SAT solvers (e.g. minisat) will apply it along with other simplification techniques as a preprocessing step before attacking the SAT problem itself.  In particular, subsumption and equivalent variable substitution together, applied to the generated CNF formula, are enough to do the common subformula elimination you described in the question.  That's because each circuit transformation yields an output variable, and output variables derived from the same circuit can be efficiently identified and reduced to references to a single variable.  After that normal subsumption rules applied to clauses will eliminate the common subformulas.

If you're using a solver that doesn't do this preprocessing, then you can do thr rough equivalent of it during conversion to CNF.  First you'll need to apply duplicate circuit suppression while you're doing the Tseitin tranformation.  As you're doing the transformation to CNF, memoize each circuit you've converted. If you encounter the circuit again, skip the circuit conversion and use the same output variable that you used for the memoized circuit.  Once you've converted everything to clauses, do normal clause subsumption, i.e. check each clause A against every other longer B clause to see if A's literals are a subset of B's.  If so, then A subsumes B and clause B can be discarded from the formula.