Skip to content
STIMSMITH

Sequential Reference Model (SEQ)

Concept WIKI v1 · 5/26/2026

SEQ is the sequential Y86-64 processor model used as a reference implementation of the ISA in verification of pipelined PIPE variants. It represents instruction execution in strict sequential order and is compared against PIPE through Burch-Dill correspondence checking.

Definition

The Sequential Reference Model (SEQ) is the sequential processor model used as the reference version of the Y86-64 ISA in the cited verification framework. The ISA-level specification is based on sequential processing, meaning instructions execute in strict sequential order and define effects on architectural state such as registers, the program counter, and memory. [C1]

Role in verification

In the verification task, SEQ serves as the reference against which the pipelined PIPE implementations are checked for functional equivalence. The work specifically frames the task as determining whether SEQ and seven PIPE variants are functionally equivalent. [C2]

SEQ is easier to test by conventional simulation than the more complex pipelined implementations, although the source notes that SEQ itself could still be incorrect. [C3]

Relationship to PIPE

SEQ and PIPE share functional elements such as instruction decoding logic and the ALU. Their main differences are PIPE's additional pipeline registers and PIPE-specific control logic. [C4]

The verification framework includes control signals that allow PIPE to run in normal or flushing mode, allow SEQ state elements to import corresponding values from PIPE, and allow SEQ to operate. During execution, state variables are captured as UCLID5 variables and assertions are checked over those values. [C5]

Correspondence checking

The cited framework uses a Burch-Dill-style abstraction function, α, that maps a pipeline state to the architectural state obtained after flushing partially executed instructions until they complete. After flushing, the architectural state is transferred to SEQ and saved. [C6]

Correspondence checking compares two symbolic simulation sequences:

  • one sequence performs one PIPE step, flushes the pipeline, and saves the resulting architectural state;
  • the other sequence flushes the same initial PIPE state, transfers the resulting architectural state to SEQ, saves it, executes one SEQ step, and saves the new SEQ state. [C7]

The required correspondence condition is that the architectural state after the PIPE step and flush equals either the state after one SEQ step or the pre-step SEQ state. The first case corresponds to a PIPE cycle that eventually completes an instruction; the second corresponds to a stall or canceled instruction, so the cycle has no architectural effect. [C8]

State compared

The UCLID5 verification condition checks that PIPE operation is consistent with SEQ operation by comparing saved state components including the program counter when appropriate, register file, condition codes, memory, and status. [C9]

Modeling and generation

The control logic for both SEQ and PIPE is described in HCL, the Hardware Control Language. HCL definitions are translated into UCLID5 macro definitions, and shared functional-block definitions are duplicated into the two models to maintain consistency. [C10]

LINKED ENTITIES

1 links
UCLID5 modeled_and_verified_with

CITATIONS

10 sources
10 citations
[1] SEQ is a sequential reference model for the Y86-64 ISA, and ISA semantics are based on strict sequential instruction execution over architectural state including registers, PC, and memory. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[2] The verification task is to determine whether SEQ and seven PIPE variants are functionally equivalent. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[3] SEQ may still be incorrect, but it is easier to test with conventional methods than more complex pipelined implementations. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[4] SEQ and PIPE share functional elements such as instruction decoding logic and the ALU, differing mainly in PIPE's pipeline registers and PIPE-specific control logic. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[5] The framework supports normal/flushing PIPE operation, transfer of PIPE architectural state into SEQ state elements, SEQ operation, and assertion checking over captured UCLID5 variables. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[6] The abstraction function α maps a pipeline state to the architectural state obtained after flushing partially executed instructions and transferring the state to SEQ. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[7] Correspondence checking compares a PIPE-step-then-flush sequence with a flush-transfer-SEQ-step sequence. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[8] The correspondence condition requires the PIPE-derived state to equal either the state after one SEQ step or the pre-step SEQ state, covering completed instructions as well as stalls or canceled instructions. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[9] The UCLID5 verification condition compares state components including PC, register file, condition codes, memory, and status to ensure PIPE operation is consistent with SEQ operation. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[10] SEQ and PIPE control logic is described in HCL and translated into UCLID5, with shared functional-block definitions duplicated into both models for consistency. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5