• 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-alist-xeval
            • 4vec-xfree-p
            • Svexlist-xeval
            • Svex-fn/args-xeval
            • Svex-call-xeval
          • Svex-mono-eval
          • Svex-eval
          • Svex-apply
          • Svex-env
          • Svex-alist-eval
          • Svar-boolmasks-lookup
          • Svex-s4eval
          • 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

• Evaluation

Svex-xeval

Cheaply detect always-constant bits in an svex by approximately evaluating it under the empty (i.e., all X) environment.

Signature

(svex-xeval x) → val

Arguments

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

Returns

val — Type (4vec-p val).

This is a lightweight way to tell that certain bits of an svex expression are actually particular constants, no matter how you bind its variables. It returns an 4vec which tells us that certain bits of expr are ``obviously'' constant, and that other bits are not known to be constant. In particular:

• Xes indicate that this bit of expr is not obviously constant,
• 0/1/Z bits indicate that this bit of expr is obviously always 0/1/Z.

Example

Consider the following expression:

(bitand (bitor a b) (bitand c #b1000))

What values can this expression return? You can see that, regardless of the values of a, b, and c, the resulting 4vec will always have 0 on its lower 3 bits. It will also always have 0s on bits 5 and above. But bit 4 will depend on the values of a, b, and c.

When we use svex-xeval, we get:

(svex-xeval '(bitand (bitor a b) (bitand c #b1000))) == (8 . 0)

Here is the interpretation of the resulting 4vec, (8 . 0):

bits of upper (8) are: 0...01000
bits of lower (0) are: 0...00000
---------------------------------
01ZX interpretation:   0...0X000

So svex-xeval is telling us that:

• Bit 4 is not known to be always constant.
• All the other bits are known to be always constant 0.

Implementation

(svex-xeval expr) is almost identical to (svex-eval expr nil). Recall that, when svex-eval encounters a variable that isn't bound in the environment, it returns the all Xes vector. So, when we evaluate expr in the nil environment, it's as if we've bound all of its variables to all Xes.

If all of our expressions were ``properly monotonic'' and truly treated x bits as unknowns, then the result of (svex-eval expr nil) would clearly be a conservative approximation of (svex-eval expr env) for any environment.

This almost works. However, the case-equality operator === is problematic, because it has a non-monotonic semantics that does not treat X bits as unknown. As a result, evaluation in the nil environment doesn't really work for what we're trying to do here. For example:

(svex-eval '(=== a b) nil)     -->  -1  (all bits true)

But obviously this expression isn't always true, for instance:

(let ((env '((a . 1) (b . 0))))
  (svex-eval '(=== a b) env))    -->  0  (all bits false)

To correct for this, svex-xeval simply interprets === as == instead. Since == is an ordinary, properly monotonic function, and since it conservatively approximates ===, this works out quite well and we get, for instance:

(svex-xeval '(=== a b))  --> all Xes
(svex-xeval '(=== a a))  --> all Xes
(svex-xeval '(=== 0 0))  --> all true

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

(defthm return-type-of-svex-xeval.val
  (b* ((?val (svex-xeval x)))
    (4vec-p val))
  :rule-classes :rewrite)

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

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

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

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

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

(defthm return-type-of-svexlist-xeval.val
  (b* ((?val (svexlist-xeval x)))
    (4veclist-p val))
  :rule-classes :rewrite)

Theorem: svex-xeval-of-quote

(defthm svex-xeval-of-quote
  (implies (svex-case x :quote)
           (equal (svex-xeval x)
                  (svex-quote->val x))))

Theorem: svex-xeval-of-svex-fix-x

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

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

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

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

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

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

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

Theorem: svexlist-xeval-of-svexlist-fix-x

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

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

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

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

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

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

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

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

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

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

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

Theorem: svexlist-xeval-nil

(defthm svexlist-xeval-nil
  (equal (svexlist-xeval nil) nil))

Theorem: car-of-svexlist-xeval

(defthm car-of-svexlist-xeval
  (4vec-equiv (car (svexlist-xeval x))
              (svex-xeval (car x))))

Theorem: cdr-of-svexlist-xeval

(defthm cdr-of-svexlist-xeval
  (4veclist-equiv (cdr (svexlist-xeval x))
                  (svexlist-xeval (cdr x))))

Theorem: len-of-svexlist-xeval

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

Theorem: svexlist-xeval-of-append

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

Subtopics

Svex-alist-xeval

Maps svex-xeval over an svex alist.

4vec-xfree-p

Recognizer for 4vecs with no X bits. These have a special relationship with svex-xeval.

Svexlist-xeval

Maps svex-xeval over an svex list.

Svex-fn/args-xeval

Svex-call-xeval