Timing verification of microprocessor-based designs
Anurag Gupta · 1994
Timing verification ascertains whether setup/hold checks on components in a circuit are satisfied given component delays. This thesis addresses timing verification of microprocessor-based designs, where each component is modeled by its bus-interface state machine and min-max delays between pins. For these circuits, previous approaches are inadequate since they do not reason with sequential behavior and hence cannot automatically handle multi-cycle paths--paths that are allowed more than one clock cycle to propagate--and do not prune sequentially unsensitizable false paths. Reasoning about sequential behavior is particularly difficult since these circuits have multiple clocks without a predefined clock schedule, gated clocks, asynchronous set and clear, and complex power-up initialization sequences. MTV, a Multi-cycle Timing Verification approach that addresses these limitations, has been developed. MTV uses sequential path tracing--tracing paths through space and time, i.e. looking beyond the storage elements to the previous state. Another unique feature is that MTV generates constraints relating symbolic delays; these constraints must be satisfied when numeric values are substituted for the symbolic delays. The symbolic constraints can be re-used while exploring component alternatives during synthesis. MTV includes two major subtasks: (1) Circuit behavior, represented as a trigger-based state transition graph (STG), is generated by exhaustive trigger-based simulation of components modeled as event-based finite state machines. This approach essentially extends STG generation using cycle simulation of fully synchronous designs to general circuits with timing-dependent logic behavior. (2) Sequential paths are traced in this graph to generate constraints for each check. Delays between transitions in the graph automatically account for multi-cycle paths. Also, only sequentially sensitizable paths are traced, since the graph is generated by simulation from the reset state. MTV has been implemented in a tool that has been demonstrated to work correctly on several designs based on the Motorola 6809, Intel 8085, and Intel 80188 microprocessors. MTV takes just a few CPU minutes for these designs. Experimental results show that the worst case exponential growth in STG size and computational complexity does not occur; in fact, the complexity grows linearly with most circuit attributes and hence MTV can be applicable to larger designs also.