		Search-engine friendly clone of the ACL2 documentation.

Instructions

Instr

Fixtype of instructions.

This is a tagged union type, introduced by fty::deftagsum.

The tags of the summands of this fixtype correspond to opcodes. The components of each summand correspond to the non-opcode fields.

The OP-IMM opcode corresponds to :op-imm for non-shift instructions, :op-imms32 for RV32I shift instructions, and :op-imms64 for RV64I shift instructions. They are distinct summands because the formats differ: non-shift instructions use the I-type format; shift instructions use a specialization of the I-type format, but a slightly different one in RV32I vs. RV64I, namely in the number of bits of the shift amount (5 vs. 6).

The OP-IMM-32 opcode corresponds to :op-imm-32 for non-shift instructions, and :op-imms-32 for shift instructions. They are distinct summands because the formats differ: non-shift instructions use the I-type format; shift instructions use a specialization of the I-type format.

The LUI opcode corresponds to :lui.

The AUIPC opcode corresponds to :auipc.

The OP opcode corresponds to :op.

The OP-32 opcode corresponds to :op-32.

The JAL opcode corresponds to :jal.

The JALR opcode corresponds to :jalr.

The BRANCH opcode corresponds to :branch.

The LOAD opcode corresponds to :load.

The STORE opcode corresponds to :store.

Subtopics

Instrp: Recognizer for instr structures.
Instr-fix: Fixing function for instr structures.
Instr-case: Case macro for the different kinds of instr structures.
Instr-store
Instr-op-imms64
Instr-op-imms32
Instr-op-imms-32
Instr-op-imm-32
Instr-op-imm
Instr-op-32
Instr-op
Instr-load
Instr-branch
Instr-equiv: Basic equivalence relation for instr structures.
Instr-jalr
Instr-lui
Instr-jal
Instr-auipc
Instr-kind: Get the kind (tag) of a instr structure.

Instr

Member Tags → Types

Subtopics