Overview
Y86-64 is an instruction set presented in the Bryant–O’Hallaron textbook, together with a pipelined implementation of a Y86-64 processor. The same textbook also defines homework modifications to that pipeline, yielding seven pipeline variants used in a formal-verification study. [Y86-64 instruction set and variants]
Programmer-visible state
The Y86-64 programmer-visible state is described as analogous to x86-64 in that programs access and modify the program registers, the condition codes, the program counter (PC), and data memory. The architecture also includes an exception status word for exceptional conditions. [Programmer-visible state]
The register file shown for Y86-64 includes registers such as %rax, %rcx, %rdx, %rbx, %rsp, %rbp, %rsi, %rdi, %r8 through %r14, and RNONE. The condition-code state includes ZF, SF, and OF. [Programmer-visible state]
SEQ: sequential implementation
SEQ is the sequential reference implementation used in the verification work. During a clock cycle, execution begins from the current PC: bytes are fetched from instruction memory, the next sequential address is computed by incrementing the PC, up to two register values are read, the ALU operates on register values, instruction immediate data, or constants, data memory may be read or written, results are written back to registers, and the PC is updated to the next instruction address, a branch target, or a return address read from memory. [SEQ execution flow]
In the verification task, SEQ serves as the reference version of the Y86-64 ISA. The source notes that SEQ could itself be incorrect, but is easier to test by conventional methods such as simulation than the more complex pipelined implementations. [SEQ as reference]
PIPE: pipelined implementation
PIPE is a five-stage pipelined implementation of the Y86-64 instruction set. It partitions computation into stages similar to SEQ and uses the same set of functional blocks, but adds pipeline registers so that up to five instructions can flow through the pipeline simultaneously, each in a different stage. PIPE also requires additional data connections and control logic to handle hazards in which data or control must pass between instructions in the pipeline. [PIPE structure]
The verification study considers seven PIPE variants. The standard implementation, STD, handles execute-stage data hazards by forwarding into the decode stage; it uses a one-cycle decode-stage stall for load/use hazards, a three-cycle stall for ret, and predicts branches as taken, canceling up to two instructions after a misprediction. [PIPE variants]
Other variants modify the baseline design: FULL implements the optional iaddq instruction and is verified against a SEQ variant that also implements it; STALL removes data forwarding and stalls decode for up to three cycles on data hazards; NT predicts branches not taken except for unconditional branches; BTFNT predicts backward branches as taken and forward branches as not taken except for unconditional branches; LF adds a forwarding path from data-memory output to the pipeline register feeding data-memory input; and SW simplifies the register file to a single write port, splitting popq execution into two cycles. [PIPE variants]
Control logic and model generation
The control logic for both SEQ and PIPE is described in HCL, the Hardware Control Language. Existing translators generated C simulation models, Verilog suitable for logic synthesis, and earlier UCLID models from HCL. The verification framework generated UCLID5 models by extracting control logic directly from HCL descriptions, helping maintain consistency among simulation models, synthesizable hardware descriptions, and formal-verification models. [HCL control logic]
The UCLID5 model-generation flow combines HCL control logic with frameworks for functional-block operations and interconnections. Functional-block definitions are kept in a single file and duplicated into the two processor models to keep them consistent. The generated processor models are merged with common data types, an overall system model, and a verification script; model and verification options select a concrete verification task. [UCLID5 generation]
Formal verification task
The verification task is to determine whether SEQ and all seven PIPE variants are functionally equivalent. This is simplified because SEQ and PIPE share many functional elements, including instruction decoding logic and the ALU; they differ in PIPE’s additional pipeline registers and pipeline-specific control logic. [Functional equivalence task]
UCLID5 generates verification conditions from a model and verification script, expresses them as formulas over supported theories, and invokes an SMT solver. In the cited work, the Z3 solver was used. The SMT solver may report the negated verification condition unsatisfiable, indicating that the desired condition holds; satisfiable, producing concrete values that UCLID5 uses to build a counterexample; or indeterminate, indicating that it could neither find a satisfying solution nor prove unsatisfiability. [UCLID5 verification process]