On equivalence checking and logic synthesis of circuits with a common specification