• 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

Vl-always-apply-trigger-to-updates

Signature

(vl-always-apply-trigger-to-updates trigger x) → new-x

Arguments

trigger — Guard (sv::svex-p trigger).

x — Guard (sv::svex-alist-p x).

Returns

new-x — Type (sv::svex-alist-p new-x).

Definitions and Theorems

Function: vl-always-apply-trigger-to-updates

(defun vl-always-apply-trigger-to-updates (trigger x)
 (declare (xargs :guard (and (sv::svex-p trigger)
                             (sv::svex-alist-p x))))
 (let ((__function__ 'vl-always-apply-trigger-to-updates))
   (declare (ignorable __function__))
   (b*
    (((when (atom x)) nil)
     ((unless (mbt (and (consp (car x))
                        (sv::svar-p (caar x)))))
      (vl-always-apply-trigger-to-updates trigger (cdr x)))
     ((cons var upd) (car x))
     (upd (sv::svex-fix upd))
     (prev-var (sv::make-svex-var :name (sv::svar-add-delay var 1)))
     (trigger-upd
          (sv::make-svex-call :fn 'sv::?
                              :args (list trigger upd prev-var))))
    (cons (cons var trigger-upd)
          (vl-always-apply-trigger-to-updates trigger (cdr x))))))

Theorem: svex-alist-p-of-vl-always-apply-trigger-to-updates

(defthm svex-alist-p-of-vl-always-apply-trigger-to-updates
  (b* ((new-x (vl-always-apply-trigger-to-updates trigger x)))
    (sv::svex-alist-p new-x))
  :rule-classes :rewrite)

Theorem: keys-of-vl-always-apply-trigger-to-updates

(defthm keys-of-vl-always-apply-trigger-to-updates
  (b* ((?new-x (vl-always-apply-trigger-to-updates trigger x)))
    (iff (sv::svex-lookup v new-x)
         (sv::svex-lookup v x))))

Theorem: vars-of-vl-always-apply-trigger-to-updates

(defthm vars-of-vl-always-apply-trigger-to-updates
 (b* ((?new-x (vl-always-apply-trigger-to-updates trigger x)))
  (implies
   (and (not (member v (sv::svex-alist-vars x)))
        (not (member v (sv::svex-vars trigger)))
        (not (member v
                     (sv::svarlist-add-delay (sv::svex-alist-keys x)
                                             1))))
   (not (member v (sv::svex-alist-vars new-x))))))

Theorem: vl-always-apply-trigger-to-updates-of-svex-alist-fix-x

(defthm vl-always-apply-trigger-to-updates-of-svex-alist-fix-x
  (equal (vl-always-apply-trigger-to-updates
              trigger (sv::svex-alist-fix x))
         (vl-always-apply-trigger-to-updates trigger x)))

Theorem: vl-always-apply-trigger-to-updates-svex-alist-equiv-congruence-on-x

(defthm
 vl-always-apply-trigger-to-updates-svex-alist-equiv-congruence-on-x
 (implies
      (sv::svex-alist-equiv x x-equiv)
      (equal (vl-always-apply-trigger-to-updates trigger x)
             (vl-always-apply-trigger-to-updates trigger x-equiv)))
 :rule-classes :congruence)

Theorem: vl-always-apply-trigger-to-updates-of-svex-fix-trigger

(defthm vl-always-apply-trigger-to-updates-of-svex-fix-trigger
  (equal (vl-always-apply-trigger-to-updates (sv::svex-fix trigger)
                                             x)
         (vl-always-apply-trigger-to-updates trigger x)))

Theorem: vl-always-apply-trigger-to-updates-svex-equiv-congruence-on-trigger

(defthm
 vl-always-apply-trigger-to-updates-svex-equiv-congruence-on-trigger
 (implies
      (sv::svex-equiv trigger trigger-equiv)
      (equal (vl-always-apply-trigger-to-updates trigger x)
             (vl-always-apply-trigger-to-updates trigger-equiv x)))
 :rule-classes :congruence)