Verifying Nondeterministic Implementations of Deterministic Systems

Some modern systems with a simple deterministic high-level specification have implementations that exhibit highly nondeterministic behavior. Such systems maintain a simple operation semantics at the high-level. However their underlying implementations exploit parallelism to enhance performance leading to interaction among operations and contention for resources. The deviation from the sequential execution model not only leads to nondeterminism in the implementation but creates the potential for serious design errors. This paper presents a methodology for formal verification of such systems. An abstract specification describes the high-level behavior as a set of operations. A mapping relates the sequential semantics of these operations to the underlying nondeterminism in the implementation. Symbolic Trajectory Evaluation, a modified form of symbolic simulation, is used to perform the actual verification. The methodology is currently being used to verify portions of a superscalar processor which implements the PowerPC architecture. Our initial work on the fixed point unit indicates that this is a promising approach for verification of processors.