• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Pfcs
      • Wp-gen
      • Dimacs-reader
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • Taspi
      • Riscv
        • Specification
        • Executable
        • Specialized
          • Specialized-features
            • Feat-rv64im-le
            • Feat-rv64em-le
            • Feat-rv32im-le
            • Feat-rv32em-le
            • Feat-rv64im-be
            • Feat-rv64i-le
            • Feat-rv64i-be
            • Feat-rv64em-be
            • Feat-rv64e-le
            • Feat-rv64e-be
            • Feat-rv32im-be
            • Feat-rv32i-le
            • Feat-rv32i-be
            • Feat-rv32em-be
            • Feat-rv32e-le
            • Feat-rv32e-be
          • Rv64im
          • Rv32im
          • Specialized-states
      • Bitcoin
      • Des
      • Ethereum
      • X86isa
      • Sha-2
      • Yul
      • Zcash
      • Proof-checker-itp13
      • Regex
      • ACL2-programming-language
      • Json
      • Jfkr
      • Equational
      • Cryptography
      • Poseidon
      • Where-do-i-place-my-book
      • Axe
      • Aleo
      • Bigmems
      • Builtins
      • Execloader
      • Solidity
      • Paco
      • Concurrent-programs
      • Bls12-377-curves
    • Debugging
    • Std
    • Community
    • Proof-automation
    • ACL2
    • Macro-libraries
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Specialized

Specialized-features

Specialized features.

We define constants for various combinations of features.

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-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-le
Features for RV32I, with little 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.