• 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
        • Svstmt-case
        • Svstmt-while
        • Svstmt-p
        • Svstmt-if
        • Svstmt-equiv
        • Svstmt-xcond
        • Svstmt-scope
        • Svstmt-assign
        • Svstmt-compile
          • Svstmt-compile.lisp
            • Svstate-merge-branches
            • Svex-alist-merge-branches
            • Svstmt-assign->subst
            • Svstack-merge-branches
            • Svstacks-compatible
            • Svjumpstate-merge-svstate-branches
            • Svjumpstate-svstate-compatible
            • Svstmt-lhs-check-masks
            • Svjumpstate
            • Svjumpstates-compatible
            • Svstmtlist-compile-top
            • Svjumpstate-sequence-svstates
            • Constraintlist-merge-branches
            • Svjumpstate-merge-branches
            • Svex-replace-range
            • Svex-svstmt-ite
            • Svstmt-process-write
            • Svjumpstate-sequence
            • Svstmt-process-writelist
            • Svstack-assign
            • Svstmt-writelist-var-sizes
            • Svstates-compatible
            • 4vec-replace-range
            • Svstmt-write-var-sizes
            • Make-empty-svjumpstate
            • Constraintlist-add-pathcond
            • Svjumpstate-pop-scope
            • Constraintlist-compose-svstack
            • Svstack-to-svex-alist
            • Svstack-filter-global-lhs-vars
            • Svjumpstate-vars
            • Svex-svstmt-or
            • Svex-svstmt-andc1
            • Svstate-push-scope
            • Svstate-pop-scope
            • Svstate-vars
            • Svstack-lookup
            • Svar-subtract-delay
            • Svstmt-initialize-locals
            • Svstack-fork
            • Svstack-clean
            • Svstack-nonempty-fix
            • Svstate-fork
            • Svstate-clean
            • Svstack-globalp
            • Svjumpstate-fork
            • Svar-delayed-member
            • Svjumpstate-levels
            • Svjumpstate-free
            • Svstate-free
            • Svstack-free
            • Svstack
            • Svar-size-alist
          • Svstate
        • Svstmt-constraints
        • Svstmt-jump
        • Svstmtlist
        • Svstmt-kind
        • Svstmt.lisp
        • Svstmt-fix
        • Svstmt-count
      • Sv-tutorial
      • Expressions
      • Symbolic-test-vector
      • Vl-to-svex
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Svstmt-compile.lisp

Svstmt-assign->subst

Signature

(svstmt-assign->subst lhs rhs offset blockingp st) → new-st

Arguments

lhs — E.g., {a[3:0], b[2:1]}, reverse order lhs.
    Guard (lhs-p lhs).

rhs — Guard (svex-p rhs).

offset — Total bits of the lhs we've processed so far.
    Guard (natp offset).

st — Guard (svstate-p st).

Returns

new-st — Type (svstate-p new-st).

Definitions and Theorems

Function: svstmt-assign->subst

