		Search-engine friendly clone of the ACL2 documentation.

Semantics-equivalences

Exec-andi-alt-defs

Equivalent semantic definitions of ANDI.

Definitions and Theorems

Theorem: exec-andi-alt-def-signed-signed

(defthm exec-andi-alt-def-signed-signed
  (equal (exec-andi rd rs1 imm stat feat)
         (b* ((rs1-operand (read-xreg-signed (ubyte5-fix rs1)
                                             stat feat))
              (imm-operand (logext 12 (ubyte12-fix imm)))
              (result (logand rs1-operand imm-operand))
              (stat (write-xreg (ubyte5-fix rd)
                                result stat feat))
              (stat (inc4-pc stat feat)))
           stat)))

Theorem: exec-andi-alt-def-unsigned-signed

(defthm exec-andi-alt-def-unsigned-signed
  (equal (exec-andi rd rs1 imm stat feat)
         (b* ((rs1-operand (read-xreg-unsigned (ubyte5-fix rs1)
                                               stat feat))
              (imm-operand (logext 12 (ubyte12-fix imm)))
              (result (logand rs1-operand imm-operand))
              (stat (write-xreg (ubyte5-fix rd)
                                result stat feat))
              (stat (inc4-pc stat feat)))
           stat)))

Theorem: exec-andi-alt-def-signed-unsigned

(defthm exec-andi-alt-def-signed-unsigned
  (equal (exec-andi rd rs1 imm stat feat)
         (b* ((rs1-operand (read-xreg-signed (ubyte5-fix rs1)
                                             stat feat))
              (imm-operand (loghead (feat->xlen feat)
                                    (logext 12 (ubyte12-fix imm))))
              (result (logand rs1-operand imm-operand))
              (stat (write-xreg (ubyte5-fix rd)
                                result stat feat))
              (stat (inc4-pc stat feat)))
           stat)))