		Search-engine friendly clone of the ACL2 documentation.

Specialized-rv32im-le

Rv32im-le-states

Specialization of states to RV32IM little endian.

We define a recognizer for the valid states for RV32IM little endian; in our current model, the states do not depend on (the presence of absence of) the M extension or on the endianness. We introduce a fixtype that is isomorphic to that recognizer. We specialize the operations on states to operate on that fixtype. This is work in progress.

Along with the model of states, we define some operations on the states.

Subtopics

Write32-xreg: Write a 32-bit integer to an x register.
Stat32: Fixtype of states for RV32IM little endian.
Write32-mem-ubyte16-lendian: Write an unsigned 16-bit little endian integer to memory.
Memory: Fixtype of memories fo RV32IM little endian.
Xregs: Fixtype of the x registers for RV32IM little endian.
Write32-pc: Write the program counter.
Write32-mem-ubyte32-lendian: Write an unsigned 32-bit little endian integer to memory.
Read32-xreg-unsigned: Read an unsigned 32-bit integer from an x register.
Read32-mem-ubyte16-lendian: Read an unsigned 16-bit little endian integer from memory.
Read32-mem-ubyte8: Read an unsigned 8-bit integer from memory.
Read32-mem-ubyte32-lendian: Read an unsigned 32-bit little endian integer from memory.
Write32-mem-ubyte8: Write an unsigned 8-bit integer to memory.
Stat32-iso: Isomorphism between stat-rv32im-le-p and stat32.
Read32-xreg-unsigned{3}: Simplify read32-xreg-unsigned{2} after the isomorphic state transformation.
Read32-xreg-signed: Read a signed 32-bit integer from an x register.
Inc32-pc: Increment the program counter.
Read32-xreg-signed{3}: Simplify the body of read32-xreg-signed{2} to call read32-xreg-unsigned{3}.
Stat-from-stat32: Convert from stat32 to stat-rv32im-le-p.
Read32-xreg-unsigned{2}: Refine read32-xreg-unsigned{1} to use the isomorphic states stat32.
Read32-xreg-signed{2}: Refine read32-xreg-signed{1} to use the isomorphic states stat32.
Stat-rv32im-le-p: Recognizer of states for RV32IM little endian.
Read32-xreg-signed{4}: Simplify the guard of read32-xreg-signed{3} to eliminate the isomorphic conversion.
Read32-xreg-unsigned{1}: Simplify read32-xreg-unsigned{0} after partial evaluation.
Read32-xreg-signed{1}: Simplify read32-xreg-signed{0} after partial evaluation.
Read32-pc: Read the program counter.
Read32-xreg-unsigned{0}: Partially evaluate riscv::read-xreg-unsigned for RV32IM little endian.
Error32p: Check if the error flag in the state is set.
Error32: Set the error flag in the state.
Stat32-from-stat: Convert from stat-rv32im-le-p to stat32.
Read32-xreg-signed{0}: Partially evaluate riscv::read-xreg-unsigned for RV32IM little endian.
Read-xreg-unsigned-to-read32-xreg-unsigned{3}: Rewriting of riscv::read-xreg-unsigned to read32-xreg-unsigned{3}.