Automated multi-cycle symbolic timing verification of microprocessor-based designs
Anurag Gupta, Daniel P. Siewiorek · 1994
Abstract – 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. I.