		Search-engine friendly clone of the ACL2 documentation.

Condcheck

Vl-condcheck-fix

Canonicalize an test expression for condcheck.

Signature
(vl-condcheck-fix x) → new-x
Arguments: x — Guard (vl-expr-p x).
Returns: new-x — Type (vl-expr-p new-x).

We fix X (in the normal sense of vl-expr-strip, to throw away widths, attributes, etc., to facilitate equality checking), and then do certain kinds of not-necessarily-sound rewriting to try to further canonicalize things. These rewrites might possibly help us recognize a broader class of errors, but probably aren't super important.

!A     --> ~A               unsound, but sort of valid for one-bit ops

A != B --> ~(A == B)        and we sort the args
A ~^ B --> A == B           unsound, but sort of valid for one-bit ops
A ^ B  --> ~(A == B)        unsound, but sort of valid for one-bit ops

A < B  --> ~(A >= B)
A > B  --> ~(B >= A)
A <= B --> B >= A

We also put arguments of commutative operators into << order. Note that we only apply these rewrites at the top-level and not in any deep way, which also sort of makes sense since we only want to assume that the top-level expression is one-bit wide.

Definitions and Theorems

Function: vl-condcheck-fix

(defun vl-condcheck-fix (x)
 (declare (xargs :guard (vl-expr-p x)))
 (let ((__function__ 'vl-condcheck-fix))
  (declare (ignorable __function__))
  (b* ((x (vl-expr-strip x)))
   (vl-expr-case
    x :vl-unary
    (if (vl-unaryop-equiv x.op :vl-unary-lognot)
        (change-vl-unary x :op :vl-unary-bitnot)
      x)
    :vl-binary
    (b*
     (((mv min max)
       (if (<< x.left x.right)
           (mv x.left x.right)
         (mv x.right x.left)))
      ((when (vl-binaryop-equiv x.op :vl-binary-neq))
       (make-vl-unary :op :vl-unary-bitnot
                      :arg (change-vl-binary x
                                             :op :vl-binary-eq
                                             :left min
                                             :right max)))
      ((when (vl-binaryop-equiv x.op :vl-binary-xnor))
       (change-vl-binary x
                         :op :vl-binary-eq
                         :left min
                         :right max))
      ((when (vl-binaryop-equiv x.op :vl-binary-xor))
       (make-vl-unary :op :vl-unary-bitnot
                      :arg (change-vl-binary x
                                             :op :vl-binary-eq
                                             :left min
                                             :right max)))
      ((when (vl-binaryop-equiv x.op :vl-binary-lt))
       (make-vl-unary :op :vl-unary-bitnot
                      :arg (change-vl-binary x
                                             :op :vl-binary-gte)))
      ((when (vl-binaryop-equiv x.op :vl-binary-gt))
       (make-vl-unary :op :vl-unary-bitnot
                      :arg (change-vl-binary x
                                             :op :vl-binary-gte
                                             :left x.right
                                             :right x.left)))
      ((when (vl-binaryop-equiv x.op :vl-binary-lte))
       (change-vl-binary x
                         :op :vl-binary-gte
                         :left x.right
                         :right x.left))
      ((when
        (member
             x.op
             '(:vl-binary-plus :vl-binary-times
                               :vl-binary-ceq :vl-binary-cne
                               :vl-binary-logand :vl-binary-logor
                               :vl-binary-bitand :vl-binary-bitor)))
       (change-vl-binary x
                         :left min
                         :right max)))
     x)
    :otherwise x))))

Theorem: vl-expr-p-of-vl-condcheck-fix

(defthm vl-expr-p-of-vl-condcheck-fix
  (b* ((new-x (vl-condcheck-fix x)))
    (vl-expr-p new-x))
  :rule-classes :rewrite)

Theorem: vl-condcheck-fix-of-vl-expr-fix-x

(defthm vl-condcheck-fix-of-vl-expr-fix-x
  (equal (vl-condcheck-fix (vl-expr-fix x))
         (vl-condcheck-fix x)))

Theorem: vl-condcheck-fix-vl-expr-equiv-congruence-on-x

(defthm vl-condcheck-fix-vl-expr-equiv-congruence-on-x
  (implies (vl-expr-equiv x x-equiv)
           (equal (vl-condcheck-fix x)
                  (vl-condcheck-fix x-equiv)))
  :rule-classes :congruence)