• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
        • Svex-stvs
        • Svex-decomposition-methodology
        • Sv-versus-esim
        • Svex-decomp
        • Svex-compose-dfs
        • Svex-compilation
        • Moddb
        • Svmods
        • Svstmt
        • Sv-tutorial
        • Expressions
          • Rewriting
          • Svex
          • Bit-blasting
          • Functions
          • 4vmask
            • Svex-argmasks
              • Svmask-for-bitand
              • Svmask-for-signx
              • Svmask-for-bitxor
              • Svmask-for-concat
              • Svmask-for-bit?!
              • Svmask-for-bit?
              • Svmask-for-?!
              • Svmask-for-?
              • Svmask-for-?*
              • Svmask-for-==??
              • Svmask-for-rsh
              • Svmask-for-bitsel
              • Svmask-for-+
              • Svmask-for-override
              • Svmask-for-uand
              • Svmask-for-zerox
              • Svmask-for-safer-==?
              • Svmask-for-bitor
              • Svmask-for-partinst
              • 4vmasklist-len-fix
              • Svmask-for-==?
              • Svmask-for-xdet
              • Svmask-for-unfloat
              • 4vmask-all-or-none
              • Svmask-for-partsel
              • Svmask-for-offp
              • Svmask-for-bitnot
              • Svmask-for-===*
              • Svmask-for-===
              • Svmask-for-res
              • Svmask-for-onp
              • Svmask-for-blkrev
              • Svmask-for-resor
              • Svmask-for-resand
              • Svmask-for-pow
              • Svmask-for-onehot0
              • Svmask-for-onehot
              • Svmask-for-lsh
              • Svmask-for-id
              • Svmask-for-countones
              • Svmask-for-clog2
              • Svmask-for-/
              • Svmask-for-==
              • Svmask-for-<
              • Svmask-for-*
              • Svmask-for-%
              • Svmask-for-uxor
              • Svmask-for-uor
              • Svmask-for-u-
              • Svmask-for-b-
              • Unrev-block-index
              • Svmask-for-unknown-function
              • Sparseint-unrev-blocks
            • 4vmask-p
            • 4vmask-subsumes
            • 4veclist-mask
            • 4vec-mask-to-zero
            • 4vec-mask
            • 4vmasklist-subsumes
            • 4vmask-union
            • 4vec-mask?
            • 4vmask-equiv
            • 4vmask-fix
            • 4vmask-alist
            • 4veclist-mask?
            • 4vmasklist
            • 4vmask-empty
          • Why-infinite-width
          • Svex-vars
          • Evaluation
          • Values
        • Symbolic-test-vector
        • Vl-to-svex
      • Fgl
      • Vwsim
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • 4vmask

Svex-argmasks

Statically compute the care masks for a function's arguments, starting from the care mask for the result of the function application.

Signature
(svex-argmasks mask fn args) → argmasks
Arguments
mask — Outer care mask, i.e., the care mask for the whole expression fn(args).
    Guard (4vmask-p mask).
fn — The function being applied.
    Guard (fnsym-p fn).
args — The arguments that fn is being applied to, whose care masks we want to determine.
    Guard (svexlist-p args).
Returns
argmasks — Care masks to use for the arguments.
    Type (and (4vmasklist-p argmasks) (equal (len argmasks) (len args))).

This function understands the SVEX functions and which bits of their arguments are sure to influence which bits of their outputs. For example, if we are given a function like:

(bitsel 4 <bigexpr>)

and if the initial, outer 4vmask for the whole expression is -1, i.e., we care about all of the bits of the result, then we will produce two new masks, one for each of the function's arguments:

  • For 4, we will just care about all the bits, i.e., our mask will be -1. This expression is already a constant anyway so there isn't much hope of simplifying it further and it poses no problems in computations such as reaching a compositional fixpoint.
  • For <bigexpr>, since we are selecting bit 4, we obviously only care about the fourth bit. Accordingly, the resulting care mask will be #b1000. Knowing that we only care about the fourth bit of <bigexpr> may allow us to make important simplifications to it, and may also allow us to generate better (more restrictive) care masks for its subexpressions.

