Sequential Reference Model (SEQ)
ConceptSEQ 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.
First seen 5/26/2026
Last seen 5/26/2026
Evidence 5 chunks
Wiki v1
WIKI
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
NEIGHBORHOOD
No graph connections found for this entity yet. It may appear in future ingestion runs.
explore full graph →RELATIONSHIPS
5 connectionsSEQ is the sequential reference implementation of the Y86-64 ISA.
Verification checks that PIPE and SEQ are functionally equivalent for all possible programs.
The ISA describes a sequential model of processing that SEQ implements as its reference.
The Bryant-O'Hallaron textbook introduces SEQ as the sequential reference model for Y86-64.
The control logic for SEQ is described in HCL.
CITATIONS
10 sources10 citations — click to expand
[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