Parsing the circuit description file in the AIGER format. Using hash to detect structurally equivalent signals in a circuit. Performing Boolean logic simulations and identify functionally equivalent candidate pairs in the circuit as “functionally equivalent candidate (FEC) pair”. Calling Boolean Satisfiability (SAT) solver to prove the functional equivalence. Reducing the circuit size automatically.