Abstract
The complexity of the instruction set of modern microprocessors often leads to faults in the microinstruction sequencing and timing errors in the implementation of the processor control. These errors are difficult to detect with conventional simulation methods. As an alternative, formal verification uses a mathematical model of the system to verify its correct behavior by constructing a formal proof. Recently we introduced a new partial order formal verification method based on the notion of series-parallel posets. The associated verification algorithms have a low order space- and time complexity, and have been successfully applied to the verification of properties of real-world systems such as the PCI local bus protocol and the MESI cache coherence protocol. In this paper we use series-parallel posets to model and verify the behavior of the DLX microprocessor control.