		Search-engine friendly clone of the ACL2 documentation.

States32

Model of states for RV32IM.

Along with the model of states, which we take from states32i, 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.
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-xreg-unsigned: Read an unsigned 32-bit integer from an x register.
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-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.