• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Fgl
    • Vwsim
    • Vl
      • Syntax
      • Loader
      • Warnings
      • Getting-started
      • Utilities
      • Printer
      • Kit
      • Mlib
        • Scopestack
        • Hid-tools
        • Filtering-by-name
        • Vl-interface-mocktype
        • Stripping-functions
        • Genblob
        • Expr-tools
        • Extract-vl-types
        • Hierarchy
        • Range-tools
        • Finding-by-name
        • Stmt-tools
          • Vl-rebuild-caselist
          • Vl-stmt-atomicstmts
          • Vl-compoundstmt->stmts
          • Vl-compoundstmt->exprs
          • Vl-compoundstmt->vardecls
          • Change-vl-compoundstmt
            • Change-vl-compoundstmt-core
          • Vl-compoundstmt->paramdecls
          • Vl-compoundstmt->ctrl
          • Vl-atomicstmtlist-p
          • Vl-stmt->atts
          • Vl-atomicstmt-p
          • Vl-timingstmt-p
          • Vl-repeatstmt-p
          • Vl-foreverstmt-p
          • Vl-assignstmt-p
          • Vl-whilestmt-p
          • Vl-waitstmt-p
          • Vl-nullstmt-p
          • Vl-ifstmt-p
          • Vl-forstmt-p
          • Vl-dostmt-p
          • Vl-casestmt-p
          • Vl-callstmt-p
          • Vl-exprlistlist
        • Modnamespace
        • Flat-warnings
        • Reordering-by-name
        • Datatype-tools
        • Syscalls
        • Allexprs
        • Lvalues
        • Port-tools
      • Transforms
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Change-vl-compoundstmt

Change-vl-compoundstmt-core

Mutate an arbitrary compound (non-atomic) statement.

Signature

(change-vl-compoundstmt-core x stmts exprs ctrl vardecls paramdecls) 
  → 
new-x

Arguments

x — Initial compound statement, to be updated.
    Guard (vl-stmt-p x).

stmts — New statements to install. Should agree in length with vl-compoundstmt->stmts.
    Guard (vl-stmtlist-p stmts).

exprs — New expressions to install. Should agree in length with vl-compoundstmt->exprs.
    Guard (vl-exprlist-p exprs).

ctrl — New timing control to install, for timing statements only.
    Guard (vl-maybe-delayoreventcontrol-p ctrl).

vardecls — New variable declarations to install.
    Guard (vl-vardecllist-p vardecls).

paramdecls — New parameter declarations to install.
    Guard (vl-paramdecllist-p paramdecls).

Returns

new-x — Type (vl-stmt-p new-x).

Definitions and Theorems

Function: change-vl-compoundstmt-core

