• 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
        • Svstmt
        • Sv-tutorial
        • Expressions
          • Rewriting
          • Svex
          • Bit-blasting
            • Svex-focused-equivalence-checking
            • A4vec-operations
            • Svexlist-eval-gl
            • Aig-symbolic-arithmetic
              • Sv::aig-floor-ss-aux
              • Sv::aig-mod-ss-aux
              • Sv::aig-integer-length-s1
              • Sv::aig-logapp-russ
              • Sv::aig-logand-ssss
              • Sv::aig-sign-abs-not-s
              • Sv::aig-ash-ss
              • Sv::aig-+-ss
              • Sv::aig-truncate-ss
              • Sv::aig-logior-sss
              • Sv::aig-logapp-nus-aux
              • Sv::aig-logand-sss
              • Sv::aig-logapp-nus
              • Sv::aig-logapp-nss
              • Sv::aig-ite-bvv-fn-aux
              • Sv::aig-ite-bss-fn-aux
              • Sv::aig-i2v-aux
              • Sv::aig-<-=-ss
              • Sv::aig-*-ss
              • Sv::aig-rem-ss
              • Sv::aig-mod-ss
              • Sv::aig-logxor-ss
              • Sv::aig-lognor-ss
              • Sv::aig-lognand-ss
              • Sv::aig-logior-ss
              • Sv::aig-logeqv-ss
              • Sv::aig-logbitp-n2v
              • Sv::aig-logandc2-ss
              • Sv::aig-logandc1-ss
              • Sv::aig-logand-ss
              • Sv::aig-ite-bvv-fn
              • Sv::aig-ite-bss-fn
              • Sv::aig-floor-ss
              • Sv::aig-expt-su
              • Sv::aig-logtail-ns
              • Sv::aig-loghead-nu
              • Sv::aig-loghead-ns
              • Sv::aig-logext-ns
              • Sv::aig-unary-minus-s
              • Sv::aig-lognot-s
              • Sv::aig-integer-length-s
              • Sv::aig-abs-s
              • Sv::aig-=-ss
              • Sv::aig-<-ss
              • Sv::aig-=-uu
              • Sv::aig-sign-s
              • Sv::aig-i2v
            • Svex-varmasks/env->aig-env-rec
            • Svex-varmasks->a4env-rec
            • Svexlist/env-list-eval-gl
            • 4vmask-to-a4vec-rec-env
            • 4vmask-to-a4vec-rec
            • Svexlist->a4vecs-for-varlist
            • Svex-varmasks/env->aig-env-stats-rec
            • Svexlist->a4vec-nrev
            • A4veclist/svex-env-list-eval
            • A4vec
            • Svexlist-x-out-unused-vars
            • Svex->a4vec-memotable-correctp
            • A4vec/svex-env-eval
            • Svex-varmasks->a4env
            • Svex-varmasks/env->aig-env-rec-log
            • 4vmask-to-a4vec-env
            • 4veclist-from-bitlist-log-rec
            • Svex-apply-aig
            • Svexlist-vars-for-symbolic-eval
            • Nat-bool-a4env-upper-boundp
            • 4vmask-to-a4vec
            • Svexlist/env-list-vars-for-symbolic-eval
            • Svex-maskbits-for-vars
            • Svexlist->a4vec-aig-env-for-varlist
            • 4vec-from-bitlist
            • Svexlist-full-masks-p
            • Svex-varmasks/env->aig-env-stats
            • Svex-varmasks/env->aig-env
            • Svexlistlist->a4vec
            • Svex-const-concat-args
            • Svex-mask-alist-extract-vars
            • Svexlist->a4vec-top
            • Nat-bool-a4vec-upper-boundp
            • Nat-bool-a4env-lower-boundp
            • Maybe-a3vec-fix
            • Svex-maskbits-ok
            • Svex-envlist-check-boolmasks
            • Svex-env-check-boolmasks
            • Nat-bool-list-upper-boundp
            • Nat-bool-a4vec-lower-boundp
            • Maybe-svexlist-rewrite-fixpoint
            • 4vmask-to-a4vec-varcount
            • A4vec-eval
            • Svexlist-nth
            • A4veclist-nth
            • Nat-bool-list-lower-boundp
            • 4veclist-from-bitlist
            • V2i-first-n
            • A4veclist-eval-gl
            • Svex-envlist-keyset
            • Svex-a4vec-env-eval
            • A4veclist/env-list-eval
            • Svexlist-variable-mask-alist
            • Sparseint-nfix
            • A4veclist-length
            • A4veclist-eval
            • 4vec-boolmaskp
            • Nat-bool-list-nats
            • Nat-bool-a4env-p
            • Nat-bool-listp
            • A4veclist->aiglist
            • Svexlist-rewrite-fixpoint-memo
            • Nat-bool-a4vec-p
            • A4vec->aiglist
            • Svex-is-const-concat
            • Nat-bool-a4env-vars
            • Svexlist-mask-alist-memo
            • Nat-bool-a4vec-vars
            • Svexlist-vars-memo
            • A4vec-constantp
            • Svex-aig-memotable
            • Svex-a4vec-env
            • A4veclistlist
            • A4veclist
            • Symbolic-params-x-out-cond
          • Functions
          • 4vmask
          • Why-infinite-width
          • Svex-vars
          • Evaluation
          • Values
        • Symbolic-test-vector
        • Vl-to-svex
      • Fgl
      • Vwsim
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Bit-blasting

Aig-symbolic-arithmetic

A more or less complete set of functions for doing arithmetic on a symbolic bitvector representation consisting of lists of AIGs.

See gl::symbolic-arithmetic. This is almost the same, but for AIGs instead of for gl::bfrs.

Subtopics

Sv::aig-floor-ss-aux
Sv::aig-mod-ss-aux
Sv::aig-integer-length-s1
Sv::aig-logapp-russ
Sv::aig-logand-ssss
Sv::aig-sign-abs-not-s
Sv::aig-ash-ss
Sv::aig-+-ss
Sv::aig-truncate-ss
Sv::aig-logior-sss
Sv::aig-logapp-nus-aux
Sv::aig-logand-sss
Sv::aig-logapp-nus
Sv::aig-logapp-nss
Sv::aig-ite-bvv-fn-aux
Sv::aig-ite-bss-fn-aux
Sv::aig-i2v-aux
Sv::aig-<-=-ss
Sv::aig-*-ss
Sv::aig-rem-ss
Sv::aig-mod-ss
Sv::aig-logxor-ss
Sv::aig-lognor-ss
Sv::aig-lognand-ss
Sv::aig-logior-ss
Sv::aig-logeqv-ss
Sv::aig-logbitp-n2v
Sv::aig-logandc2-ss
Sv::aig-logandc1-ss
Sv::aig-logand-ss
Sv::aig-ite-bvv-fn
Sv::aig-ite-bss-fn
Sv::aig-floor-ss
Sv::aig-expt-su
Sv::aig-logtail-ns
Sv::aig-loghead-nu
Sv::aig-loghead-ns
Sv::aig-logext-ns
Sv::aig-unary-minus-s
Sv::aig-lognot-s
Sv::aig-integer-length-s
Sv::aig-abs-s
Sv::aig-=-ss
Sv::aig-<-ss
Sv::aig-=-uu
Sv::aig-sign-s
Sv::aig-i2v
Like i2v but for AIGs only.