Verification and Synthesis of Clock-Gated Circuit

As system complexity and transistor density increase, the power consumed by digital integrated circuits has become a critical constraint for VLSI design and manufacturing. To reduce dynamic power dissipation, clock-gating synthesis techniques are applied to circuits to prune register updates by modifying the next-state functions of the registers. Hence to verify this kind of synthesis, sequential equivalence checking (SEC) of clock-gated circuits is required.;In this thesis, we examine the application of reverse engineering and control logic extraction to assist in the analysis and verification of clock-gated circuits. The proposed methodology also enables sequential clock-gating synthesis to further reduce dynamic power. A secondary focus is on recognizing circuit functionalities with deep learning techniques.;The first part of the work deals with the use of transparent logic to recognize control and data paths of gated-level circuits. We invent abstraction models (dependencies graphs, DGs) of sequential circuits and then explain how they can be used to formulate sufficient conditions for legal clock-gating. It is then demonstrated how to perform efficient sequential equivalence checking (SEC) between a circuit before and after clock-gating synthesis based on DGs. The proposed formulation is extended to allow sequential clock-gating synthesis to be done systematically and automatically.;The second part of the thesis introduces the use of neural networks to recognize circuit properties, which can be used to benefit and improve reverse engineering methods. We invent a representation of gate-level circuits to work with neural networks and build a framework for circuit recognition, including function classification and detection. The proposed framework can also be used to locate high-level constructs in the sea of logic gates.