		Search-engine friendly clone of the ACL2 documentation.

States32

State32

Fixtype of (unprivileged) processor states.

This is a product type introduced by fty::defprod.

Fields

xregfile — xregfile32
pc — ubyte32
mem — memory32
error — booleanp

This consists of the register file, the program counter (which is an unsigned 32-bit integer, addressing the memory space), and the memory. We also include a flag that is set when there is an error; this is an artifact of the model, not part of the RISC-V standard.

Subtopics

State32p: Recognizer for state32 structures.
State32-fix: Fixing function for state32 structures.
State32-equiv: Basic equivalence relation for state32 structures.
Make-state32: Basic constructor macro for state32 structures.
State32->xregfile: Get the xregfile field from a state32.
Change-state32: Modifying constructor for state32 structures.
State32->error: Get the error field from a state32.
State32->pc: Get the pc field from a state32.
State32->mem: Get the mem field from a state32.