		Search-engine friendly clone of the ACL2 documentation.

Specification

States

Model of states.

We introduce a model of states, along with operations on those states. We capture all possible states for all possible RISC-V features, but we also introduce a predicate saying when a state is valid with respect to given features.

Subtopics

Stat: Fixtype of machine states.
Stat-validp: Check if a state is valid with respect to given features.
Read-instruction: Read the 32-bit encoding of an instruction from memory.
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.
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.
Read-xreg-unsigned: Read an unsigned integer from an x register.
Write-xreg: Write an integer to an x register.
Read-memory-unsigned64: Read an unsigned 64-bit integer from memory.
Read-memory-unsigned8: Read an unsigned 8-bit integer from memory.
Read-memory-unsigned32: Read an unsigned 32-bit integer from memory.
Read-xreg-signed: Read a signed integer from an x register.
Read-memory-unsigned16: Read an unsigned 16-bit integer from memory.
Read-xreg-unsigned32: Read an unsigned 32-bit integer from a 64-bit x register.
Write-pc: Write the program counter.
Read-xreg-signed32: Read a signed 32-bit integer from a 64-bit x register.
Inc4-pc: Increment the program counter by 4.
Read-pc: Read the program counter.
Errorp: Check if the error flag in the state is set.
Error: Set the error flag in the state.