Pipeline Consistency Predicate
CodeArtifactThe Pipeline Consistency Predicate is a formal predicate used in verification of pipelined Y86-64 microprocessors. It combines per-stage consistency checks with return-instruction spacing constraints to restrict pipeline states to combinations that can arise during normal operation.
First seen 5/26/2026
Last seen 5/26/2026
Evidence 1 chunks
Wiki v1
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();
NEIGHBORHOOD
No graph connections found for this entity yet. It may appear in future ingestion runs.
explore full graph →RELATIONSHIPS
1 connectionsThe pipeline consistency predicate is part of the UCLID5 model, restricting the initial pipeline state for verification.
CITATIONS
9 sources9 citations — click to expand
[1] The Pipeline Consistency Predicate is Figure 15 and defines pipe_ok as the conjunction of D_ok, E_ok, M_ok, W_ok, and ret_ok. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[2] M_ok constrains memory-stage status, instruction code, and destination registers for SAOK, SBUB, SHLT, SINS, and SADR. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[3] W_ok constrains write-back-stage status, instruction code, and destination registers for the statuses shown in the excerpt. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[4] The execute-stage conditions shown require SINS and SADR to imply RNONE destinations and INOP. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[5] ret_ok requires bubbles behind return instructions in execute, memory, and successful write-back positions. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[6] The paper identifies impossible intra-instruction and inter-instruction states, including a nop with a regular register identifier and a ret followed by instructions rather than at least three bubbles. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[7] A pipeline restriction I is an invariant if it holds in reset states and is preserved by processor operation; preservation is checked with Init(P0), Pipe, SaveP(P1) and proof obligation I(P0) implies I(P1). Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[8] Figure 16 defines the Pipeline single-write predicate sw_ok, and the SW model requires this restriction on the initial pipeline state. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[9] Impossible pipeline states can be excluded by the verifier only if they can be proven unreachable, and the paper recommends keeping restrictions simple because users must formulate and prove them invariant. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5