ModelSim or Questa for Netlist Simulation
Depending on your approach for RTL simulation, you can use the same method and test suite for netlist verification, i.e., ModelSim for traditional simulation and Questa for more advanced methods.
FormalPro uses formal (mathematical) methods to compare one model to another, to determine if they are functionally equivalent. This is especially useful in DO-254 flows to verify that the synthesized (or placed-and-routed) netlist functions the same as the RTL. FormalPro can be used standalone or in a flow integrated with Precision Synthesis.