• 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-lhs-preproc

    Preprocesses an expression into one that only contains concat, rsh, and signx operators.

    Signature
    (svex-lhs-preproc x) → new-x
    Arguments
    x — Guard (svex-p x).
    Returns
    new-x — Type (svex-p new-x).

    Handles zerox, blkrev, bitsel operators.