		Search-engine friendly clone of the ACL2 documentation.

Semantics

Exec-mulhsu

Semanics of the MULHSU instruction [ISA:13.1].

Signature
(exec-mulhsu rd rs1 rs2 stat feat) → new-stat
Arguments: rd — Guard (ubyte5p rd).; rs1 — Guard (ubyte5p rs1).; rs2 — Guard (ubyte5p rs2).; stat — Guard (statp stat).; feat — Guard (featp feat).
Returns: new-stat — Type (statp new-stat).

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

Definitions and Theorems

Function: exec-mulhsu

(defun exec-mulhsu (rd rs1 rs2 stat feat)
  (declare (xargs :guard (and (ubyte5p rd)
                              (ubyte5p rs1)
                              (ubyte5p rs2)
                              (statp stat)
                              (featp feat))))
  (declare (xargs :guard (stat-validp stat feat)))
  (let ((__function__ 'exec-mulhsu))
    (declare (ignorable __function__))
    (b* ((rs1-operand (read-xreg-signed (ubyte5-fix rs1)
                                        stat feat))
         (rs2-operand (read-xreg-unsigned (ubyte5-fix rs2)
                                          stat feat))
         (product (* rs1-operand rs2-operand))
         (result (ash product (feat->xlen feat)))
         (stat (write-xreg (ubyte5-fix rd)
                           result stat feat))
         (stat (inc4-pc stat feat)))
      stat)))

Theorem: statp-of-exec-mulhsu

(defthm statp-of-exec-mulhsu
  (b* ((new-stat (exec-mulhsu rd rs1 rs2 stat feat)))
    (statp new-stat))
  :rule-classes :rewrite)

Theorem: stat-validp-of-exec-mulhsu

(defthm stat-validp-of-exec-mulhsu
  (implies (stat-validp stat feat)
           (b* ((?new-stat (exec-mulhsu rd rs1 rs2 stat feat)))
             (stat-validp new-stat feat))))

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

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

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

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

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

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

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

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

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

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

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

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

Theorem: exec-mulhsu-of-stat-fix-stat

(defthm exec-mulhsu-of-stat-fix-stat
  (equal (exec-mulhsu rd rs1 rs2 (stat-fix stat)
                      feat)
         (exec-mulhsu rd rs1 rs2 stat feat)))

Theorem: exec-mulhsu-stat-equiv-congruence-on-stat

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

Theorem: exec-mulhsu-of-feat-fix-feat

(defthm exec-mulhsu-of-feat-fix-feat
  (equal (exec-mulhsu rd rs1 rs2 stat (feat-fix feat))
         (exec-mulhsu rd rs1 rs2 stat feat)))

Theorem: exec-mulhsu-feat-equiv-congruence-on-feat

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