Symbolic multi-level verification of refinement

VLSI-system design can, in general, be characterized in terms of the step-wise refinement of intermediate solutions. Despite the fact that suck refinements usually no not preserve time-scales, current formal verification approaches mostly. start from the assumption that both specification and implementation utilize the same scales of time. Realizing the importance of being able to cope with differences in timing granularity this preliminary paper proposes a symbolic methodology to verify that a low-level finite state machine is a refinement of a high-level finite state machine To illustrate aw approach, the step-M ise refinement - and verification - of a simple microprocessor is presented.