We describe a methodology for the formal verification of complex
out-of-order pipelines as they may be used as execution units in
out-of-order processors. The pipelines may process multiple
instructions simultaneously, may have branches and cycles in the
pipeline structure, may have variable latency, and may reorder
instructions internally. The methodology combines model-checking for
the verification of the pipeline control, and theorem proving for the
verification of the pipeline functionality. In order to combine both
techniques, we formally verify that the FairCTL operators defined in
mu-calculus match their intended semantics expressed in a form where
computation traces are explicit, since this form is better suited for
theorem proving. This allows the formally safe translation of
model-checked properties of the pipeline control into a
theorem-proving friendly form, which is used for the verification of
the overall correctness, including the functionality. As an example
we prove the correctness of the pipeline of a multiplication/division
floating point unit with all the features mentioned above.
(
geocities.com/de/christian_jacobi) (
geocities.com/de)