Early formal verification of conditional coverage points to identify intrinsically hard-to-verify logic

Design verification of complex digital circuits typically starts only after the register-transfer level (RTL) description is complete. This frequently makes verification more difficult than necessary because logic that is intrinsically hard to verify, such as memories, counters and deep first-in, first-out (FIFO) structures, becomes immutable in the design. This paper proposes a new approach that exploits formal verification of conditional coverage points with the goal of early identification of hard-to-verify logic. We use the difficulty of formal verification problems as an early estimator of the verification complexity of a design. While traditional verification methods consider conditional coverage only in the design verification phase, we describe an approach that uses conditional coverage at a much earlier stage---the design phase, during which changes to the RTL code are still possible. The method is illustrated using real examples from the verification of an ASIC designed for a specialized supercomputer.