Symbolic simulation extends standard digital circuit simulation with symbolic representations of values, covering behaviors of a circuit for all possible instantiations of the symbolic values in a single simulation. Used as a formal verification method, symbolic simulation is algorithmically simple and intuitive, which enables precise analysis and fine-grained mitigation of computational complexity, allowing the method to handle circuits that are above the capacity of most standard formal model checking tools, as well as circuits with highly enmeshed pipelines. Symbolic simulation excels in verification of deep targeted properties of fixed-length pipelines, in particular arithmetic and other datapath circuits. It has been extensively applied in industrial verification of different kinds of integer and floating-point arithmetic circuits, such as adders, multipliers, and fused multiply-adders and dividers. Thanks to repeatable systematic verification strategies for complexity management and mitigation, such verification can be carried out routinely in development projects with rapidly evolving designs. Symbolic simulation is less optimal for verification of general consistency invariants and other inductive properties, as the method does not automate reachable-state analysis and requires a higher degree of human interaction and expertise than standard model checking tools.