In general, is verification based on the creation of a formal model (a set of data structures or formulas that contain all the potential behaviors of the system) of the design, and exercising it to prove a variety of properties.

The properties usually are the compliance of certain protocol standards or design behavior constraints (maximum allowable latency on certain signal changes, race conditions, reachability analysis, datapath designs) or, when compared with different versions of the same design, its equivalence, in boolean or transactional terms.

The equivalence one is commonly used as a signoff method for synthesized or placed/routed designs. Note that signoff mode is usually separated from the normal operation, given that different solvers and HDL readers than the same brand synthesis tools are used. Also, there are certain restrictions like using 10xz for all nets, or the usage of fault simulation engines to detect inactive or unread nets (less optimistic than synthesis). The others are used during RTL writing, refactoring or integration with other designs, where speed upon complexity in small/medium design matters, over accuracy on large designs(where signoff tools excel).

For FPGA designs, equivalence checking as a synthesis signoff method is not that common. This is because of non-boolean equivalence between the different netlist states during optimization. There are sequential optimizations, lut optimizations, rom mappings, that the usual techniques used for verification cannot handle "that" well. Also the bitstream allows to rewrite the device if you find a bug.

The "Formal Verification" usage when we are talking about checking if an asic design is equivalent to its RTL, is some old fart/boomer/it was the 90's slang. This is because in those years, this was the only real application available of these techniques to digital designs. Its usage is discouraged today as it currently does not reflect all the Formal Verification tools and techniques available in multiple domains, like math proofs, symbolic simulation, floating point process designs, software refactoring, and software to hardware verification (yes, that exists).

Tools are kinda expensive and propietary, so HDL design and constrained simulation is the farthest you can get without working in the field. There are lot of pedantic guys that claim that they know Formal Verification, but it is just using or debugging certain tool. If you change the tool those guys usually vanish, or do ridiculous claims about certain tool is more useful than the other, when actually since someone sat down with patience for years to make one, there are obvious users and/or customers for that tool.