		Search-engine friendly clone of the ACL2 documentation.

Specialized-rv64im-le

Rv64im-le-states

Specialization of states to RV64IM little endian.

We define a recognizer for the valid states for RV64IM little endian; in our current model, the states do not depend on (the presence of absence of) the M extension or on the endianness. It remains to introduce the isomorphism between this recognizer and our model of specialized states.

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.
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-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.
Write64-pc: Write the program counter.
Write64-mem-ubyte32-lendian: Write an unsigned 32-bit little endian integer to memory.
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.
Read64-xreg-unsigned: Read an unsigned 64-bit integer from an x register.
Read64-mem-ubyte8: Read an unsigned 8-bit integer from memory.
Read64-mem-ubyte32-lendian: Read an unsigned 32-bit little endian integer from memory.
Read64-xreg-unsigned32: Read an unsigned 32-bit integer from the low bits of an x register.
Write64-mem-ubyte8: Write an unsigned 8-bit integer to memory.
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.
Stat-rv64im-le-p: Recognizer of states for RV64IM little endian.
*mem64-size*: Size of (the address space of) the memory [ISA:1.4].