This research is on a timing verification and optimization framework for designing an entire digital system (e.g. a microprocessor). The research builds on a widely used model for synchronous timing analysis and an efficient method for estimating gate and wire delays. The model is being extended to include relevant functional information in order to enhance accuracy. Components of the framework are: design decomposition to isolate critical elements; a path delay calculator; algorithms for finding synchronizer components; clock analysis algorithms; a symbolic sequential timing verification component; a hybrid timing-logic simulator; and design optimizers.