		Search-engine friendly clone of the ACL2 documentation.

Semantics32

Exec32-sltu

Semantics of the SLTU instruction [ISA:2.4.2].

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

We read two unsigned 32-bit integers from rs1 and rs2. We compare the two unsigned integers: if the first one is less than the second, the result is 1, otherwise it is 0. We write the result to rd. We increment the program counter.

Definitions and Theorems

Function: exec32-sltu

(defun exec32-sltu (rd rs1 rs2 stat)
  (declare (xargs :guard (and (ubyte5p rd)
                              (ubyte5p rs1)
                              (ubyte5p rs2)
                              (state32p stat))))
  (let ((__function__ 'exec32-sltu))
    (declare (ignorable __function__))
    (b* ((rs1-operand (read32-xreg-unsigned rs1 stat))
         (rs2-operand (read32-xreg-unsigned rs2 stat))
         (result (if (< rs1-operand rs2-operand) 1 0))
         (stat (write32-xreg rd result stat))
         (stat (inc32-pc stat)))
      stat)))

Theorem: state32p-of-exec32-sltu

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem: exec32-sltu-of-state32-fix-stat

(defthm exec32-sltu-of-state32-fix-stat
  (equal (exec32-sltu rd rs1 rs2 (state32-fix stat))
         (exec32-sltu rd rs1 rs2 stat)))

Theorem: exec32-sltu-state32-equiv-congruence-on-stat

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