• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • 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
          • Address
          • Wire
          • Module
          • Lhs
            • Lhs.lisp
              • Lhs-vars-normorderedp
              • Lhs-norm
              • Lhatom-normorderedp
              • Lhs-normp
              • Svex-lhsrewrite-aux
                • Lhs-concat
                • Lhs-check-masks
                • Lhrange-combine
                • Svexarr-vars-aux
                • Assigns-check-masks
                • Svex->lhs-range
                • Svex-lhs-preproc-blkrev
                • Svarlist-boundedp-badguy
                • Driverlist-rest-after-strength
                • Aliases-normorderedp
                • Lhs-rsh
                • Lhs-cons
                • Svarlist-boundedp
                • Lhs-bitproj
                • Lhs-vars
                • Driver
                • Svex-override
                • Make-simple-lhs
                • Lhssvex-range-p
                • Lhs-override
                • Lhs-first-aux
                • Lhrange-combinable-dec
                • Lhrange-bitproj
                • Lhatom
                • Driverlist-values-of-strength
                • Lhs-rest-aux
                • Lhs-rest
                • Aliases-normorderedp-aux
                • Svexarr-vars
                • Lhsarr-to-svexarr
                • Svexarr-vars-witness-aux
                • Lhbit
                • Svex-lhsrewrite
                • Svar-boundedp
                • Lhs-decomp-aux
                • Svex->lhs-bound
                • Aliases-vars-aux
                • Svexarr
                • Svexarr-vars-witness
                • Svar-set-index
                • Lhsarr
                • Lhs-override-vars
                • Lhatom-eval-zero
                • Lhatom-bitproj
                • Lhrange-nextbit
                • Lhrange-combinable
                • Driverlist->svex
                • Svexlist-resolve
                • Lhs->svex-zero
                • Lhs-overridelist-vars
                • Lhs-overridelist-keys
                • Lhbit-eval
                • Driverlist-vars
                • Assigns-vars
                • Svex-int
                • Lhssvex-bounded-p
                • Lhslist-vars
                • Lhs-decomp
                • Lhatom-vars
                • Svar-map-vars
                • Lhssvex-unbounded-p
                • Lhspairs-vars
                • Lhs-width
                • Aliases-vars
                • Lhs-first
                • Svar-index
                • Assigns
                • Svar-indexedp
                • Lhspairs
                • Svex-overridelist
                • Lhslist
                • Lhs-overridelist
                • Driverlist
                • Svex-lhs-preproc
                • Svexarr-fix
                • Lhsarr-fix
              • Lhs-p
              • Lhs-fix
              • Lhrange
              • Lhs-eval-zx
              • Lhs-equiv
              • Lhs-eval
              • Lhs->svex
            • Path
            • Svar-add-namespace
            • Design
            • Modinst
            • Lhs-add-namespace
            • Modalist
            • Path-add-namespace
            • Modname->submodnames
            • Name
            • Constraintlist-addr-p
            • Svex-alist-addr-p
            • Svar-map-addr-p
            • Lhspairs-addr-p
            • Modname
            • Assigns-addr-p
            • Lhs-addr-p
            • Lhatom-addr-p
            • Modhier-list-measure
            • Attributes
            • Modhier-measure
            • Modhier-list-measure-aux
            • Modhier-loopfreelist-p
            • Modhier-loopfree-p
          • Svstmt
          • Sv-tutorial
          • Expressions
          • Symbolic-test-vector
          • Vl-to-svex
        • Fgl
        • Vwsim
        • Vl
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Lhs.lisp

    Svex-lhsrewrite-aux

    Signature
    (svex-lhsrewrite-aux x shift w) → xx
    Arguments
    x — Guard (svex-p x).
    shift — Guard (natp shift).
    w — Guard (natp w).
    Returns
    xx — Type (svex-p xx).

    Definitions and Theorems

    Function: svex-lhsrewrite-aux

    (defun svex-lhsrewrite-aux (x shift w)
     (declare (xargs :guard (and (svex-p x) (natp shift) (natp w))))
     (let ((__function__ 'svex-lhsrewrite-aux))
      (declare (ignorable __function__))
      (svex-case
       x :var (svex-fix x)
       :quote (svex-fix x)
       :call
       (b* ((shift (lnfix shift)) (w (lnfix w)))
        (case x.fn
         (concat
          (b*
           (((unless
                  (and (eql (len x.args) 3)
                       (eq (svex-kind (first x.args)) :quote)
                       (4vec-index-p (svex-quote->val (first x.args)))))
             (svex-fix x))
            (xw (2vec->val (svex-quote->val (first x.args))))
            ((when (<= xw shift))
             (svex-concat xw (svex-quote (4vec-z))
                          (svex-lhsrewrite-aux (third x.args)
                                               (- shift xw)
                                               w)))
            ((when (<= (+ shift w) xw))
             (svex-lhsrewrite-aux (second x.args)
                                  shift w))
            (low (svex-lhsrewrite-aux (second x.args)
                                      shift (- xw shift)))
            (high (svex-lhsrewrite-aux (third x.args)
                                       0 (- (+ shift w) xw))))
           (svex-concat xw low high)))
         (signx
          (b*
           (((unless
                  (and (eql (len x.args) 2)
                       (eq (svex-kind (first x.args)) :quote)
                       (4vec-index-p (svex-quote->val (first x.args)))))
             (svex-fix x))
            (xw (2vec->val (svex-quote->val (first x.args))))
            ((when (<= xw shift)) (svex-fix x))
            ((when (<= (+ shift w) xw))
             (svex-lhsrewrite-aux (second x.args)
                                  shift w)))
           (svex-fix x)))
         (rsh
          (b*
           (((unless
                  (and (eql (len x.args) 2)
                       (eq (svex-kind (first x.args)) :quote)
                       (4vec-index-p (svex-quote->val (first x.args)))))
             (svex-fix x))
            (xsh (2vec->val (svex-quote->val (first x.args)))))
           (svex-rsh xsh
                     (svex-lhsrewrite-aux (second x.args)
                                          (+ shift xsh)
                                          w))))
         (otherwise (svex-fix x)))))))

    Theorem: svex-p-of-svex-lhsrewrite-aux

    (defthm svex-p-of-svex-lhsrewrite-aux
      (b* ((xx (svex-lhsrewrite-aux x shift w)))
        (svex-p xx))
      :rule-classes :rewrite)

    Theorem: svex-lhsrewrite-aux-of-svex-fix-x

    (defthm svex-lhsrewrite-aux-of-svex-fix-x
      (equal (svex-lhsrewrite-aux (svex-fix x)
                                  shift w)
             (svex-lhsrewrite-aux x shift w)))

    Theorem: svex-lhsrewrite-aux-svex-equiv-congruence-on-x

    (defthm svex-lhsrewrite-aux-svex-equiv-congruence-on-x
      (implies (svex-equiv x x-equiv)
               (equal (svex-lhsrewrite-aux x shift w)
                      (svex-lhsrewrite-aux x-equiv shift w)))
      :rule-classes :congruence)

    Theorem: svex-lhsrewrite-aux-of-nfix-shift

    (defthm svex-lhsrewrite-aux-of-nfix-shift
      (equal (svex-lhsrewrite-aux x (nfix shift) w)
             (svex-lhsrewrite-aux x shift w)))

    Theorem: svex-lhsrewrite-aux-nat-equiv-congruence-on-shift

    (defthm svex-lhsrewrite-aux-nat-equiv-congruence-on-shift
      (implies (nat-equiv shift shift-equiv)
               (equal (svex-lhsrewrite-aux x shift w)
                      (svex-lhsrewrite-aux x shift-equiv w)))
      :rule-classes :congruence)

    Theorem: svex-lhsrewrite-aux-of-nfix-w

    (defthm svex-lhsrewrite-aux-of-nfix-w
      (equal (svex-lhsrewrite-aux x shift (nfix w))
             (svex-lhsrewrite-aux x shift w)))

    Theorem: svex-lhsrewrite-aux-nat-equiv-congruence-on-w

    (defthm svex-lhsrewrite-aux-nat-equiv-congruence-on-w
      (implies (nat-equiv w w-equiv)
               (equal (svex-lhsrewrite-aux x shift w)
                      (svex-lhsrewrite-aux x shift w-equiv)))
      :rule-classes :congruence)

    Theorem: svex-lhsrewrite-aux-correct-lemma

    (defthm svex-lhsrewrite-aux-correct-lemma
     (equal
       (4vec-concat (2vec (nfix w))
                    (4vec-rsh (2vec (nfix shift))
                              (svex-eval (svex-lhsrewrite-aux x shift w)
                                         env))
                    (4vec-z))
       (4vec-concat (2vec (nfix w))
                    (4vec-rsh (2vec (nfix shift))
                              (svex-eval x env))
                    (4vec-z))))

    Theorem: svex-lhsrewrite-aux-vars

    (defthm svex-lhsrewrite-aux-vars
      (implies (not (member v (svex-vars x)))
               (not (member v
                            (svex-vars (svex-lhsrewrite-aux x sh w))))))