		Search-engine friendly clone of the ACL2 documentation.

Rv64im

States64

Model of states for RV64IM.

Along with the model of states, we define some operations on the states.

Subtopics

Write64-xreg: Write a 64-bit integer to an x register.
Write64-xreg-32: Write an integer to the low 32 bits of an x register, sign-extending it to the high 32 bits of the register.
Write64-mem-ubyte64-lendian: Write an unsigned 64-bit little endian integer to memory.
Write64-mem-ubyte16-lendian: Write an unsigned 16-bit little endian integer to memory.
Xregfile64: Fixtype of the x register file [ISA:2.1].
State64: Fixtype of (unprivileged) processor states.
Memory64: Fixtype of memories [ISA:1.4].
Write64-mem-ubyte32-lendian: Write an unsigned 32-bit little endian integer to memory.
Write64-pc: Write the program counter.
Read64-mem-ubyte64-lendian: Read an unsigned 64-bit little endian integer from memory.
Read64-mem-ubyte16-lendian: Read an unsigned 16-bit little endian integer from memory.
Write64-mem-ubyte8: Write an unsigned 8-bit integer to memory.
Read64-xreg-unsigned: Read an unsigned 64-bit integer from an x register.
Read64-mem-ubyte32-lendian: Read an unsigned 32-bit little endian integer from memory.
Read64-mem-ubyte8: Read an unsigned 8-bit integer from memory.
Read64-xreg-unsigned32: Read an unsigned 32-bit integer from the low bits of an x register.
Read64-xreg-signed32: Read a signed 32-bit integer from the low bits of an x register.
Read64-xreg-signed: Read a signed 64-bit integer from an x register.
Inc64-pc: Increment the program counter.
Read64-pc: Read the program counter.
Error64p: Check if the error flag in the state is set.
Error64: Set the error flag in the state.
*mem64-size*: Size of (the address space of) the memory [ISA:1.4].