		Search-engine friendly clone of the ACL2 documentation.

Semantics-equivalences

Exec-sll-alt-defs

Equivalent semantic definitions of SLL.

Definitions and Theorems

Theorem: exec-sll-alt-def

(defthm exec-sll-alt-def
  (equal (exec-sll rd rs1 rs2 stat feat)
         (b* ((rs1-operand (read-xreg-signed (ubyte5-fix rs1)
                                             stat feat))
              (rs2-operand (read-xreg-signed (ubyte5-fix rs2)
                                             stat feat))
              (shift-amount (cond ((feat-32p feat)
                                   (loghead 5 rs2-operand))
                                  ((feat-64p feat)
                                   (loghead 6 rs2-operand))
                                  (t (impossible))))
              (result (ash rs1-operand shift-amount))
              (stat (write-xreg (ubyte5-fix rd)
                                result stat feat))
              (stat (inc4-pc stat feat)))
           stat)))