		Search-engine friendly clone of the ACL2 documentation.

Missing-parents

Exec-slti

Semantics of the SLTI instruction [ISA:2.4.1].

Signature
(exec-slti 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 a signed XLEN-bit integer from rs1. We sign-extend the 12-bit immediate, obtaining a signed integer. We compare the two signed 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-slti

(defun exec-slti (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-slti))
    (declare (ignorable __function__))
    (b* ((rs1-operand (read-xreg-signed (ubyte5-fix rs1)
                                        stat feat))
         (imm-operand (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-slti

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem: exec-slti-of-stat-fix-stat

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

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

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

Theorem: exec-slti-of-feat-fix-feat

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

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

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