• Top
  • Documentation
    • Xdoc
      • Missing-parents
        • Exec-bgeu
        • Exec-bltu
        • Exec-blt
        • Exec-bge
        • Exec-jalr
        • Exec-bne
        • Exec-beq
        • Exec-sra
        • Exec-op-imms-32
        • Exec-srl
        • Exec-sll
        • Exec-op-imms64
        • Exec-op-imms32
        • Exec-op-imm-32
        • Exec-op-32
        • Exec-op
        • Exec-branch
        • Exec-srlw
        • Exec-srliw
        • Exec-sraw
        • Exec-sraiw
        • Exec-sltiu
        • Exec-remuw
        • Exec-op-imm
        • Exec-jal
        • Exec-store
        • Exec-srli64
        • Exec-srli32
        • Exec-srai64
        • Exec-srai32
        • Exec-sllw
        • Exec-remw
        • Exec-load
        • Exec-divuw
        • Exec-addiw
        • Exec-xori
        • Exec-slti
        • Exec-slliw
        • Exec-remu
        • Exec-rem
        • Exec-divw
        • Exec-sw
        • Exec-slli64
        • Exec-slli32
        • Exec-ori
        • Exec-mulhsu
        • Exec-divu
        • Exec-andi
        • Exec-addi
        • Exec-sltu
        • Exec-slt
        • Exec-mulhu
        • Exec-lwu
        • Exec-div
        • Exec-auipc
        • Exec-addw
        • Exec-xor
        • Exec-mulw
        • Exec-mulh
        • Exec-and
        • Exec-subw
        • Exec-sub
        • Exec-sh
        • Exec-sd
        • Exec-sb
        • Exec-or
        • Exec-lhu
        • Exec-lh
        • Exec-ld
        • Exec-lbu
        • Exec-lb
        • Exec-mul
        • Exec-add
        • Exec-lw
        • Exec-lui
        • Eff-addr
        • Exec-instr
        • Missing-parents-test
      • Undocumented
      • Save
      • Defsection
      • Markup
      • Preprocessor
      • Terminal
      • Emacs-links
      • Defxdoc
      • Katex-integration
      • Constructors
      • Entities
      • Defxdoc+
      • Save-rendered
      • Add-resource-directory
      • Testing
      • Order-subtopics
      • Save-rendered-event
      • Archive-matching-topics
      • Archive-xdoc
      • Xdoc-extend
      • Set-default-parents
      • Defpointer
      • Defxdoc-raw
      • Xdoc-tests
      • Xdoc-prepend
      • Defsection-progn
      • Gen-xdoc-for-file
    • ACL2-doc
    • Recursion-and-induction
    • Loop$-primer
    • Operational-semantics
    • Pointers
    • Doc
    • Documentation-copyright
    • Course-materials
    • Publications
    • Args
    • ACL2-doc-summary
    • Finding-documentation
    • Broken-link
    • Doc-terminal-test-2
    • Doc-terminal-test-1
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Missing-parents

Exec-auipc

Semantics of the AUIPC instruction [ISA:4.2.1].

Signature

(exec-auipc rd imm pc stat feat) → new-stat

Arguments

rd — Guard (ubyte5p rd).

imm — Guard (ubyte20p imm).

stat — Guard (statp stat).

feat — Guard (featp feat).

Returns

new-stat — Type (statp 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. In 64-bit mode, we extend the unsigned 32-bit integer to 64 bits, obtaining an unsigned 64-bit integer. 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: exec-auipc

(defun exec-auipc (rd imm pc stat feat)
  (declare (xargs :guard (and (ubyte5p rd)
                              (ubyte20p imm)
                              (statp stat)
                              (featp feat))))
  (declare (xargs :guard (and (stat-validp stat feat)
                              (cond ((feat-32p feat) (ubyte32p pc))
                                    ((feat-64p feat) (ubyte64p pc))
                                    (t (impossible))))))
  (let ((__function__ 'exec-auipc))
    (declare (ignorable __function__))
    (b* ((offset (ash (ubyte20-fix imm) 12))
         (offset (if (feat-64p feat)
                     (loghead 64 (logext 32 offset))
                   offset))
         (result (+ pc offset))
         (stat (write-xreg (ubyte5-fix rd)
                           result stat feat))
         (stat (inc4-pc stat feat)))
      stat)))

Theorem: statp-of-exec-auipc

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

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

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

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

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

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

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

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

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

Theorem: exec-auipc-of-stat-fix-stat

(defthm exec-auipc-of-stat-fix-stat
  (equal (exec-auipc rd imm pc (stat-fix stat)
                     feat)
         (exec-auipc rd imm pc stat feat)))

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

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

Theorem: exec-auipc-of-feat-fix-feat

(defthm exec-auipc-of-feat-fix-feat
  (equal (exec-auipc rd imm pc stat (feat-fix feat))
         (exec-auipc rd imm pc stat feat)))

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

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