Stat
Fixtype of machine states.
This is a product type introduced by fty::defprod.
Fields
- xregs
- pc
- memory — ubyte8-list
- error — booleanp
This captures all possible states for all possible features.
Restrictions based on features are formalized in stat-validp.
The processor state always includes the x<i> registers,
whose number and size depends on the choice of base.
The size in bits is XLEN [ISA:1.3],
which is 32 in RV32I/RV32E, or 64 in RV64I/RV64E;
it is 128 in the upcoming RV128I [ISA:5].
The number of registers is 32 or 16,
based on whether the base is RV32I/RV64I or RV32R/RV64E.
In stat-validp,
we constrain this state component to be
a list of appropriate type and appropriate length;
thus, here we do not need to constrain it at all.
The program counter pc has the same size XLEN
as the x registers.
In stat-validp,
we constrain this state component to be
an integer in the appropriate range;
thus, here we do not need to constrain it at all.
The memory component models the whole addressable space,
which consists of 2^XLEN bytes [ISA:1.4].
We generically define it as a list of bytes here;
in stat-validp, we constrain its length.
RISC-V extensions may require the extension of this fixtype,
with more components that support those extensions.
We will do that as we model those extensions,
which also requires extending the features.
We also include a boolean flag that says whether an error has occurred.
This does not exist in the real machine;
it is just a modeling convenience.
We may refine this boolean flag into some richer data type.
Subtopics
- Stat-fix
- Fixing function for stat structures.
- Stat-equiv
- Basic equivalence relation for stat structures.
- Make-stat
- Basic constructor macro for stat structures.
- Change-stat
- Modifying constructor for stat structures.
- Stat->memory
- Get the memory field from a stat.
- Stat->error
- Get the error field from a stat.
- Statp
- Recognizer for stat structures.
- Stat->xregs
- Get the xregs field from a stat.
- Stat->pc
- Get the pc field from a stat.
