		Search-engine friendly clone of the ACL2 documentation.

Semantics-equivalences

Exec-add-alt-defs

Equivalent semantic definitions of ADD.

Definitions and Theorems

Theorem: exec-add-alt-def-signed-signed

(defthm exec-add-alt-def-signed-signed
  (equal (exec-add rd rs1 rs2 stat feat)
         (b* ((rs1-operand (read-xreg-signed (ubyte5-fix rs1)
                                             stat feat))
              (rs2-operand (read-xreg-signed (ubyte5-fix rs2)
                                             stat feat))
              (result (+ rs1-operand rs2-operand))
              (stat (write-xreg (ubyte5-fix rd)
                                result stat feat))
              (stat (inc4-pc stat feat)))
           stat)))

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

(defthm exec-add-alt-def-unsigned-signed
  (equal (exec-add rd rs1 rs2 stat feat)
         (b* ((rs1-operand (read-xreg-unsigned (ubyte5-fix rs1)
                                               stat feat))
              (rs2-operand (read-xreg-signed (ubyte5-fix rs2)
                                             stat feat))
              (result (+ rs1-operand rs2-operand))
              (stat (write-xreg (ubyte5-fix rd)
                                result stat feat))
              (stat (inc4-pc stat feat)))
           stat)))

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

(defthm exec-add-alt-def-signed-unsigned
  (equal (exec-add rd rs1 rs2 stat feat)
         (b* ((rs1-operand (read-xreg-signed (ubyte5-fix rs1)
                                             stat feat))
              (rs2-operand (read-xreg-unsigned (ubyte5-fix rs2)
                                               stat feat))
              (result (+ rs1-operand rs2-operand))
              (stat (write-xreg (ubyte5-fix rd)
                                result stat feat))
              (stat (inc4-pc stat feat)))
           stat)))