Pipeline Consistency Predicate Wiki

Overview

The Pipeline Consistency Predicate is presented as Figure 15 in Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5. It defines a predicate pipe_ok() for checking whether a pipeline state is internally consistent. The predicate is built as a conjunction of stage-level predicates and a return-instruction predicate:

pipe_ok() = D_ok() && E_ok() && M_ok() && W_ok() && ret_ok();

This means that the pipeline is considered consistent only when the decode, execute, memory, and write-back stage predicates all hold, and the return-instruction constraints also hold. [C1]

Stage consistency checks

The visible definitions show that the memory-stage predicate M_ok() constrains combinations of status code, instruction code, and destination registers. For example, when M_stat == SAOK, the memory-stage instruction must not be IHALT or IBAD; when M_stat == SBUB, the destination registers must be RNONE and the instruction code must be INOP; and when M_stat == SHLT, the instruction code must be IHALT. Invalid-instruction and address-error statuses shown for the memory stage also require RNONE destinations and INOP. [C2]

The write-back-stage predicate W_ok() follows the same general pattern for the statuses shown: SAOK excludes IHALT and IBAD; SBUB requires no destination registers and INOP; SHLT requires IHALT; and SINS requires no destination registers and INOP. [C3]

The excerpt also shows execute-stage conditions for invalid-instruction and address-error statuses: both E_stat == SINS and E_stat == SADR imply that E_dstM == RNONE, E_dstE == RNONE, and E_icode == INOP. [C4]

Return-instruction constraints

The helper predicate ret_ok() encodes inter-stage constraints for return instructions. If a return instruction is in the execute stage, the decode stage must be a bubble. If a return instruction is in the memory stage, both decode and execute must be bubbles. If a return instruction is in the write-back stage with status SAOK, then decode, execute, and memory must all be bubbles. [C5]

These constraints rule out pipeline states where a ret instruction is followed too closely by other instructions. The paper explicitly describes such states as inter-instruction inconsistencies, giving the example of a ret instruction followed by other instructions rather than by at least three bubbles. [C6]

Role in restricting initial pipeline states

The paper notes that some models required restrictions on the initial pipeline state. Such restrictions are motivated by the fact that many possible pipeline states would never arise during actual operation. Examples include intra-instruction inconsistency, such as a regular register identifier being present even though the pipeline register contains a nop, and inter-instruction inconsistency involving ret spacing. [C6]

A restriction over pipeline states is expressed as a predicate I. The paper defines such a restriction as a pipeline invariant when it holds under all possible operating conditions. To establish invariance, it must hold in reset states and be preserved by each processor operation. The preservation check is described using the simulation sequence:

Init(P₀), Pipe, SaveP(P₁)

After this sequence, the required proof obligation is:

I(P₀) ⇒ I(P₁)

where SaveP(s) saves all pipeline state elements as state s. [C7]

Related single-write restriction

The same excerpt also presents a separate Pipeline single-write predicate sw_ok() in Figure 16. It requires that, in the execute, memory, and write-back stages, at least one of dstM or dstE is RNONE:

sw_ok() =
   (E_dstM == RNONE || E_dstE == RNONE)
&& (M_dstM == RNONE || M_dstE == RNONE)
&& (W_dstM == RNONE || W_dstE == RNONE);

The paper states that the SW model also requires this restriction on the initial pipeline state. [C8]

Verification significance

The predicate helps exclude impossible pipeline states from verification, but the paper emphasizes that such states can be excluded only if the restriction can also be proven invariant. This creates an additional burden on the verifier: restrictions should be kept simple, because users must formulate them and prove that they are preserved. [C9]