• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • 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
      • Symbolic-test-vector
      • Vl-to-svex
        • Vl-to-sv
        • Vl-design->sv-design
          • Vl-simpconfig
          • Vl-hierarchy-sv-translation
          • Vl-expr-svex-translation
          • Vl-design->svex-modalist
          • Vl-svstmt
            • Vl-svstmt.lisp
              • Vl-casestmt-violation-conds
              • Vl-caselist-none/multiple
              • Vl-elaborated-expr-consteval
              • Vl-always->svex
              • Vl-caseexprs->svex-test
              • Vl-always->svex-checks
              • Vl-implicitvalueparam-final-type
              • Vl-assignstmt->svstmts
              • Vl-fundecl-to-svex
              • Vl-evatomlist-delay-substitution
              • Vl-consteval
              • Vl-alwayslist->svex
              • Vl-index-expr-svex/size/type
              • Vl-vardecllist->svstmts
              • Sv::svex-alist->assigns
              • Vl-case-conservative-test-expr
              • Vl-evatomlist->svex
              • Vl-case-xcond-wrapper
              • Sv::constraintlist-maybe-rewrite-fixpoint
              • Vl-always-apply-trigger-to-updates
              • Vl-initiallist-size-warnings
              • Vl-initial-size-warnings
              • Vl-finallist-size-warnings
              • Vl-always->svex-latch-warnings
              • Vl-final-size-warnings
              • Sv::svarlist-masked-x-subst
              • Sv::svar->lhs-by-mask
              • Svstmt-config
              • Sv::svex-alist-unset-nonblocking
              • Sv::svar->lhs-by-size
              • Combine-mask-alists
              • Sv::svarlist-delay-subst
              • Vttree-constraints-to-svstmts
              • Sv::4vmask-alist-unset-nonblocking
              • Sv::svarlist-remove-delays
              • Vl-caselist->caseexprs
              • Vl-evatomlist-has-edge
        • Vl-to-sv-main
        • Vl-simplify-sv
        • Vl-user-paramsettings->unparam-names
        • Vl-user-paramsettings->modnames
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Vl-svstmt.lisp

Sv::svarlist-masked-x-subst

Signature

(sv::svarlist-masked-x-subst sv::vars sv::masks) → subst

Arguments

sv::vars — Guard (sv::svarlist-p sv::vars).

sv::masks — Guard (sv::4vmask-alist-p sv::masks).

Returns

subst — Type (sv::svex-alist-p subst).

Definitions and Theorems

Function: svarlist-masked-x-subst

(defun sv::svarlist-masked-x-subst (sv::vars sv::masks)
 (declare (xargs :guard (and (sv::svarlist-p sv::vars)
                             (sv::4vmask-alist-p sv::masks))))
 (let ((__function__ 'sv::svarlist-masked-x-subst))
  (declare (ignorable __function__))
  (b* (((when (atom sv::vars)) nil)
       (sv::var (sv::svar-fix (car sv::vars)))
       (sv::mask (cdr (hons-get sv::var
                                (sv::4vmask-alist-fix sv::masks))))
       ((when (or (not sv::mask)
                  (bitops::sparseint-equal sv::mask 0)))
        (sv::svarlist-masked-x-subst (cdr sv::vars)
                                     sv::masks)))
   (cons
    (cons
     sv::var
     (sv::make-svex-call
      :fn 'sv::bit?
      :args
      (list
        (sv::svex-quote (sv::2vec (bitops::sparseint-val sv::mask)))
        (sv::svex-x)
        (sv::svex-var sv::var))))
    (sv::svarlist-masked-x-subst (cdr sv::vars)
                                 sv::masks)))))

Theorem: svex-alist-p-of-svarlist-masked-x-subst

(defthm sv::svex-alist-p-of-svarlist-masked-x-subst
  (b* ((subst (sv::svarlist-masked-x-subst sv::vars sv::masks)))
    (sv::svex-alist-p subst))
  :rule-classes :rewrite)

Theorem: vars-of-svarlist-masked-x-subst

(defthm sv::vars-of-svarlist-masked-x-subst
 (b* ((common-lisp::?subst
           (sv::svarlist-masked-x-subst sv::vars sv::masks)))
  (implies (not (member-equal sv::v (sv::svarlist-fix sv::vars)))
           (not (member-equal sv::v (sv::svex-alist-vars subst))))))

Theorem: svarlist-masked-x-subst-of-svarlist-fix-vars

(defthm sv::svarlist-masked-x-subst-of-svarlist-fix-vars
  (equal (sv::svarlist-masked-x-subst (sv::svarlist-fix sv::vars)
                                      sv::masks)
         (sv::svarlist-masked-x-subst sv::vars sv::masks)))

Theorem: svarlist-masked-x-subst-svarlist-equiv-congruence-on-vars

(defthm
      sv::svarlist-masked-x-subst-svarlist-equiv-congruence-on-vars
 (implies
     (sv::svarlist-equiv sv::vars sv::vars-equiv)
     (equal (sv::svarlist-masked-x-subst sv::vars sv::masks)
            (sv::svarlist-masked-x-subst sv::vars-equiv sv::masks)))
 :rule-classes :congruence)

Theorem: svarlist-masked-x-subst-of-4vmask-alist-fix-masks

(defthm sv::svarlist-masked-x-subst-of-4vmask-alist-fix-masks
 (equal
      (sv::svarlist-masked-x-subst sv::vars
                                   (sv::4vmask-alist-fix sv::masks))
      (sv::svarlist-masked-x-subst sv::vars sv::masks)))

Theorem: svarlist-masked-x-subst-4vmask-alist-equiv-congruence-on-masks

(defthm
 sv::svarlist-masked-x-subst-4vmask-alist-equiv-congruence-on-masks
 (implies
     (sv::4vmask-alist-equiv sv::masks sv::masks-equiv)
     (equal (sv::svarlist-masked-x-subst sv::vars sv::masks)
            (sv::svarlist-masked-x-subst sv::vars sv::masks-equiv)))
 :rule-classes :congruence)