| Because of the large size of industrial designs, modern sequential logic synthesis and formal verification techniques cannot afford to accurately characterize the state space of a design. This limits the ability to both optimize designs and to formally prove the designs behave as required.;Invariants are properties that hold in all reachable states. They can be generated in an automated manner, and the set of generated invariants provides a characterization of the design's state space. This characterization can be utilized sequential logic synthesis and formal verification.;In total, this thesis provides (1) a framework to efficiently generate invariants, (2) extensions to sequential logic synthesis to make it more capable of reducing the size of complex designs, and (3) extensions to formal verification to increase its scalability on complex industrial designs. |
