• 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
        • Functions
        • 4vmask
        • Why-infinite-width
        • Svex-vars
        • Evaluation
          • Svex-xeval
          • Svex-mono-eval
          • Svex-eval
          • Svex-apply
          • Svex-env
          • Svex-alist-eval
          • Svar-boolmasks-lookup
          • Svex-s4eval
            • Svex-s4xeval
              • Svexlist-s4xeval
              • Svex-fn/args-s4xeval
              • Svex-call-s4xeval
          • Svexlist-unquote
          • Svex-alist-eval-for-symbolic
          • Svexlist-eval
          • Svexlist-quotesp
          • Svar-boolmasks
          • Svexlist-s4eval
          • Svexlist-eval-for-symbolic
        • Values
      • Symbolic-test-vector
      • Vl-to-svex
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Svex-s4eval

Svex-s4xeval

Evaluate an svex using s4vecs in an all-X environment.

Signature

(svex-s4xeval x) → val

Arguments

x — Expression to evaluate.
    Guard (svex-p x).

Returns

val — Indication of always-constant bits (see below).
    Type (s4vec-p val).

Theorem: return-type-of-svex-s4xeval.val

(defthm return-type-of-svex-s4xeval.val
  (b* ((?val (svex-s4xeval x)))
    (s4vec-p val))
  :rule-classes :rewrite)

Theorem: return-type-of-svex-call-s4xeval.val

(defthm return-type-of-svex-call-s4xeval.val
  (b* ((?val (svex-call-s4xeval x)))
    (s4vec-p val))
  :rule-classes :rewrite)

Theorem: return-type-of-svex-fn/args-s4xeval.val

(defthm return-type-of-svex-fn/args-s4xeval.val
  (b* ((?val (svex-fn/args-s4xeval fn args)))
    (s4vec-p val))
  :rule-classes :rewrite)

Theorem: return-type-of-svexlist-s4xeval.val

(defthm return-type-of-svexlist-s4xeval.val
  (b* ((?val (svexlist-s4xeval x)))
    (s4veclist-p val))
  :rule-classes :rewrite)

Function: svex-s4xeval-memoize-condition

(defun svex-s4xeval-memoize-condition (x)
  (declare (ignorable x)
           (xargs :guard (svex-p x)))
  (eq (svex-kind x) :call))

Theorem: svex-s4xeval-of-svex-fix-x

(defthm svex-s4xeval-of-svex-fix-x
  (equal (svex-s4xeval (svex-fix x))
         (svex-s4xeval x)))

Theorem: svex-call-s4xeval-of-svex-fix-x

(defthm svex-call-s4xeval-of-svex-fix-x
  (equal (svex-call-s4xeval (svex-fix x))
         (svex-call-s4xeval x)))

Theorem: svex-fn/args-s4xeval-of-fnsym-fix-fn

(defthm svex-fn/args-s4xeval-of-fnsym-fix-fn
  (equal (svex-fn/args-s4xeval (fnsym-fix fn)
                               args)
         (svex-fn/args-s4xeval fn args)))

Theorem: svex-fn/args-s4xeval-of-svexlist-fix-args

(defthm svex-fn/args-s4xeval-of-svexlist-fix-args
  (equal (svex-fn/args-s4xeval fn (svexlist-fix args))
         (svex-fn/args-s4xeval fn args)))

Theorem: svexlist-s4xeval-of-svexlist-fix-x

(defthm svexlist-s4xeval-of-svexlist-fix-x
  (equal (svexlist-s4xeval (svexlist-fix x))
         (svexlist-s4xeval x)))

Theorem: svex-s4xeval-svex-equiv-congruence-on-x

(defthm svex-s4xeval-svex-equiv-congruence-on-x
  (implies (svex-equiv x x-equiv)
           (equal (svex-s4xeval x)
                  (svex-s4xeval x-equiv)))
  :rule-classes :congruence)

Theorem: svex-call-s4xeval-svex-equiv-congruence-on-x

(defthm svex-call-s4xeval-svex-equiv-congruence-on-x
  (implies (svex-equiv x x-equiv)
           (equal (svex-call-s4xeval x)
                  (svex-call-s4xeval x-equiv)))
  :rule-classes :congruence)

Theorem: svex-fn/args-s4xeval-fnsym-equiv-congruence-on-fn

(defthm svex-fn/args-s4xeval-fnsym-equiv-congruence-on-fn
  (implies (fnsym-equiv fn fn-equiv)
           (equal (svex-fn/args-s4xeval fn args)
                  (svex-fn/args-s4xeval fn-equiv args)))
  :rule-classes :congruence)

Theorem: svex-fn/args-s4xeval-svexlist-equiv-congruence-on-args

(defthm svex-fn/args-s4xeval-svexlist-equiv-congruence-on-args
  (implies (svexlist-equiv args args-equiv)
           (equal (svex-fn/args-s4xeval fn args)
                  (svex-fn/args-s4xeval fn args-equiv)))
  :rule-classes :congruence)

Theorem: svexlist-s4xeval-svexlist-equiv-congruence-on-x

(defthm svexlist-s4xeval-svexlist-equiv-congruence-on-x
  (implies (svexlist-equiv x x-equiv)
           (equal (svexlist-s4xeval x)
                  (svexlist-s4xeval x-equiv)))
  :rule-classes :congruence)

Theorem: svexlist-s4xeval-nil

(defthm svexlist-s4xeval-nil
  (equal (svexlist-s4xeval nil) nil))

Theorem: car-of-svexlist-s4xeval

(defthm car-of-svexlist-s4xeval
  (s4vec-equiv (car (svexlist-s4xeval x))
               (svex-s4xeval (car x))))

Theorem: cdr-of-svexlist-s4xeval

(defthm cdr-of-svexlist-s4xeval
  (s4veclist-equiv (cdr (svexlist-s4xeval x))
                   (svexlist-s4xeval (cdr x))))

Theorem: len-of-svexlist-s4xeval

(defthm len-of-svexlist-s4xeval
  (equal (len (svexlist-s4xeval x))
         (len x)))

Theorem: svexlist-s4xeval-of-append

(defthm svexlist-s4xeval-of-append
  (equal (svexlist-s4xeval (append a b))
         (append (svexlist-s4xeval a)
                 (svexlist-s4xeval b))))

Theorem: svex-s4xeval-is-svex-xeval

(defthm svex-s4xeval-is-svex-xeval
  (b* ((?val (svex-s4xeval x)))
    (equal (s4vec->4vec val)
           (svex-xeval x))))

Theorem: svex-call-s4xeval-is-svex-call-xeval

(defthm svex-call-s4xeval-is-svex-call-xeval
  (b* ((?val (svex-call-s4xeval x)))
    (equal (s4vec->4vec val)
           (svex-call-xeval x))))

Theorem: svex-fn/args-s4xeval-is-svex-fn/args-xeval

(defthm svex-fn/args-s4xeval-is-svex-fn/args-xeval
  (b* ((?val (svex-fn/args-s4xeval fn args)))
    (equal (s4vec->4vec val)
           (svex-fn/args-xeval fn args))))

Theorem: svexlist-s4xeval-is-svexlist-xeval

(defthm svexlist-s4xeval-is-svexlist-xeval
  (b* ((?val (svexlist-s4xeval x)))
    (equal (s4veclist->4veclist val)
           (svexlist-xeval x))))

Subtopics

Svexlist-s4xeval

Maps svex-s4xeval over an svex list.

Svex-fn/args-s4xeval

Svex-call-s4xeval