		Search-engine friendly clone of the ACL2 documentation.

Rv32im-le-states

Read32-xreg-unsigned{0}

Partially evaluate riscv::read-xreg-unsigned for RV32IM little endian.

Definitions and Theorems

Function: read32-xreg-unsigned{0}

(defun read32-xreg-unsigned{0} (riscv::reg riscv::stat)
 (declare
  (xargs
       :guard (and (natp riscv::reg)
                   (riscv::statp riscv::stat)
                   (riscv::featp (feat-rv32im-le))
                   (riscv::stat-validp riscv::stat (feat-rv32im-le))
                   (< (lnfix riscv::reg)
                      (riscv::feat->xnum (feat-rv32im-le))))))
 (let ((riscv::reg (lnfix riscv::reg))
       (riscv::feat (feat-rv32im-le)))
   (if (= riscv::reg 0)
       0
     (unsigned-byte-fix (riscv::feat->xlen riscv::feat)
                        (nth (1- riscv::reg)
                             (riscv::stat->xregs riscv::stat))))))

Theorem: read-xreg-unsigned-becomes-read32-xreg-unsigned{0}

(defthm read-xreg-unsigned-becomes-read32-xreg-unsigned{0}
 (implies
  (equal riscv::feat (feat-rv32im-le))
  (equal
      (riscv::read-xreg-unsigned riscv::reg riscv::stat riscv::feat)
      (read32-xreg-unsigned{0} riscv::reg riscv::stat)))
 :rule-classes :rewrite)