		Search-engine friendly clone of the ACL2 documentation.

Missing-parents

Exec-sltiu

Semantics of the SLTIU instruction [ISA:2.4.1].

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

We read an unsigned XLEN-bit integer from rs1. We sign-extend the 12-bit immediate to XLEN bits, obtaining an unsigned XLEN-bit integer. 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: exec-sltiu

(defun exec-sltiu (rd rs1 imm stat feat)
  (declare (xargs :guard (and (ubyte5p rd)
                              (ubyte5p rs1)
                              (ubyte12p imm)
                              (statp stat)
                              (featp feat))))
  (declare (xargs :guard (stat-validp stat feat)))
  (let ((__function__ 'exec-sltiu))
    (declare (ignorable __function__))
    (b* ((rs1-operand (read-xreg-unsigned (ubyte5-fix rs1)
                                          stat feat))
         (imm-operand (loghead (feat->xlen feat)
                               (logext 12 (ubyte12-fix imm))))
         (result (if (< rs1-operand imm-operand) 1 0))
         (stat (write-xreg (ubyte5-fix rd)
                           result stat feat))
         (stat (inc4-pc stat feat)))
      stat)))

Theorem: statp-of-exec-sltiu

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

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

(defthm exec-sltiu-of-ubyte5-fix-rd
  (equal (exec-sltiu (ubyte5-fix rd)
                     rs1 imm stat feat)
         (exec-sltiu rd rs1 imm stat feat)))

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

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

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

(defthm exec-sltiu-of-ubyte5-fix-rs1
  (equal (exec-sltiu rd (ubyte5-fix rs1)
                     imm stat feat)
         (exec-sltiu rd rs1 imm stat feat)))

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

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

Theorem: exec-sltiu-of-ubyte12-fix-imm

(defthm exec-sltiu-of-ubyte12-fix-imm
  (equal (exec-sltiu rd rs1 (ubyte12-fix imm)
                     stat feat)
         (exec-sltiu rd rs1 imm stat feat)))

Theorem: exec-sltiu-ubyte12-equiv-congruence-on-imm

(defthm exec-sltiu-ubyte12-equiv-congruence-on-imm
  (implies (acl2::ubyte12-equiv imm imm-equiv)
           (equal (exec-sltiu rd rs1 imm stat feat)
                  (exec-sltiu rd rs1 imm-equiv stat feat)))
  :rule-classes :congruence)

Theorem: exec-sltiu-of-stat-fix-stat

(defthm exec-sltiu-of-stat-fix-stat
  (equal (exec-sltiu rd rs1 imm (stat-fix stat)
                     feat)
         (exec-sltiu rd rs1 imm stat feat)))

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

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

Theorem: exec-sltiu-of-feat-fix-feat

(defthm exec-sltiu-of-feat-fix-feat
  (equal (exec-sltiu rd rs1 imm stat (feat-fix feat))
         (exec-sltiu rd rs1 imm stat feat)))

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

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