Automated Multi-Cycle Symbolic Timing Verification of Microprocessor-based Designs

Timing verification ascertains whether timing checks on components in a circuit are satisfied given component delay models. This paper addresses timing verification of microprocessor-based designs for which previous approaches are shown to be inadequate. It introduces the concept of sequential path tracing - tracing paths through both space and time - that forms the basis of the mtv tool. mtv has the following novel features: unlike previous approaches, it considers sequential behavior together with timing and handles sequential sensitizability and multi-cycle paths automatically; it does not require a predefined clock schedule and can handle circuits with conditional or gated clocks, multiple unrelated clocks, asynchronous set/reset, and power-up initialization; it generates symbolic constraints between timing attributes of components that can be efficiently re-used for small circuit changes or by a synthesis/optimization tool; symbolic constraints also enable common ambiguity removal. Experimental results demonstrate that mtv takes only a few CPU minutes to generate symbolic constraints for each of several microprocessor-based designs.