		Search-engine friendly clone of the ACL2 documentation.

States64

State64

Fixtype of (unprivileged) processor states.

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

Fields

xregfile — xregfile64
pc — ubyte64
mem — memory64
error — booleanp

This consists of the register file, the program counter (which is an unsigned 64-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

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