		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), given the guard.

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))
    ((when (vl-fast-atom-p x)) x)
    (op (vl-nonatom->op x))
    (args (vl-nonatom->args x))
    ((when (eq op :vl-unary-lognot))
     (change-vl-nonatom x
                        :op :vl-unary-bitnot))
    ((when (eq op :vl-binary-neq))
     (make-vl-nonatom
        :op :vl-unary-bitnot
        :args
        (list (change-vl-nonatom x :op :vl-binary-eq :args
                                 (if (<< (first args) (second args))
                                     args
                                   (rev args))))))
    ((when (eq op :vl-binary-xnor))
     (change-vl-nonatom x :op :vl-binary-eq :args
                        (if (<< (first args) (second args))
                            args
                          (rev args))))
    ((when (eq op :vl-binary-xor))
     (make-vl-nonatom
        :op :vl-unary-bitnot
        :args
        (list (change-vl-nonatom x :op :vl-binary-eq :args
                                 (if (<< (first args) (second args))
                                     args
                                   (rev args))))))
    ((when (eq op :vl-binary-lt))
     (make-vl-nonatom
          :op :vl-unary-bitnot
          :args (list (change-vl-nonatom x
                                         :op :vl-binary-gte))))
    ((when (eq op :vl-binary-gt))
     (make-vl-nonatom
          :op :vl-unary-bitnot
          :args (list (change-vl-nonatom x
                                         :op :vl-binary-gte
                                         :args (rev args)))))
    ((when (eq op :vl-binary-lte))
     (change-vl-nonatom x
                        :op :vl-binary-gte
                        :args (rev args)))
    ((when
        (member
             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-nonatom x :args
                        (if (<< (first args) (second args))
                            args
                          (rev args)))))
   x)))

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

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