		Search-engine friendly clone of the ACL2 documentation.

Rv32im-le-states

Read32-xreg-signed{0}

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

Definitions and Theorems

Function: read32-xreg-signed{0}

(defun read32-xreg-signed{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))))))
 (logext (riscv::feat->xlen (feat-rv32im-le))
         (riscv::read-xreg-unsigned riscv::reg
                                    riscv::stat (feat-rv32im-le))))

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

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