		Search-engine friendly clone of the ACL2 documentation.

States32

Model of states for RV32I.

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

Write32-xreg: Write a 32-bit integer to an x register.
Write32-mem-ubyte16-lendian: Write an unsigned 16-bit little endian integer to memory.
State32: Fixtype of (unprivileged) processor states.
Xregfile32: Fixtype of the x register file [ISA:2.1].
Memory32: Fixtype of memories [ISA:1.4].
Write32-mem-ubyte32-lendian: Write an unsigned 32-bit little endian integer to memory.
Write32-pc: Write the program counter.
Write32-mem-ubyte8: Write an unsigned 8-bit integer to memory.
Read32-mem-ubyte16-lendian: Read an unsigned 16-bit little endian integer from memory.
Read32-mem-ubyte8: Read an unsigned 8-bit integer from memory.
Read32-mem-ubyte32-lendian: Read an unsigned 32-bit little endian integer from memory.
Read32-xreg-unsigned: Read an unsigned 32-bit integer from an x register.
Read32-xreg-signed: Read a signed 32-bit integer from an x register.
Inc32-pc: Increment the program counter.
Read32-pc: Read the program counter.
Error32p: Check if the error flag in the state is set.
Error32: Set the error flag in the state.
*mem32-size*: Size of (the address space of) the memory [ISA:1.4].