		Search-engine friendly clone of the ACL2 documentation.

Instructions

Instr-validp

Check if an instruction is valid with respect to given features.

Signature
(instr-validp instr feat) → yes/no
Arguments: instr — Guard (instrp instr).; feat — Guard (featp feat).
Returns: yes/no — Type (booleanp yes/no).

Currently our model of features only consists of one bit of information: whether we are in 32-bit mode or in 64-bit mode; more precisely, whether our base is RV32I (or RV32E) or RV64I (or RV64E). For now we implicitly assume that the M extension is present; we plan to add a choice about that in the features.

Definitions and Theorems

Function: instr-validp

(defun instr-validp (instr feat)
 (declare (xargs :guard (and (instrp instr) (featp feat))))
 (let ((__function__ 'instr-validp))
  (declare (ignorable __function__))
  (b* (((feat feat) feat))
   (instr-case
        instr
        :op-imm t
        :op-imms32 (feat-bits-case feat.bits :|32|)
        :op-imms64 (feat-bits-case feat.bits :|64|)
        :op-imm-32 (feat-bits-case feat.bits :|64|)
        :op-imms-32 (feat-bits-case feat.bits :|64|)
        :lui t
        :auipc t
        :op t
        :op-32 (feat-bits-case feat.bits :|64|)
        :jal t
        :jalr t
        :branch t
        :load (load-funct-case instr.funct
                               :lb t
                               :lbu t
                               :lh t
                               :lhu t
                               :lw t
                               :lwu (feat-bits-case feat.bits :|64|)
                               :ld (feat-bits-case feat.bits :|64|))
        :store
        (store-funct-case instr.funct
                          :sb t
                          :sh t
                          :sw t
                          :sd (feat-bits-case feat.bits :|64|))))))

Theorem: booleanp-of-instr-validp

(defthm booleanp-of-instr-validp
  (b* ((yes/no (instr-validp instr feat)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: instr-validp-of-instr-fix-instr

(defthm instr-validp-of-instr-fix-instr
  (equal (instr-validp (instr-fix instr) feat)
         (instr-validp instr feat)))

Theorem: instr-validp-instr-equiv-congruence-on-instr

(defthm instr-validp-instr-equiv-congruence-on-instr
  (implies (instr-equiv instr instr-equiv)
           (equal (instr-validp instr feat)
                  (instr-validp instr-equiv feat)))
  :rule-classes :congruence)

Theorem: instr-validp-of-feat-fix-feat

(defthm instr-validp-of-feat-fix-feat
  (equal (instr-validp instr (feat-fix feat))
         (instr-validp instr feat)))

Theorem: instr-validp-feat-equiv-congruence-on-feat

(defthm instr-validp-feat-equiv-congruence-on-feat
  (implies (feat-equiv feat feat-equiv)
           (equal (instr-validp instr feat)
                  (instr-validp instr feat-equiv)))
  :rule-classes :congruence)