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-instr
- Read the 32-bit encoding of an instruction from memory.
- Write-mem64
- Write an unsigned 64-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.
- Write-xreg
- Write an integer to an x register.
- Write-mem8
- Write an unsigned 8-bit integer to memory.
- Write-mem32
- Write an unsigned 32-bit integer to memory.
- Write-mem16
- Write an unsigned 16-bit integer to memory.
- Read-mem8
- Read an unsigned 8-bit integer from memory.
- Read-xreg-signed
- Read a signed integer from an x register.
- Read-mem64
- Read an unsigned 64-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-mem32
- Read an unsigned 32-bit integer from memory.
- Read-mem16
- Read an unsigned 16-bit integer from memory.
- 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.