		Search-engine friendly clone of the ACL2 documentation.

Duperhs-check

Vl-duperhs-too-trivial-p

Heuristic to avoid warning about assigning simple, common right-hand sides to multiple wires.

Signature
(vl-duperhs-too-trivial-p rhs) → trivial-p
Arguments: rhs — The rhs shared by some list of assignments.
Guard (vl-expr-p rhs).
Returns: trivial-p — Is this too trivial to warn about?.
Type (booleanp trivial-p).

It seems fine to assign a constant, weirdint, real, or string to multiple wires; this is especially frequent for things like 0 and 1, so we don't want to warn in these cases.

We'll just suppress warnings for any atoms other than identifiers. This will allow us to still flag situations like:

assign wire1 = wirefoo;
assign wire2 = wirefoo;

I later decided I wanted to extend this, and additionally not cause warnings for odd but innocuous things like ~ 1'b0 and {1'b0}.

Definitions and Theorems

Function: vl-duperhs-too-trivial-p

(defun vl-duperhs-too-trivial-p (rhs)
  (declare (xargs :guard (vl-expr-p rhs)))
  (let ((__function__ 'vl-duperhs-too-trivial-p))
    (declare (ignorable __function__))
    (b* (((when (vl-fast-atom-p rhs))
          (not (vl-fast-id-p (vl-atom->guts rhs))))
         ((vl-nonatom rhs) rhs))
      (and (or (eq rhs.op :vl-unary-bitnot)
               (eq rhs.op :vl-concat))
           (tuplep 1 rhs.args)
           (vl-fast-atom-p (first rhs.args))
           (not (vl-fast-id-p (vl-atom->guts (first rhs.args))))))))

Theorem: booleanp-of-vl-duperhs-too-trivial-p

(defthm booleanp-of-vl-duperhs-too-trivial-p
  (b* ((trivial-p (vl-duperhs-too-trivial-p rhs)))
    (booleanp trivial-p))
  :rule-classes :type-prescription)