• 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-evatomlist-delay-substitution

Signature

(vl-evatomlist-delay-substitution x edge-dependent-delayp ss scopes) 
  → 
(mv warnings subst)

Arguments

x — Guard (vl-evatomlist-p x).

ss — Guard (vl-scopestack-p ss).

scopes — Guard (vl-elabscopes-p scopes).

Returns

warnings — Type (vl-warninglist-p warnings).

subst — Type (and (sv::svex-alist-p subst) (sv::svarlist-addr-p (sv::svex-alist-vars subst)) (sv::svarlist-addr-p (sv::svex-alist-keys subst))) .

Definitions and Theorems

Function: vl-evatomlist-delay-substitution

(defun vl-evatomlist-delay-substitution
       (x edge-dependent-delayp ss scopes)
 (declare (xargs :guard (and (vl-evatomlist-p x)
                             (vl-scopestack-p ss)
                             (vl-elabscopes-p scopes))))
 (let ((__function__ 'vl-evatomlist-delay-substitution))
  (declare (ignorable __function__))
  (b*
   (((when (atom x)) (mv nil nil))
    ((vl-evatom x1) (vl-evatom-fix (car x)))
    (warnings nil)
    ((unless
         (vl-expr-case
              x1.expr
              :vl-index (and (vl-partselect-case x1.expr.part :none)
                             (atom x1.expr.indices))
              :otherwise nil))
     (vl-evatomlist-delay-substitution
          (cdr x)
          edge-dependent-delayp ss scopes))
    ((mv err opinfo)
     (vl-index-expr-typetrace x1.expr ss scopes))
    ((when err)
     (vl-evatomlist-delay-substitution
          (cdr x)
          edge-dependent-delayp ss scopes))
    ((vl-operandinfo opinfo))
    ((unless (and (vl-hidtrace-resolved-p opinfo.hidtrace)
                  (eql (vl-seltrace-unres-count opinfo.seltrace)
                       0)))
     (vl-evatomlist-delay-substitution
          (cdr x)
          edge-dependent-delayp ss scopes))
    (warnings
     (if
      (or opinfo.seltrace opinfo.part)
      (warn
       :type :vl-always-trigger-dubiously-translated
       :msg
       "Event trigger expression ~a0 has selects on it; we ~
                        probably don't deal well with this yet."
       :args (list x1))
      warnings))
    ((mv err var)
     (vl-operandinfo-base-svar opinfo ss))
    ((when err)
     (vl-evatomlist-delay-substitution
          (cdr x)
          edge-dependent-delayp ss scopes))
    (expr (sv::make-svex-var :name var))
    (delay-expr
     (if edge-dependent-delayp
      (case
       x1.type (:vl-noedge expr)
       (:vl-posedge
        (sv::make-svex-call
          :fn 'sv::?
          :args (list (sv::make-svex-call
                           :fn 'sv::bitsel
                           :args (list (sv::svex-quote (sv::2vec 0))
                                       expr))
                      expr (sv::svex-add-delay expr 1))))
       (:vl-negedge
        (sv::make-svex-call
          :fn 'sv::?
          :args (list (sv::make-svex-call
                           :fn 'sv::bitsel
                           :args (list (sv::svex-quote (sv::2vec 0))
                                       expr))
                      (sv::svex-add-delay expr 1)
                      expr)))
       (:vl-edge expr))
      expr))
    ((wmv warnings rest)
     (vl-evatomlist-delay-substitution
          (cdr x)
          edge-dependent-delayp ss scopes)))
   (mv warnings
       (cons (cons var delay-expr) rest)))))

Theorem: vl-warninglist-p-of-vl-evatomlist-delay-substitution.warnings

(defthm
      vl-warninglist-p-of-vl-evatomlist-delay-substitution.warnings
  (b* (((mv ?warnings common-lisp::?subst)
        (vl-evatomlist-delay-substitution
             x edge-dependent-delayp ss scopes)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-evatomlist-delay-substitution.subst

(defthm return-type-of-vl-evatomlist-delay-substitution.subst
  (b* (((mv ?warnings common-lisp::?subst)
        (vl-evatomlist-delay-substitution
             x edge-dependent-delayp ss scopes)))
    (and (sv::svex-alist-p subst)
         (sv::svarlist-addr-p (sv::svex-alist-vars subst))
         (sv::svarlist-addr-p (sv::svex-alist-keys subst))))
  :rule-classes :rewrite)

Theorem: vl-evatomlist-delay-substitution-of-vl-evatomlist-fix-x

(defthm vl-evatomlist-delay-substitution-of-vl-evatomlist-fix-x
 (equal
  (vl-evatomlist-delay-substitution (vl-evatomlist-fix x)
                                    edge-dependent-delayp ss scopes)
  (vl-evatomlist-delay-substitution
       x edge-dependent-delayp ss scopes)))

Theorem: vl-evatomlist-delay-substitution-vl-evatomlist-equiv-congruence-on-x

(defthm
 vl-evatomlist-delay-substitution-vl-evatomlist-equiv-congruence-on-x
 (implies (vl-evatomlist-equiv x x-equiv)
          (equal (vl-evatomlist-delay-substitution
                      x edge-dependent-delayp ss scopes)
                 (vl-evatomlist-delay-substitution
                      x-equiv
                      edge-dependent-delayp ss scopes)))
 :rule-classes :congruence)

Theorem: vl-evatomlist-delay-substitution-of-vl-scopestack-fix-ss

(defthm vl-evatomlist-delay-substitution-of-vl-scopestack-fix-ss
  (equal (vl-evatomlist-delay-substitution x edge-dependent-delayp
                                           (vl-scopestack-fix ss)
                                           scopes)
         (vl-evatomlist-delay-substitution
              x edge-dependent-delayp ss scopes)))

Theorem: vl-evatomlist-delay-substitution-vl-scopestack-equiv-congruence-on-ss

(defthm
 vl-evatomlist-delay-substitution-vl-scopestack-equiv-congruence-on-ss
 (implies (vl-scopestack-equiv ss ss-equiv)
          (equal (vl-evatomlist-delay-substitution
                      x edge-dependent-delayp ss scopes)
                 (vl-evatomlist-delay-substitution
                      x
                      edge-dependent-delayp ss-equiv scopes)))
 :rule-classes :congruence)

Theorem: vl-evatomlist-delay-substitution-of-vl-elabscopes-fix-scopes

(defthm vl-evatomlist-delay-substitution-of-vl-elabscopes-fix-scopes
 (equal
    (vl-evatomlist-delay-substitution x edge-dependent-delayp
                                      ss (vl-elabscopes-fix scopes))
    (vl-evatomlist-delay-substitution
         x edge-dependent-delayp ss scopes)))

Theorem: vl-evatomlist-delay-substitution-vl-elabscopes-equiv-congruence-on-scopes

(defthm
 vl-evatomlist-delay-substitution-vl-elabscopes-equiv-congruence-on-scopes
 (implies (vl-elabscopes-equiv scopes scopes-equiv)
          (equal (vl-evatomlist-delay-substitution
                      x edge-dependent-delayp ss scopes)
                 (vl-evatomlist-delay-substitution
                      x
                      edge-dependent-delayp ss scopes-equiv)))
 :rule-classes :congruence)