This research explores a set of techniques for robust logic synthesis tools to support the design automation of high-performance and low-power sequential synchronous circuits. The approach is based on a new concept of logic timing, which combines retiming with logic optimization across register boundaries into a single efficient optimization technique. Also being explored is state encoding for sequential synthesis of circuits specified as finite state machines. The model is based on a controlled reencoding/retiming of the symbolic representation of the state machine represented initially with one-hot code. This facilitates a reliable estimation of circuit cost, such as delay, power, and sequential testability, as a direct function of the encoding. The proposed work is being carried out in collaboration with Advanced Micro Devices, Inc. of Austin, TX.