		Search-engine friendly clone of the ACL2 documentation.

Riscv

States

Model of states.

Currently we have two similar but slightly different models, one for RV32I and one for RV64I. We are in the process of consolidating them into one model for both; towards that end, we also provide a more generic definition of states here.

Subtopics

Stat: Fixtype of machine states.
Stat-validp: Check if a state is valid with respect to given features.
Write-memory-unsigned64: Write an unsigned 64-bit integer to memory.
Write-memory-unsigned32: Write an unsigned 32-bit integer to memory.
Write-memory-unsigned8: Write an unsigned 8-bit integer to memory.
Write-memory-unsigned16: Write an unsigned 16-bit integer to memory.
Read-xreg-unsigned: Read an unsigned integer from an x register.
Write-xreg-32: Write an integer to the low 32 bit of a 64-bit x register, sign-extending to the high 32 bits of the register.
States64: Model of states for RV64I.
Write-xreg: Write an integer to an x register.
Read-memory-unsigned8: Read an unsigned 8-bit integer from memory.
Read-memory-unsigned64: Read an unsigned 64-bit integer from memory.
Read-memory-unsigned32: Read an unsigned 32-bit integer from memory.
Read-memory-unsigned16: Read an unsigned 16-bit integer from memory.
Read-xreg-signed: Read a signed integer from an x register.
Read-xreg-unsigned32: Read an unsigned 32-bit integer from a 64-bit x register.
States32: Model of states for RV32I.
Write-pc: Write the program counter.
Read-xreg-signed32: Read a signed 32-bit integer from a 64-bit x register.
Read-pc: Read the program counter.
Inc4-pc: Increment the program counter by 4.