		Search-engine friendly clone of the ACL2 documentation.

Rv32im-le-semantics

Exec32-mulh

Semantics of the MULH instruction [ISA:12.1].

Signature
(exec32-mulh rd rs1 rs2 stat) → new-stat
Arguments: rd — Guard (ubyte5p rd).; rs1 — Guard (ubyte5p rs1).; rs2 — Guard (ubyte5p rs2).; stat — Guard (stat32p stat).
Returns: new-stat — Type (stat32p new-stat).

We read two signed 32-bit integers from rs1 and rs2. We multiply them, we shift the product right by 32 bits, and we write the result to rd. We increment the program counter.

Definitions and Theorems

Function: exec32-mulh

(defun exec32-mulh (rd rs1 rs2 stat)
  (declare (xargs :guard (and (ubyte5p rd)
                              (ubyte5p rs1)
                              (ubyte5p rs2)
                              (stat32p stat))))
  (b* ((rs1-operand (read32-xreg-signed rs1 stat))
       (rs2-operand (read32-xreg-signed rs2 stat))
       (product (* rs1-operand rs2-operand))
       (result (ash product 32))
       (stat (write32-xreg rd result stat))
       (stat (inc32-pc stat)))
    stat))

Theorem: stat32p-of-exec32-mulh

(defthm stat32p-of-exec32-mulh
  (b* ((new-stat (exec32-mulh rd rs1 rs2 stat)))
    (stat32p new-stat))
  :rule-classes :rewrite)

Theorem: exec32-mulh-of-ubyte5-fix-rd

(defthm exec32-mulh-of-ubyte5-fix-rd
  (equal (exec32-mulh (ubyte5-fix rd)
                      rs1 rs2 stat)
         (exec32-mulh rd rs1 rs2 stat)))

Theorem: exec32-mulh-ubyte5-equiv-congruence-on-rd

(defthm exec32-mulh-ubyte5-equiv-congruence-on-rd
  (implies (ubyte5-equiv rd rd-equiv)
           (equal (exec32-mulh rd rs1 rs2 stat)
                  (exec32-mulh rd-equiv rs1 rs2 stat)))
  :rule-classes :congruence)

Theorem: exec32-mulh-of-ubyte5-fix-rs1

(defthm exec32-mulh-of-ubyte5-fix-rs1
  (equal (exec32-mulh rd (ubyte5-fix rs1)
                      rs2 stat)
         (exec32-mulh rd rs1 rs2 stat)))

Theorem: exec32-mulh-ubyte5-equiv-congruence-on-rs1

(defthm exec32-mulh-ubyte5-equiv-congruence-on-rs1
  (implies (ubyte5-equiv rs1 rs1-equiv)
           (equal (exec32-mulh rd rs1 rs2 stat)
                  (exec32-mulh rd rs1-equiv rs2 stat)))
  :rule-classes :congruence)

Theorem: exec32-mulh-of-ubyte5-fix-rs2

(defthm exec32-mulh-of-ubyte5-fix-rs2
  (equal (exec32-mulh rd rs1 (ubyte5-fix rs2)
                      stat)
         (exec32-mulh rd rs1 rs2 stat)))

Theorem: exec32-mulh-ubyte5-equiv-congruence-on-rs2

(defthm exec32-mulh-ubyte5-equiv-congruence-on-rs2
  (implies (ubyte5-equiv rs2 rs2-equiv)
           (equal (exec32-mulh rd rs1 rs2 stat)
                  (exec32-mulh rd rs1 rs2-equiv stat)))
  :rule-classes :congruence)

Theorem: exec32-mulh-of-stat32-fix-stat

(defthm exec32-mulh-of-stat32-fix-stat
  (equal (exec32-mulh rd rs1 rs2 (stat32-fix stat))
         (exec32-mulh rd rs1 rs2 stat)))

Theorem: exec32-mulh-stat32-equiv-congruence-on-stat

(defthm exec32-mulh-stat32-equiv-congruence-on-stat
  (implies (stat32-equiv stat stat-equiv)
           (equal (exec32-mulh rd rs1 rs2 stat)
                  (exec32-mulh rd rs1 rs2 stat-equiv)))
  :rule-classes :congruence)