		Search-engine friendly clone of the ACL2 documentation.

Semantics32

Exec32-sltiu

Semantics of the SLTIU instruction [ISA:2.4.1].

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

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

(defun exec32-sltiu (rd rs1 imm stat)
  (declare (xargs :guard (and (ubyte5p rd)
                              (ubyte5p rs1)
                              (ubyte12p imm)
                              (state32p stat))))
  (let ((__function__ 'exec32-sltiu))
    (declare (ignorable __function__))
    (b* ((rs1-operand (read32-xreg-unsigned rs1 stat))
         (imm-operand (loghead 32 (logext 12 (ubyte12-fix imm))))
         (result (if (< rs1-operand imm-operand) 1 0))
         (stat (write32-xreg rd result stat))
         (stat (inc32-pc stat)))
      stat)))

Theorem: state32p-of-exec32-sltiu

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(defthm exec32-sltiu-of-state32-fix-stat
  (equal (exec32-sltiu rd rs1 imm (state32-fix stat))
         (exec32-sltiu rd rs1 imm stat)))

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

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