		Search-engine friendly clone of the ACL2 documentation.

Rv32im-le-states

Read32-xreg-signed{1}

Simplify read32-xreg-signed{0} after partial evaluation.

We assume the guard so that we can replace XLEN with 32.

Definitions and Theorems

Function: read32-xreg-signed{1}

(defun read32-xreg-signed{1} (riscv::reg riscv::stat)
 (declare
    (xargs :guard (and (natp riscv::reg)
                       (riscv::statp riscv::stat)
                       (riscv::stat-validp riscv::stat
                                           '((riscv::base :rv32i)
                                             (riscv::endian :little)
                                             (riscv::m . t)))
                       (< (nfix riscv::reg) 32))))
 (logext 32
         (riscv::read-xreg-unsigned riscv::reg riscv::stat
                                    '((riscv::base :rv32i)
                                      (riscv::endian :little)
                                      (riscv::m . t)))))

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

(defthm read32-xreg-signed{0}-becomes-read32-xreg-signed{1}
  (implies (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))))
           (equal (read32-xreg-signed{0} riscv::reg riscv::stat)
                  (read32-xreg-signed{1} riscv::reg riscv::stat))))