Why do we do Equivalence Check on RTL vs Gate Netlist?

I’m quite confused about the importance of Equivalence Checking between RTL and Gate Netlist… I know that synthesis converts RTL code into gate netlist, but does this mean that the reason why we do Equivalence Checking between this two is because we don’t trust the synthesis tool that it correctly synthesized the code?.. If yes then, we are rather verifying the reliability of the tool, which I think is not practical since the creators of the tool might have done exhaustive verification of their product… We could have just focus on verifying our design rather than verifying the tool.

So what is the real reason why we do EC? I haven’t used it. My only guess is that maybe there’s a user input when doing EC, and this might be the reason why we still need to do EC - to verify if these user inputs are correctly set. Am I right?

One of the reason for LEC is to independently verify that the synthesis tool has not introduced an error into the netlist. A synthesis tool is just software after all so can still have some corner case bugs This is often mandated for design assurance flows such as D0-254.
In ASIC flows, sometimes a manual netlist edit can be done when a late ECO occurs, and again the LEC tool will check that the designs are still equivalent.
You can also use LEC after DFT scan insertion, again to check that the functionality has not been affected. For FPGA you can verify the output from synthesis and again after place and route.

LEC does NOT eliminate the need to run some gate level simulation (GLS), but it can be greatly reduced. This is often the main reason for using LEC as gate level sims just take too long… in some cases a GLS regression could take weeks or months.
LEC runtimes in comparison (although design dependent) would be in the order of a couple of hours.

When you do use LEC, you black box any vendor macros such as RAMS, FIFOs, etc so you should always run some GLS just to check that the interfaces to these macros is functioning correctly.
You should also be running static timing analysis to check the timings on the complete design.