(defun svstmt-assign->subst (lhs rhs offset blockingp st)
 (declare (xargs :guard (and (lhs-p lhs)
                             (svex-p rhs)
                             (natp offset)
                             (svstate-p st))))
 (let ((__function__ 'svstmt-assign->subst))
  (declare (ignorable __function__))
  (b* ((offset (lnfix offset))
       ((mv first rest) (lhs-decomp lhs))
       ((unless first) (svstate-fix st))
       ((lhrange first) first)
       (st (svstmt-assign->subst rest rhs (+ offset first.w)
                                 blockingp st))
       ((svstate st)))
   (lhatom-case
     first.atom :z st :var
     (b* ((var first.atom.name)
          (binding (or (if blockingp (svstack-lookup var st.blkst)
                         (svex-fastlookup var st.nonblkst))
                       (make-svex-var :name var)))
          (new-val (svex-replace-range binding
                                       :lsb first.atom.rsh
                                       :width first.w
                                       :val (svex-rsh offset rhs)))
          (new-alist
               (if blockingp
                   (svstack-assign first.atom.name new-val st.blkst)
                 (hons-acons first.atom.name new-val st.nonblkst)))
          (st (if blockingp (change-svstate st :blkst new-alist)
                (change-svstate st
                                :nonblkst new-alist))))
       st)))))

Theorem: svstate-p-of-svstmt-assign->subst

(defthm svstate-p-of-svstmt-assign->subst
  (b* ((new-st (svstmt-assign->subst lhs rhs offset blockingp st)))
    (svstate-p new-st))
  :rule-classes :rewrite)

Theorem: svex-p-nonnil-compound-recognizer

(defthm svex-p-nonnil-compound-recognizer
  (implies (svex-p x) x)
  :rule-classes :compound-recognizer)

Theorem: svstmt-assign->subst-preserves-blkst-when-nonblocking

(defthm svstmt-assign->subst-preserves-blkst-when-nonblocking
  (equal
       (svstate->blkst (svstmt-assign->subst lhs rhs offset nil st))
       (svstate->blkst st)))

Theorem: svstmt-assign->subst-preserves-nonblkst-when-blocking

(defthm svstmt-assign->subst-preserves-nonblkst-when-blocking
 (equal
      (svstate->nonblkst (svstmt-assign->subst lhs rhs offset t st))
      (svstate->nonblkst st)))

Theorem: keys-of-svstmt-assign->subst-blkst

(defthm keys-of-svstmt-assign->subst-blkst
 (implies
  (and
     (not (svex-lookup v
                       (svstack-to-svex-alist (svstate->blkst st))))
     (not (member (svar-fix v) (lhs-vars lhs))))
  (not
   (svex-lookup
    v
    (svstack-to-svex-alist
       (svstate->blkst
            (svstmt-assign->subst lhs rhs offset blockingp st)))))))

Theorem: keys-of-svstmt-assign->subst-nonblkst

(defthm keys-of-svstmt-assign->subst-nonblkst
 (implies
  (and (not (svex-lookup v (svstate->nonblkst st)))
       (not (member (svar-fix v) (lhs-vars lhs))))
  (not
   (svex-lookup
        v
        (svstate->nonblkst
             (svstmt-assign->subst lhs rhs offset blockingp st))))))

Theorem: vars-of-svstmt-assign->subst-blkst

(defthm vars-of-svstmt-assign->subst-blkst
 (implies
  (and
   (not
    (member
     v
     (svex-alist-vars (svstack-to-svex-alist (svstate->blkst st)))))
   (not (member v (lhs-vars lhs)))
   (not (member v (svex-vars rhs))))
  (not
   (member
    v
    (svex-alist-vars
     (svstack-to-svex-alist
      (svstate->blkst
           (svstmt-assign->subst lhs rhs offset blockingp st))))))))

Theorem: vars-of-svstmt-assign->subst-nonblkst

(defthm vars-of-svstmt-assign->subst-nonblkst
 (implies
  (and (not (member v
                    (svex-alist-vars (svstate->nonblkst st))))
       (not (member v (lhs-vars lhs)))
       (not (member v (svex-vars rhs))))
  (not
   (member
    v
    (svex-alist-vars
       (svstate->nonblkst
            (svstmt-assign->subst lhs rhs offset blockingp st)))))))

Theorem: vars-of-svstmt-assign->subst

(defthm vars-of-svstmt-assign->subst
 (implies
  (and (not (member v (svstate-vars st)))
       (not (member v (lhs-vars lhs)))
       (not (member v (svex-vars rhs))))
  (not
   (member
        v
        (svstate-vars
             (svstmt-assign->subst lhs rhs offset blockingp st))))))

Theorem: consp-blkst-of-svstmt-assign->subst

(defthm consp-blkst-of-svstmt-assign->subst
  (b* ((?new-st (svstmt-assign->subst lhs rhs offset blockingp st)))
    (implies (consp (svstate->blkst st))
             (consp (svstate->blkst new-st)))))

Theorem: len-blkst-of-svstmt-assign->subst

(defthm len-blkst-of-svstmt-assign->subst
  (b* ((?new-st (svstmt-assign->subst lhs rhs offset blockingp st)))
    (<= (len (svstate->blkst st))
        (len (svstate->blkst new-st))))
  :rule-classes :linear)

Theorem: svstates-compatible-of-svstmt-assign->subst

(defthm svstates-compatible-of-svstmt-assign->subst
  (b* ((?new-st (svstmt-assign->subst lhs rhs offset blockingp st)))
    (implies (consp (svstate->blkst st))
             (svstates-compatible new-st st))))

Theorem: svstmt-assign->subst-of-lhs-fix-lhs

(defthm svstmt-assign->subst-of-lhs-fix-lhs
  (equal (svstmt-assign->subst (lhs-fix lhs)
                               rhs offset blockingp st)
         (svstmt-assign->subst lhs rhs offset blockingp st)))

Theorem: svstmt-assign->subst-lhs-equiv-congruence-on-lhs

(defthm svstmt-assign->subst-lhs-equiv-congruence-on-lhs
 (implies
   (lhs-equiv lhs lhs-equiv)
   (equal (svstmt-assign->subst lhs rhs offset blockingp st)
          (svstmt-assign->subst lhs-equiv rhs offset blockingp st)))
 :rule-classes :congruence)

Theorem: svstmt-assign->subst-of-svex-fix-rhs

(defthm svstmt-assign->subst-of-svex-fix-rhs
  (equal (svstmt-assign->subst lhs (svex-fix rhs)
                               offset blockingp st)
         (svstmt-assign->subst lhs rhs offset blockingp st)))

Theorem: svstmt-assign->subst-svex-equiv-congruence-on-rhs

(defthm svstmt-assign->subst-svex-equiv-congruence-on-rhs
 (implies
   (svex-equiv rhs rhs-equiv)
   (equal (svstmt-assign->subst lhs rhs offset blockingp st)
          (svstmt-assign->subst lhs rhs-equiv offset blockingp st)))
 :rule-classes :congruence)

Theorem: svstmt-assign->subst-of-nfix-offset

(defthm svstmt-assign->subst-of-nfix-offset
  (equal (svstmt-assign->subst lhs rhs (nfix offset)
                               blockingp st)
         (svstmt-assign->subst lhs rhs offset blockingp st)))

Theorem: svstmt-assign->subst-nat-equiv-congruence-on-offset

(defthm svstmt-assign->subst-nat-equiv-congruence-on-offset
 (implies
   (nat-equiv offset offset-equiv)
   (equal (svstmt-assign->subst lhs rhs offset blockingp st)
          (svstmt-assign->subst lhs rhs offset-equiv blockingp st)))
 :rule-classes :congruence)

Theorem: svstmt-assign->subst-of-svstate-fix-st

(defthm svstmt-assign->subst-of-svstate-fix-st
 (equal (svstmt-assign->subst lhs
                              rhs offset blockingp (svstate-fix st))
        (svstmt-assign->subst lhs rhs offset blockingp st)))

Theorem: svstmt-assign->subst-svstate-equiv-congruence-on-st

(defthm svstmt-assign->subst-svstate-equiv-congruence-on-st
 (implies
   (svstate-equiv st st-equiv)
   (equal (svstmt-assign->subst lhs rhs offset blockingp st)
          (svstmt-assign->subst lhs rhs offset blockingp st-equiv)))
 :rule-classes :congruence)