+Short summary:
+
+there are two main ways to check that the HDL matches (is "equivalent") with the transistor layout, which has many changes made:
+
+1) simulation. for large designs this requires supercomputers for months and sometimes years to complete the simulation. realistically, only a
+very small number of cycles can be run (several days to run one "clock" cycle).
+
+2) Formal Mathematical "Logical equivalence". this performs boolean logic analysis and takes only hours (or days for very large designs).
+
+it is extremely important for a professional VLSI toolchain to have this capability.
+
+Longer version:
+