BMC for Multi-Clock Systems

Current System-on-Chip (SoC) designs are essentially multi-clock systems with multiple clock domains, gated clocks, and latches. Further, the intellectual property (IP) blocks building SoC, with their own clock generators, mandate the requirement for synchronous primitives between the resulting asynchronous clock domains. To meet the high performance and low power requirements [183], multi-clock systems have become the norm of current designs, taking over the single global clock synchronous designs. Routing single clock over a large die incurs large skew delays, unacceptable for high-performance designs. With low power stringent requirements, it is difficult to reduce the clock skews for a distributed clock simply by increasing the power of the clock drivers. For power-conscious designs, designers often use gated clocks to reduce or disable the switching activity of certain portions of the design. Each of these design styles increases the verification complexity in terms of increased number of state bits and deeper bug traces. The following design features and specification of clocked systems pose additional challenges to the existing verification efforts.