		Search-engine friendly clone of the ACL2 documentation.

Semantics32

Exec32-slti

Semantics of the SLTI instruction [ISA:2.4.1].

Signature
(exec32-slti 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 a signed 32-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: exec32-slti

(defun exec32-slti (rd rs1 imm stat)
  (declare (xargs :guard (and (ubyte5p rd)
                              (ubyte5p rs1)
                              (ubyte12p imm)
                              (state32p stat))))
  (let ((__function__ 'exec32-slti))
    (declare (ignorable __function__))
    (b* ((rs1-operand (read32-xreg-signed rs1 stat))
         (imm-operand (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-slti

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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