Specialized-features
Specialized features.
We define constants (nullary functions)
for various combinations of features.
We disable their executable counterparts, to maintain the abstraction.
We enable them only where needed in proofs.
Subtopics
- Feat-rv64im-le
- Features for RV64IM, with little endian memory.
- Feat-rv64em-le
- Features for RV64EM, with little endian memory.
- Feat-rv32im-le
- Features for RV32IM, with little endian memory.
- Feat-rv32i-le
- Features for RV32I, with little endian memory.
- Feat-rv32em-le
- Features for RV32EM, with little endian memory.
- Feat-rv64im-be
- Features for RV64IM, with big endian memory.
- Feat-rv64i-le
- Features for RV64I, with little endian memory.
- Feat-rv64i-be
- Features for RV64I, with big endian memory.
- Feat-rv64em-be
- Features for RV64EM, with big endian memory.
- Feat-rv64e-le
- Features for RV64E, with little endian memory.
- Feat-rv64e-be
- Features for RV64E, with big endian memory.
- Feat-rv32im-be
- Features for RV32IM, with big endian memory.
- Feat-rv32i-be
- Features for RV32I, with big endian memory.
- Feat-rv32em-be
- Features for RV32EM, with big endian memory.
- Feat-rv32e-le
- Features for RV32E, with little endian memory.
- Feat-rv32e-be
- Features for RV32E, with big endian memory.
