• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Pfcs
      • Wp-gen
      • Dimacs-reader
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • Taspi
      • Riscv
        • Specification
          • Semantics
            • Exec-bltu
            • Exec-blt
            • Exec-bgeu
            • Exec-bge
            • Exec-jalr
            • Exec-bne
            • Exec-beq
            • Exec-sra
            • Exec-op
            • Exec-srl
            • Exec-op-imms-32
            • Exec-op-32
            • Exec-srlw
            • Exec-sraw
            • Exec-sll
            • Exec-remuw
            • Exec-op-imms64
            • Exec-op-imms32
            • Exec-op-imm-32
            • Exec-branch
            • Exec-addi
            • Exec-srliw
              • Exec-sraiw
              • Exec-sltiu
              • Exec-remw
              • Exec-op-imm
              • Exec-load
              • Exec-jal
              • Exec-divuw
              • Exec-sub
              • Exec-store
              • Exec-srli64
              • Exec-srli32
              • Exec-srai64
              • Exec-srai32
              • Exec-sllw
              • Exec-remu
              • Exec-divw
              • Exec-addiw
              • Exec-xori
              • Exec-slti
              • Exec-slliw
              • Exec-rem
              • Exec-ori
              • Exec-mulhsu
              • Exec-divu
              • Exec-andi
              • Exec-add
              • Exec-sw
              • Exec-sltu
              • Exec-slt
              • Exec-slli64
              • Exec-slli32
              • Exec-mulhu
              • Exec-div
              • Exec-auipc
              • Exec-addw
              • Exec-mulw
              • Exec-mulh
              • Exec-lwu
              • Exec-xor
              • Exec-subw
              • Exec-or
              • Exec-lhu
              • Exec-lbu
              • Exec-and
              • Exec-sd
              • Exec-mul
              • Exec-lh
              • Exec-ld
              • Exec-lb
              • Exec-sh
              • Exec-sb
              • Exec-lw
              • Exec-lui
              • Eff-addr
              • Exec-instr
            • Features
            • States
            • Instructions
            • Encoding
            • Reads-over-writes
            • Execution
            • Decoding
          • Executable
          • Specialized
        • Bitcoin
        • Des
        • Ethereum
        • X86isa
        • Sha-2
        • Yul
        • Zcash
        • Proof-checker-itp13
        • Regex
        • ACL2-programming-language
        • Json
        • Jfkr
        • Equational
        • Cryptography
        • Poseidon
        • Where-do-i-place-my-book
        • Axe
        • Aleo
        • Bigmems
        • Builtins
        • Execloader
        • Solidity
        • Paco
        • Concurrent-programs
        • Bls12-377-curves
      • Debugging
      • Std
      • Community
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Semantics

    Exec-srliw

    Semantics of the SRLIW instruction [ISA:4.2.1].

    Signature
    (exec-srliw rd rs1 imm stat feat) → new-stat
    Arguments
    rd — Guard (ubyte5p rd).
    rs1 — Guard (ubyte5p rs1).
    imm — Guard (ubyte5p imm).
    stat — Guard (statp stat).
    feat — Guard (featp feat).
    Returns
    new-stat — Type (statp new-stat).

    This is only valid in 64-bit mode.

    We read an unsigned 32-bit integer from rs1. The immediate is the shift amount, from 0 to 31. We shift the integer right by the shift amount; this is a logical shift, because the integer is unsigned. We write the result to rd, as a signed 32-bit integer. We increment the program counter.

    Definitions and Theorems

    Function: exec-srliw

    (defun exec-srliw (rd rs1 imm stat feat)
      (declare (xargs :guard (and (ubyte5p rd)
                                  (ubyte5p rs1)
                                  (ubyte5p imm)
                                  (statp stat)
                                  (featp feat))))
      (declare (xargs :guard (and (feat-64p feat)
                                  (stat-validp stat feat)
                                  (< (lnfix rd) (feat->xnum feat))
                                  (< (lnfix rs1) (feat->xnum feat)))))
      (let ((__function__ 'exec-srliw))
        (declare (ignorable __function__))
        (b* ((rs1-operand (read-xreg-unsigned32 (ubyte5-fix rs1)
                                                stat feat))
             (shift-amount (ubyte5-fix imm))
             (result (ash rs1-operand (- shift-amount)))
             (stat (write-xreg-32 (ubyte5-fix rd)
                                  result stat feat))
             (stat (inc4-pc stat feat)))
          stat)))

    Theorem: statp-of-exec-srliw

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

    Theorem: stat-validp-of-exec-srliw

    (defthm stat-validp-of-exec-srliw
      (implies (and (stat-validp stat feat)
                    (< (lnfix rd) (feat->xnum feat)))
               (b* ((?new-stat (exec-srliw rd rs1 imm stat feat)))
                 (stat-validp new-stat feat))))

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

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

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

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

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

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

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

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

    Theorem: exec-srliw-of-ubyte5-fix-imm

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

    Theorem: exec-srliw-ubyte5-equiv-congruence-on-imm

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

    Theorem: exec-srliw-of-stat-fix-stat

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

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

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

    Theorem: exec-srliw-of-feat-fix-feat

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

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

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