		Search-engine friendly clone of the ACL2 documentation.

Semantics64

Exec64-slti

Semantics of the SLTI instruction [ISA:2.4.1].

Signature
(exec64-slti 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 a signed 64-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: exec64-slti

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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