Model Checking Multi-Cycle Paths
Supervisor
Suitable for
Abstract
Accurate timing analysis is crucial for obtaining the optimal clock frequency, and for other design stages such as power analysis. Most methods for estimating propagation delay identify multi-cycle paths (MCPs), which allow timing to be relaxed, but ignore the set of reachable states, achieving scalability at the cost of a severe lack of precision. Even simple circuits contain paths affecting timing that can only be detected if the set of reachable states is considered.
The goal of this project is to evaluate different methods for checking safety properties that identify MCPs. We plan to evaluate Craig Interpolation, Bounded Model Checking, and BDD-based Model Checking.