		Search-engine friendly clone of the ACL2 documentation.

Semantics64

Exec64-mulhsu

Semanics of the MULHSU instruction [ISA:13.1].

Signature
(exec64-mulhsu rd rs1 rs2 stat) → new-stat
Arguments: rd — Guard (ubyte5p rd).; rs1 — Guard (ubyte5p rs1).; rs2 — Guard (ubyte5p rs2).; stat — Guard (state64p stat).
Returns: new-stat — Type (state64p new-stat).

We read a signed 64-bit integer from rs1 and an unsigned 64-bit integer from rs2. We multiply them, we shift the product right by 64 bits, and we write the result to rd. We increment the program counter.

Definitions and Theorems

Function: exec64-mulhsu

(defun exec64-mulhsu (rd rs1 rs2 stat)
  (declare (xargs :guard (and (ubyte5p rd)
                              (ubyte5p rs1)
                              (ubyte5p rs2)
                              (state64p stat))))
  (let ((__function__ 'exec64-mulhsu))
    (declare (ignorable __function__))
    (b* ((rs1-operand (read64-xreg-signed rs1 stat))
         (rs2-operand (read64-xreg-unsigned rs2 stat))
         (product (* rs1-operand rs2-operand))
         (result (ash product 64))
         (stat (write64-xreg rd result stat))
         (stat (inc64-pc stat)))
      stat)))

Theorem: state64p-of-exec64-mulhsu

(defthm state64p-of-exec64-mulhsu
  (b* ((new-stat (exec64-mulhsu rd rs1 rs2 stat)))
    (state64p new-stat))
  :rule-classes :rewrite)

Theorem: exec64-mulhsu-of-ubyte5-fix-rd

(defthm exec64-mulhsu-of-ubyte5-fix-rd
  (equal (exec64-mulhsu (ubyte5-fix rd)
                        rs1 rs2 stat)
         (exec64-mulhsu rd rs1 rs2 stat)))

Theorem: exec64-mulhsu-ubyte5-equiv-congruence-on-rd

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

Theorem: exec64-mulhsu-of-ubyte5-fix-rs1

(defthm exec64-mulhsu-of-ubyte5-fix-rs1
  (equal (exec64-mulhsu rd (ubyte5-fix rs1)
                        rs2 stat)
         (exec64-mulhsu rd rs1 rs2 stat)))

Theorem: exec64-mulhsu-ubyte5-equiv-congruence-on-rs1

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

Theorem: exec64-mulhsu-of-ubyte5-fix-rs2

(defthm exec64-mulhsu-of-ubyte5-fix-rs2
  (equal (exec64-mulhsu rd rs1 (ubyte5-fix rs2)
                        stat)
         (exec64-mulhsu rd rs1 rs2 stat)))

Theorem: exec64-mulhsu-ubyte5-equiv-congruence-on-rs2

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

Theorem: exec64-mulhsu-of-state64-fix-stat

(defthm exec64-mulhsu-of-state64-fix-stat
  (equal (exec64-mulhsu rd rs1 rs2 (state64-fix stat))
         (exec64-mulhsu rd rs1 rs2 stat)))

Theorem: exec64-mulhsu-state64-equiv-congruence-on-stat

(defthm exec64-mulhsu-state64-equiv-congruence-on-stat
  (implies (state64-equiv stat stat-equiv)
           (equal (exec64-mulhsu rd rs1 rs2 stat)
                  (exec64-mulhsu rd rs1 rs2 stat-equiv)))
  :rule-classes :congruence)