Y86-64
Y86-64 is an instruction set architecture described in the cited formal-verification report through its instruction encodings, function-code families, and reference processor implementations. Its standard instruction set includes halt, nop, register and memory moves, arithmetic/logical operations, conditional branches and moves, procedure-call instructions, and stack operations. An iaddq instruction is described separately as optional rather than part of the standard instruction set. [instruction encoding and set]
Instruction encoding and instruction classes
Y86-64 instructions range from one to ten bytes. An instruction consists of a one-byte instruction specifier and may also include a one-byte register specifier and an eight-byte constant word. [instruction encoding and set]
The standard instruction forms shown in the report are:
haltandnoprrmovq,irmovq,rmmovq, andmrmovqOPqjXXcmovXXcallandretpushqandpopq[instruction encoding and set]
Several instruction forms are families selected by a function-code field. OPq covers addq, subq, andq, and xorq; jXX covers branch conditions including jmp, jle, jl, je, jne, jge, and jg; and cmovXX covers conditional moves including rrmovq, cmovle, cmovl, cmove, cmovne, cmovge, and cmovg. [function-code families]
Stack and procedure-call behavior is explicit in the ISA description. popq reads the top word on the stack and then increments the stack pointer by eight. call pushes the return address onto the stack and jumps to the destination, while ret pops the return address from the stack and jumps to that location. [stack and procedure calls]
The optional iaddq instruction adds an immediate value to the value in its destination register. The report describes it as outside the standard Y86-64 instruction set and as implemented by one Y86-64 variant. [optional iaddq]
Design characteristics
The report identifies several CISC-like features in Y86-64: variable-length instruction encodings, arithmetic and logical instructions that set condition codes as a side effect, condition-code-controlled conditional branches and conditional moves, pushq and popq instructions that both access memory and alter register values, and a procedure-call mechanism that uses the stack to save the return pointer. [CISC-like features]
It also identifies simplifying features commonly associated with RISC instruction sets: arithmetic and logical instructions operate only on register data, the ISA supports only simple base-plus-displacement addressing, and instruction bit encodings are simple and use fields consistently across multiple instructions. [RISC-like simplifications]
SEQ sequential implementation
SEQ is a sequential implementation of the Y86-64 ISA in which each execution cycle carries out the complete execution of a single instruction. Its only state elements are those holding Y86-64 architectural state, and its datapath includes functional blocks for instruction decoding, PC incrementing, and arithmetic/logical operations. Its control logic is described in HCL, a simple language for describing control logic. [SEQ implementation]
During a SEQ cycle, execution begins from the current program-counter value: ten bytes are fetched from memory, the next sequential instruction address is computed by incrementing the PC, up to two register-file values are read, the ALU operates on register values, immediate data, or constants, data memory may be read or written, and the PC is finally set to the next instruction address, branch target, or return address read from memory. [SEQ cycle flow]
PIPE pipelined implementation and variants
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 be in flight at once, each in a different stage. Additional data connections and control logic handle data and control hazards between instructions. [PIPE implementation]
The report describes seven PIPE variants. The standard STD variant handles execute-stage argument hazards by forwarding into the decode stage, stalls for one cycle on load/use hazards, stalls for three cycles for ret, and predicts branches as taken with up to two instructions canceled on misprediction. FULL implements the optional iaddq instruction and is verified against a SEQ variant that also implements it. [PIPE standard and FULL variants]
Other PIPE variants alter forwarding, prediction, or register-file behavior. STALL uses no data forwarding and instead stalls decode for up to three cycles when a later pipeline instruction imposes a data hazard. NT predicts branches as not taken unless unconditional. BTFNT predicts backward branches as taken and forward branches as not taken unless unconditional. LF adds a forwarding path from data-memory output to the pipeline register feeding data-memory input, allowing some load/use hazards to be resolved by forwarding. SW simplifies the register file to a single write port and splits popq execution into two cycles. [PIPE other variants]
Verification context
In the cited verification work, SEQ serves as the reference version of the Y86-64 ISA. The verification flow extracts control logic directly from HCL descriptions and can generate UCLID5 files with different modeling and verification choices. [verification setup]