		Search-engine friendly clone of the ACL2 documentation.

Semantics64

Exec64-sltiu

Semantics of the SLTIU instruction [ISA:2.4.1].

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

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

(defun exec64-sltiu (rd rs1 imm stat)
  (declare (xargs :guard (and (ubyte5p rd)
                              (ubyte5p rs1)
                              (ubyte12p imm)
                              (state64p stat))))
  (let ((__function__ 'exec64-sltiu))
    (declare (ignorable __function__))
    (b* ((rs1-operand (read64-xreg-unsigned rs1 stat))
         (imm-operand (loghead 64 (logext 12 (ubyte12-fix imm))))
         (result (if (< rs1-operand imm-operand) 1 0))
         (stat (write64-xreg rd result stat))
         (stat (inc64-pc stat)))
      stat)))

Theorem: state64p-of-exec64-sltiu

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(defthm exec64-sltiu-of-state64-fix-stat
  (equal (exec64-sltiu rd rs1 imm (state64-fix stat))
         (exec64-sltiu rd rs1 imm stat)))

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

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