Formal verification applies mathematical logic to exhaustively analyze hardware design behavior without relying on traditional stimulus generation. Using assertions to define expected behavior, the process automatically proves or refutes these properties using symbolic solvers. This approach uncovers hard-to-reach bugs, unreachable states, and deadlocks across all legal execution paths, enhancing design reliability and reducing simulation blind spots. The verification flow translates RTL into a symbolic state-transition model and applies synthesized checkers to explore legal state sequences. Proof outcomes are classified as proven, falsified (with counterexample), or inconclusive due to complexity. Successful application depends on effective property definition, design abstraction, and solver capability. Supporting elements include assertion checkers, environmental constraints, binding logic, and coverage tracking mechanisms. Managing complexity is essential to enable analysis of large-scale designs. Factors such as state space size, sequential depth, constraint density, and duplication influence proof effort. Techniques like cone-of-influence pruning, abstraction, property slici...