• 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-assignstmt->svstmts

Signature

(vl-assignstmt->svstmts lhs rhs blockingp ss scopes) 
  → 
(mv ok vttree res)

Arguments

lhs — Guard (vl-expr-p lhs).

rhs — Guard (vl-rhs-p rhs).

blockingp — Guard (booleanp blockingp).

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

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

Returns

vttree — Type (and (vttree-p vttree) (sv::svarlist-addr-p (sv::constraintlist-vars (vttree->constraints vttree)))) .

res — Type (sv::svstmtlist-p res).

Definitions and Theorems

Function: vl-assignstmt->svstmts

(defun vl-assignstmt->svstmts (lhs rhs blockingp ss scopes)
 (declare (xargs :guard (and (vl-expr-p lhs)
                             (vl-rhs-p rhs)
                             (booleanp blockingp)
                             (vl-scopestack-p ss)
                             (vl-elabscopes-p scopes))))
 (let ((__function__ 'vl-assignstmt->svstmts))
  (declare (ignorable __function__))
  (b* ((vttree nil)
       ((unless (vl-rhs-case rhs :vl-rhsexpr))
        (mv nil
            (vfatal :type :vl-assignstmt-fail
                    :msg "Not yet supported: 'new' instances: ~a0"
                    :args (list (vl-rhs-fix rhs)))
            nil))
       (lhs (vl-expr-fix lhs))
       (rhs (vl-rhsexpr->guts rhs)))
   (vl-expr-case
    lhs :vl-index
    (b* (((mv err opinfo)
          (vl-index-expr-typetrace lhs ss scopes))
         ((when err)
          (mv nil
              (vfatal :type :vl-assignstmt-fail
                      :msg "Failed to get type of LHS ~a0: ~@1"
                      :args (list lhs err))
              nil))
         ((vl-operandinfo opinfo))
         ((vmv vttree type-err rhssvex)
          (vl-expr-to-svex-datatyped rhs lhs opinfo.type ss scopes
                                     :compattype :assign))
         ((wvmv vttree)
          (vl-type-error-basic-warn
               rhs nil type-err lhs opinfo.type ss))
         ((vmv ok vttree writes ?shift)
          (vl-procedural-assign->svstmts
               lhs rhssvex blockingp ss scopes))
         (svstmts
              (list (sv::make-svstmt-assign :writes writes
                                            :blockingp blockingp))))
      (mv ok vttree svstmts))
    :vl-concat
    (b* (((vmv vttree & lhssize)
          (vl-expr-to-svex-selfdet lhs nil ss scopes))
         ((vmv vttree rhssvex ?rhssize)
          (vl-expr-to-svex-selfdet rhs lhssize ss scopes))
         ((vmv ok vttree writes ?shift)
          (vl-procedural-assign->svstmts
               lhs rhssvex blockingp ss scopes))
         (svstmts
              (list (sv::make-svstmt-assign :writes writes
                                            :blockingp blockingp))))
      (mv ok vttree svstmts))
    :otherwise (mv nil
                   (vfatal :type :vl-lhs-malformed
                           :msg "Bad lvalue: ~a0"
                           :args (list lhs))
                   nil)))))

Theorem: return-type-of-vl-assignstmt->svstmts.vttree

(defthm return-type-of-vl-assignstmt->svstmts.vttree
 (b* (((mv ?ok ?vttree ?res)
       (vl-assignstmt->svstmts lhs rhs blockingp ss scopes)))
  (and
      (vttree-p vttree)
      (sv::svarlist-addr-p
           (sv::constraintlist-vars (vttree->constraints vttree)))))
 :rule-classes :rewrite)

Theorem: svstmtlist-p-of-vl-assignstmt->svstmts.res

(defthm svstmtlist-p-of-vl-assignstmt->svstmts.res
  (b* (((mv ?ok ?vttree ?res)
        (vl-assignstmt->svstmts lhs rhs blockingp ss scopes)))
    (sv::svstmtlist-p res))
  :rule-classes :rewrite)

Theorem: vars-of-vl-assignstmt->svstmts

(defthm vars-of-vl-assignstmt->svstmts
  (b* (((mv ?ok ?vttree ?res)
        (vl-assignstmt->svstmts lhs rhs blockingp ss scopes)))
    (sv::svarlist-addr-p (sv::svstmtlist-vars res))))

Theorem: vl-assignstmt->svstmts-of-vl-expr-fix-lhs

(defthm vl-assignstmt->svstmts-of-vl-expr-fix-lhs
  (equal (vl-assignstmt->svstmts (vl-expr-fix lhs)
                                 rhs blockingp ss scopes)
         (vl-assignstmt->svstmts lhs rhs blockingp ss scopes)))

Theorem: vl-assignstmt->svstmts-vl-expr-equiv-congruence-on-lhs

(defthm vl-assignstmt->svstmts-vl-expr-equiv-congruence-on-lhs
 (implies
   (vl-expr-equiv lhs lhs-equiv)
   (equal
        (vl-assignstmt->svstmts lhs rhs blockingp ss scopes)
        (vl-assignstmt->svstmts lhs-equiv rhs blockingp ss scopes)))
 :rule-classes :congruence)

Theorem: vl-assignstmt->svstmts-of-vl-rhs-fix-rhs

(defthm vl-assignstmt->svstmts-of-vl-rhs-fix-rhs
  (equal (vl-assignstmt->svstmts lhs (vl-rhs-fix rhs)
                                 blockingp ss scopes)
         (vl-assignstmt->svstmts lhs rhs blockingp ss scopes)))

Theorem: vl-assignstmt->svstmts-vl-rhs-equiv-congruence-on-rhs

(defthm vl-assignstmt->svstmts-vl-rhs-equiv-congruence-on-rhs
 (implies
   (vl-rhs-equiv rhs rhs-equiv)
   (equal
        (vl-assignstmt->svstmts lhs rhs blockingp ss scopes)
        (vl-assignstmt->svstmts lhs rhs-equiv blockingp ss scopes)))
 :rule-classes :congruence)

Theorem: vl-assignstmt->svstmts-of-bool-fix-blockingp

(defthm vl-assignstmt->svstmts-of-bool-fix-blockingp
  (equal (vl-assignstmt->svstmts lhs rhs (acl2::bool-fix blockingp)
                                 ss scopes)
         (vl-assignstmt->svstmts lhs rhs blockingp ss scopes)))

Theorem: vl-assignstmt->svstmts-iff-congruence-on-blockingp

(defthm vl-assignstmt->svstmts-iff-congruence-on-blockingp
 (implies
   (iff blockingp blockingp-equiv)
   (equal
        (vl-assignstmt->svstmts lhs rhs blockingp ss scopes)
        (vl-assignstmt->svstmts lhs rhs blockingp-equiv ss scopes)))
 :rule-classes :congruence)

Theorem: vl-assignstmt->svstmts-of-vl-scopestack-fix-ss

(defthm vl-assignstmt->svstmts-of-vl-scopestack-fix-ss
 (equal
    (vl-assignstmt->svstmts lhs rhs blockingp (vl-scopestack-fix ss)
                            scopes)
    (vl-assignstmt->svstmts lhs rhs blockingp ss scopes)))

Theorem: vl-assignstmt->svstmts-vl-scopestack-equiv-congruence-on-ss

(defthm vl-assignstmt->svstmts-vl-scopestack-equiv-congruence-on-ss
 (implies
   (vl-scopestack-equiv ss ss-equiv)
   (equal
        (vl-assignstmt->svstmts lhs rhs blockingp ss scopes)
        (vl-assignstmt->svstmts lhs rhs blockingp ss-equiv scopes)))
 :rule-classes :congruence)

Theorem: vl-assignstmt->svstmts-of-vl-elabscopes-fix-scopes

(defthm vl-assignstmt->svstmts-of-vl-elabscopes-fix-scopes
 (equal
    (vl-assignstmt->svstmts lhs rhs
                            blockingp ss (vl-elabscopes-fix scopes))
    (vl-assignstmt->svstmts lhs rhs blockingp ss scopes)))

Theorem: vl-assignstmt->svstmts-vl-elabscopes-equiv-congruence-on-scopes

(defthm
    vl-assignstmt->svstmts-vl-elabscopes-equiv-congruence-on-scopes
 (implies
   (vl-elabscopes-equiv scopes scopes-equiv)
   (equal
        (vl-assignstmt->svstmts lhs rhs blockingp ss scopes)
        (vl-assignstmt->svstmts lhs rhs blockingp ss scopes-equiv)))
 :rule-classes :congruence)