(defun change-vl-compoundstmt-core
       (x stmts exprs ctrl vardecls paramdecls)
 (declare (xargs :guard (and (vl-stmt-p x)
                             (vl-stmtlist-p stmts)
                             (vl-exprlist-p exprs)
                             (vl-maybe-delayoreventcontrol-p ctrl)
                             (vl-vardecllist-p vardecls)
                             (vl-paramdecllist-p paramdecls))))
 (declare
  (xargs :guard (and (not (vl-atomicstmt-p x))
                     (same-lengthp stmts (vl-compoundstmt->stmts x))
                     (same-lengthp exprs (vl-compoundstmt->exprs x))
                     (iff ctrl (vl-compoundstmt->ctrl x))
                     (or (not vardecls)
                         (member (vl-stmt-kind x)
                                 '(:vl-blockstmt :vl-forstmt)))
                     (or (not paramdecls)
                         (vl-stmt-case x :vl-blockstmt)))))
 (let ((__function__ 'change-vl-compoundstmt-core))
  (declare (ignorable __function__))
  (let ((x (vl-stmt-fix x)))
   (vl-stmt-case
    x :vl-casestmt
    (change-vl-casestmt
         x
         :default (first stmts)
         :test (first exprs)
         :caselist (vl-rebuild-caselist x.caselist (rest exprs)
                                        (rest stmts)))
    :vl-ifstmt
    (change-vl-ifstmt x
                      :condition (first exprs)
                      :truebranch (first stmts)
                      :falsebranch (second stmts))
    :vl-foreverstmt
    (change-vl-foreverstmt x
                           :body (first stmts))
    :vl-waitstmt
    (change-vl-waitstmt x
                        :condition (first exprs)
                        :body (first stmts))
    :vl-whilestmt
    (change-vl-whilestmt x
                         :condition (first exprs)
                         :body (first stmts))
    :vl-dostmt
    (change-vl-dostmt x
                      :condition (first exprs)
                      :body (first stmts))
    :vl-forstmt
    (b*
      ((ninitassigns (len x.initassigns))
       (nstepforms (len x.stepforms))
       (stmts (vl-stmtlist-fix stmts))
       (stmts-starting-with-stepforms (nthcdr ninitassigns stmts)))
      (change-vl-forstmt
           x
           :initdecls vardecls
           :initassigns (take ninitassigns stmts)
           :test (first exprs)
           :stepforms (take nstepforms
                            stmts-starting-with-stepforms)
           :body (nth nstepforms
                      stmts-starting-with-stepforms)))
    :vl-foreachstmt (change-vl-foreachstmt x
                                           :vardecls vardecls
                                           :body (first stmts))
    :vl-repeatstmt (change-vl-repeatstmt x
                                         :condition (first exprs)
                                         :body (first stmts))
    :vl-blockstmt (change-vl-blockstmt x
                                       :vardecls vardecls
                                       :paramdecls paramdecls
                                       :stmts stmts)
    :vl-timingstmt (change-vl-timingstmt x
                                         :ctrl ctrl
                                         :body (first stmts))
    :vl-assertstmt
    (change-vl-assertstmt
         x
         :assertion (change-vl-assertion x.assertion
                                         :condition (first exprs)
                                         :success (first stmts)
                                         :failure (second stmts)))
    :vl-cassertstmt
    (change-vl-cassertstmt
         x
         :cassertion (change-vl-cassertion x.cassertion
                                           :success (first stmts)
                                           :failure (second stmts)))
    :vl-nullstmt (progn$ (impossible) x)
    :vl-assignstmt (progn$ (impossible) x)
    :vl-deassignstmt (progn$ (impossible) x)
    :vl-callstmt (progn$ (impossible) x)
    :vl-disablestmt (progn$ (impossible) x)
    :vl-breakstmt (progn$ (impossible) x)
    :vl-continuestmt (progn$ (impossible) x)
    :vl-returnstmt (progn$ (impossible) x)
    :vl-eventtriggerstmt (progn$ (impossible) x)))))

Theorem: vl-stmt-p-of-change-vl-compoundstmt-core

(defthm vl-stmt-p-of-change-vl-compoundstmt-core
  (b* ((new-x (change-vl-compoundstmt-core
                   x
                   stmts exprs ctrl vardecls paramdecls)))
    (vl-stmt-p new-x))
  :rule-classes :rewrite)

Theorem: change-vl-compoundstmt-core-identity

(defthm change-vl-compoundstmt-core-identity
  (equal
       (change-vl-compoundstmt-core x (vl-compoundstmt->stmts x)
                                    (vl-compoundstmt->exprs x)
                                    (vl-compoundstmt->ctrl x)
                                    (vl-compoundstmt->vardecls x)
                                    (vl-compoundstmt->paramdecls x))
       (vl-stmt-fix x)))

Theorem: vl-stmtlist-fix-of-take

(defthm vl-stmtlist-fix-of-take
  (implies (<= (nfix n) (len x))
           (equal (vl-stmtlist-fix (take n x))
                  (take n (vl-stmtlist-fix x)))))

Theorem: vl-stmtlist-fix-of-nthcdr

(defthm vl-stmtlist-fix-of-nthcdr
  (equal (vl-stmtlist-fix (nthcdr n x))
         (nthcdr n (vl-stmtlist-fix x))))

Theorem: vl-stmt-fix-of-nth

(defthm vl-stmt-fix-of-nth
  (implies (< (nfix n) (len x))
           (equal (vl-stmt-fix (nth n x))
                  (nth n (vl-stmtlist-fix x)))))

Theorem: vl-compoundstmt->stmts-of-change-vl-compoundstmt-core

(defthm vl-compoundstmt->stmts-of-change-vl-compoundstmt-core
  (implies (same-lengthp stmts (vl-compoundstmt->stmts x))
           (equal (vl-compoundstmt->stmts
                       (change-vl-compoundstmt-core
                            x stmts exprs ctrl vardecls paramdecls))
                  (vl-stmtlist-fix stmts))))

Theorem: vl-compoundstmt->exprs-of-change-vl-compoundstmt-core

(defthm vl-compoundstmt->exprs-of-change-vl-compoundstmt-core
  (implies (same-lengthp exprs (vl-compoundstmt->exprs x))
           (equal (vl-compoundstmt->exprs
                       (change-vl-compoundstmt-core
                            x stmts exprs ctrl vardecls paramdecls))
                  (list-fix (vl-exprlist-fix exprs)))))

Theorem: vl-compoundstmt->ctrl-of-change-vl-compoundstmt-core

(defthm vl-compoundstmt->ctrl-of-change-vl-compoundstmt-core
  (implies (iff ctrl (vl-compoundstmt->ctrl x))
           (equal (vl-compoundstmt->ctrl
                       (change-vl-compoundstmt-core
                            x stmts exprs ctrl vardecls paramdecls))
                  (vl-maybe-delayoreventcontrol-fix ctrl))))

Theorem: vl-compoundstmt->ctrl-of-change-vl-compoundstmt-vardecls

(defthm vl-compoundstmt->ctrl-of-change-vl-compoundstmt-vardecls
  (implies (or (not vardecls)
               (equal (vl-stmt-kind x) :vl-blockstmt)
               (equal (vl-stmt-kind x) :vl-forstmt))
           (equal (vl-compoundstmt->vardecls
                       (change-vl-compoundstmt-core
                            x stmts exprs ctrl vardecls paramdecls))
                  (vl-vardecllist-fix vardecls))))

Theorem: vl-compoundstmt->ctrl-of-change-vl-compoundstmt-paramdecls

(defthm vl-compoundstmt->ctrl-of-change-vl-compoundstmt-paramdecls
  (implies (or (not paramdecls)
               (vl-stmt-case x :vl-blockstmt))
           (equal (vl-compoundstmt->paramdecls
                       (change-vl-compoundstmt-core
                            x stmts exprs ctrl vardecls paramdecls))
                  (vl-paramdecllist-fix paramdecls))))

Theorem: change-vl-compoundstmt-core-of-vl-stmt-fix-x

(defthm change-vl-compoundstmt-core-of-vl-stmt-fix-x
 (equal
  (change-vl-compoundstmt-core (vl-stmt-fix x)
                               stmts exprs ctrl vardecls paramdecls)
  (change-vl-compoundstmt-core
       x
       stmts exprs ctrl vardecls paramdecls)))

Theorem: change-vl-compoundstmt-core-vl-stmt-equiv-congruence-on-x

(defthm change-vl-compoundstmt-core-vl-stmt-equiv-congruence-on-x
  (implies (vl-stmt-equiv x x-equiv)
           (equal (change-vl-compoundstmt-core
                       x stmts exprs ctrl vardecls paramdecls)
                  (change-vl-compoundstmt-core
                       x-equiv
                       stmts exprs ctrl vardecls paramdecls)))
  :rule-classes :congruence)

Theorem: change-vl-compoundstmt-core-of-vl-stmtlist-fix-stmts

(defthm change-vl-compoundstmt-core-of-vl-stmtlist-fix-stmts
 (equal (change-vl-compoundstmt-core x (vl-stmtlist-fix stmts)
                                     exprs ctrl vardecls paramdecls)
        (change-vl-compoundstmt-core
             x
             stmts exprs ctrl vardecls paramdecls)))

Theorem: change-vl-compoundstmt-core-vl-stmtlist-equiv-congruence-on-stmts

(defthm
  change-vl-compoundstmt-core-vl-stmtlist-equiv-congruence-on-stmts
 (implies
  (vl-stmtlist-equiv stmts stmts-equiv)
  (equal
      (change-vl-compoundstmt-core
           x stmts exprs ctrl vardecls paramdecls)
      (change-vl-compoundstmt-core x stmts-equiv
                                   exprs ctrl vardecls paramdecls)))
 :rule-classes :congruence)

Theorem: change-vl-compoundstmt-core-of-vl-exprlist-fix-exprs

(defthm change-vl-compoundstmt-core-of-vl-exprlist-fix-exprs
 (equal (change-vl-compoundstmt-core x stmts (vl-exprlist-fix exprs)
                                     ctrl vardecls paramdecls)
        (change-vl-compoundstmt-core
             x
             stmts exprs ctrl vardecls paramdecls)))

Theorem: change-vl-compoundstmt-core-vl-exprlist-equiv-congruence-on-exprs

(defthm
  change-vl-compoundstmt-core-vl-exprlist-equiv-congruence-on-exprs
  (implies (vl-exprlist-equiv exprs exprs-equiv)
           (equal (change-vl-compoundstmt-core
                       x stmts exprs ctrl vardecls paramdecls)
                  (change-vl-compoundstmt-core
                       x stmts
                       exprs-equiv ctrl vardecls paramdecls)))
  :rule-classes :congruence)

Theorem: change-vl-compoundstmt-core-of-vl-maybe-delayoreventcontrol-fix-ctrl

(defthm
 change-vl-compoundstmt-core-of-vl-maybe-delayoreventcontrol-fix-ctrl
 (equal (change-vl-compoundstmt-core
             x stmts exprs
             (vl-maybe-delayoreventcontrol-fix ctrl)
             vardecls paramdecls)
        (change-vl-compoundstmt-core
             x
             stmts exprs ctrl vardecls paramdecls)))

Theorem: change-vl-compoundstmt-core-vl-maybe-delayoreventcontrol-equiv-congruence-on-ctrl

(defthm
 change-vl-compoundstmt-core-vl-maybe-delayoreventcontrol-equiv-congruence-on-ctrl
 (implies (vl-maybe-delayoreventcontrol-equiv ctrl ctrl-equiv)
          (equal (change-vl-compoundstmt-core
                      x stmts exprs ctrl vardecls paramdecls)
                 (change-vl-compoundstmt-core
                      x stmts
                      exprs ctrl-equiv vardecls paramdecls)))
 :rule-classes :congruence)

Theorem: change-vl-compoundstmt-core-of-vl-vardecllist-fix-vardecls

(defthm change-vl-compoundstmt-core-of-vl-vardecllist-fix-vardecls
  (equal (change-vl-compoundstmt-core
              x stmts
              exprs ctrl (vl-vardecllist-fix vardecls)
              paramdecls)
         (change-vl-compoundstmt-core
              x
              stmts exprs ctrl vardecls paramdecls)))

Theorem: change-vl-compoundstmt-core-vl-vardecllist-equiv-congruence-on-vardecls

(defthm
 change-vl-compoundstmt-core-vl-vardecllist-equiv-congruence-on-vardecls
 (implies (vl-vardecllist-equiv vardecls vardecls-equiv)
          (equal (change-vl-compoundstmt-core
                      x stmts exprs ctrl vardecls paramdecls)
                 (change-vl-compoundstmt-core
                      x stmts
                      exprs ctrl vardecls-equiv paramdecls)))
 :rule-classes :congruence)

Theorem: change-vl-compoundstmt-core-of-vl-paramdecllist-fix-paramdecls

(defthm
     change-vl-compoundstmt-core-of-vl-paramdecllist-fix-paramdecls
 (equal
     (change-vl-compoundstmt-core x stmts exprs ctrl vardecls
                                  (vl-paramdecllist-fix paramdecls))
     (change-vl-compoundstmt-core
          x
          stmts exprs ctrl vardecls paramdecls)))

Theorem: change-vl-compoundstmt-core-vl-paramdecllist-equiv-congruence-on-paramdecls

(defthm
 change-vl-compoundstmt-core-vl-paramdecllist-equiv-congruence-on-paramdecls
 (implies (vl-paramdecllist-equiv paramdecls paramdecls-equiv)
          (equal (change-vl-compoundstmt-core
                      x stmts exprs ctrl vardecls paramdecls)
                 (change-vl-compoundstmt-core
                      x stmts
                      exprs ctrl vardecls paramdecls-equiv)))
 :rule-classes :congruence)