		Search-engine friendly clone of the ACL2 documentation.

Semantics32

Exec32-auipc

Semantics of the AUIPC instruction [ISA:4.2.1].

Signature
(exec32-auipc rd imm pc stat) → new-stat
Arguments: rd — Guard (ubyte5p rd).; imm — Guard (ubyte20p imm).; pc — Guard (ubyte32p pc).; stat — Guard (state32p stat).
Returns: new-stat — Type (state32p new-stat).

We use the 20 bits of the immediate as the high bits of an unsigned 32-bit integer, whose low bits are 0. We add the integer to the address of the instruction, which is passed as the pc input to this function. We write the result to rd. We increment the program counter.

Definitions and Theorems

Function: exec32-auipc

(defun exec32-auipc (rd imm pc stat)
  (declare (xargs :guard (and (ubyte5p rd)
                              (ubyte20p imm)
                              (ubyte32p pc)
                              (state32p stat))))
  (let ((__function__ 'exec32-auipc))
    (declare (ignorable __function__))
    (b* ((offset (ash (ubyte20-fix imm) 12))
         (result (+ (ubyte32-fix pc) offset))
         (stat (write32-xreg rd result stat))
         (stat (inc32-pc stat)))
      stat)))

Theorem: state32p-of-exec32-auipc

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

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

(defthm exec32-auipc-of-ubyte5-fix-rd
  (equal (exec32-auipc (ubyte5-fix rd)
                       imm pc stat)
         (exec32-auipc rd imm pc stat)))

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

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

Theorem: exec32-auipc-of-ubyte20-fix-imm

(defthm exec32-auipc-of-ubyte20-fix-imm
  (equal (exec32-auipc rd (ubyte20-fix imm)
                       pc stat)
         (exec32-auipc rd imm pc stat)))

Theorem: exec32-auipc-ubyte20-equiv-congruence-on-imm

(defthm exec32-auipc-ubyte20-equiv-congruence-on-imm
  (implies (acl2::ubyte20-equiv imm imm-equiv)
           (equal (exec32-auipc rd imm pc stat)
                  (exec32-auipc rd imm-equiv pc stat)))
  :rule-classes :congruence)

Theorem: exec32-auipc-of-ubyte32-fix-pc

(defthm exec32-auipc-of-ubyte32-fix-pc
  (equal (exec32-auipc rd imm (ubyte32-fix pc)
                       stat)
         (exec32-auipc rd imm pc stat)))

Theorem: exec32-auipc-ubyte32-equiv-congruence-on-pc

(defthm exec32-auipc-ubyte32-equiv-congruence-on-pc
  (implies (acl2::ubyte32-equiv pc pc-equiv)
           (equal (exec32-auipc rd imm pc stat)
                  (exec32-auipc rd imm pc-equiv stat)))
  :rule-classes :congruence)

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

(defthm exec32-auipc-of-state32-fix-stat
  (equal (exec32-auipc rd imm pc (state32-fix stat))
         (exec32-auipc rd imm pc stat)))

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

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