In this way, care mask information can flow downward, starting from the outside of the expression and into the arguments.

Definitions and Theorems

Function: svex-argmasks

(defun svex-argmasks (mask fn args)
  (declare (xargs :guard (and (4vmask-p mask)
                              (fnsym-p fn)
                              (svexlist-p args))))
  (let ((__function__ 'svex-argmasks))
    (declare (ignorable __function__))
    (if (4vmask-empty mask)
        (replicate (len args) 0)
      (4vmasklist-len-fix
           (len args)
           (svex-argmasks-cases (mbe :logic (fnsym-fix fn)
                                     :exec fn))))))

Theorem: return-type-of-svex-argmasks

(defthm return-type-of-svex-argmasks
  (b* ((argmasks (svex-argmasks mask fn args)))
    (and (4vmasklist-p argmasks)
         (equal (len argmasks) (len args))))
  :rule-classes :rewrite)

Theorem: svex-argmasks-correct

(defthm svex-argmasks-correct
 (implies
    (and (equal (4veclist-mask (svex-argmasks mask fn args)
                               (svexlist-eval args env))
                (4veclist-mask (svex-argmasks mask fn args)
                               args1))
         (syntaxp (not (equal args1
                              (cons 'svexlist-eval
                                    (cons args (cons env 'nil)))))))
    (equal (4vec-mask mask (svex-apply fn args1))
           (4vec-mask mask
                      (svex-apply fn (svexlist-eval args env))))))

Theorem: svex-argmasks-correct2

(defthm svex-argmasks-correct2
 (implies
    (and (equal (4veclist-mask (svex-argmasks mask fn args)
                               args1)
                (4veclist-mask (svex-argmasks mask fn args)
                               (svexlist-eval args env)))
         (syntaxp (not (equal args1
                              (cons 'svexlist-eval
                                    (cons args (cons env 'nil)))))))
    (equal (4vec-mask mask (svex-apply fn args1))
           (4vec-mask mask
                      (svex-apply fn (svexlist-eval args env))))))

Theorem: svex-argmasks-of-4vmask-fix-mask

(defthm svex-argmasks-of-4vmask-fix-mask
  (equal (svex-argmasks (4vmask-fix mask)
                        fn args)
         (svex-argmasks mask fn args)))

Theorem: svex-argmasks-4vmask-equiv-congruence-on-mask

(defthm svex-argmasks-4vmask-equiv-congruence-on-mask
  (implies (4vmask-equiv mask mask-equiv)
           (equal (svex-argmasks mask fn args)
                  (svex-argmasks mask-equiv fn args)))
  :rule-classes :congruence)

Theorem: svex-argmasks-of-fnsym-fix-fn

(defthm svex-argmasks-of-fnsym-fix-fn
  (equal (svex-argmasks mask (fnsym-fix fn) args)
         (svex-argmasks mask fn args)))

Theorem: svex-argmasks-fnsym-equiv-congruence-on-fn

(defthm svex-argmasks-fnsym-equiv-congruence-on-fn
  (implies (fnsym-equiv fn fn-equiv)
           (equal (svex-argmasks mask fn args)
                  (svex-argmasks mask fn-equiv args)))
  :rule-classes :congruence)

Theorem: svex-argmasks-of-svexlist-fix-args

(defthm svex-argmasks-of-svexlist-fix-args
  (equal (svex-argmasks mask fn (svexlist-fix args))
         (svex-argmasks mask fn args)))

Theorem: svex-argmasks-svexlist-equiv-congruence-on-args

(defthm svex-argmasks-svexlist-equiv-congruence-on-args
  (implies (svexlist-equiv args args-equiv)
           (equal (svex-argmasks mask fn args)
                  (svex-argmasks mask fn args-equiv)))
  :rule-classes :congruence)

Theorem: svex-argmasks-of-none

(defthm svex-argmasks-of-none
  (implies (4vmask-empty mask)
           (equal (svex-argmasks mask fn args)
                  (replicate (len args) 0))))

Theorem: 4veclist-mask-idempotent

(defthm 4veclist-mask-idempotent
  (equal (4veclist-mask masks (4veclist-mask masks x))
         (4veclist-mask masks x)))

Theorem: svex-argmasks-remove-mask

(defthm svex-argmasks-remove-mask
 (equal
  (4vec-mask mask
             (svex-apply fn
                         (4veclist-mask (svex-argmasks mask fn args)
                                        (svexlist-eval args env))))
  (4vec-mask mask
             (svex-apply fn (svexlist-eval args env)))))

Subtopics

Svmask-for-bitand
Implements svex-argmasks for BITAND.
Svmask-for-signx
Implements svex-argmasks for SIGNX.
Svmask-for-bitxor
Implements svex-argmasks for BITXOR.
Svmask-for-concat
Implements svex-argmasks for CONCAT.
Svmask-for-bit?!
Implements svex-argmasks for BIT?!.
Svmask-for-bit?
Implements svex-argmasks for BIT?.
Svmask-for-?!
Implements svex-argmasks for ?!.
Svmask-for-?
Implements svex-argmasks for ?.
Svmask-for-?*
Implements svex-argmasks for ?*.
Svmask-for-==??
Implements svex-argmasks for ==??.
Svmask-for-rsh
Implements svex-argmasks for RSH.
Svmask-for-bitsel
Implements svex-argmasks for BITSEL.
Svmask-for-+
Implements svex-argmasks for +.
Svmask-for-override
Implements svex-argmasks for OVERRIDE.
Svmask-for-uand
Implements svex-argmasks for UAND.
Svmask-for-zerox
Implements svex-argmasks for ZEROX.
Svmask-for-safer-==?
Implements svex-argmasks for SAFER-==?.
Svmask-for-bitor
Implements svex-argmasks for BITOR.
Svmask-for-partinst
Implements svex-argmasks for PARTINST.
4vmasklist-len-fix
Svmask-for-==?
Implements svex-argmasks for ==?.
Svmask-for-xdet
Implements svex-argmasks for XDET.
Svmask-for-unfloat
Implements svex-argmasks for UNFLOAT.
4vmask-all-or-none
Care mask for an argument that matters fully, unless we don't care about any bits at all.
Svmask-for-partsel
Implements svex-argmasks for PARTSEL.
Svmask-for-offp
Implements svex-argmasks for OFFP.
Svmask-for-bitnot
Implements svex-argmasks for BITNOT.
Svmask-for-===*
Implements svex-argmasks for ===*.
Svmask-for-===
Implements svex-argmasks for ===.
Svmask-for-res
Implements svex-argmasks for RES.
Svmask-for-onp
Implements svex-argmasks for ONP.
Svmask-for-blkrev
Implements svex-argmasks for BLKREV.
Svmask-for-resor
Implements svex-argmasks for RESOR.
Svmask-for-resand
Implements svex-argmasks for RESAND.
Svmask-for-pow
Implements svex-argmasks for POW.
Svmask-for-onehot0
Implements svex-argmasks for ONEHOT0.
Svmask-for-onehot
Implements svex-argmasks for ONEHOT.
Svmask-for-lsh
Implements svex-argmasks for LSH.
Svmask-for-id
Implements svex-argmasks for ID.
Svmask-for-countones
Implements svex-argmasks for COUNTONES.
Svmask-for-clog2
Implements svex-argmasks for CLOG2.
Svmask-for-/
Implements svex-argmasks for /.
Svmask-for-==
Implements svex-argmasks for ==.
Svmask-for-<
Implements svex-argmasks for <.
Svmask-for-*
Implements svex-argmasks for *.
Svmask-for-%
Implements svex-argmasks for %.
Svmask-for-uxor
Implements svex-argmasks for UXOR.
Svmask-for-uor
Implements svex-argmasks for UOR.
Svmask-for-u-
Implements svex-argmasks for U-.
Svmask-for-b-
Implements svex-argmasks for B-.
Unrev-block-index
Svmask-for-unknown-function
Sparseint-unrev-blocks