Heuristic to avoid warning about assigning simple, common right-hand sides to multiple wires.
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
Function:
(defun vl-duperhs-too-trivial-p (rhs) (declare (xargs :guard (vl-expr-p rhs))) (let ((__function__ 'vl-duperhs-too-trivial-p)) (declare (ignorable __function__)) (vl-expr-case rhs :vl-literal t :vl-unary (and (vl-unaryop-equiv rhs.op :vl-unary-bitnot) (vl-expr-case rhs.arg :vl-literal)) :vl-concat (and (tuplep 1 rhs.parts) (let ((arg (first rhs.parts))) (vl-expr-case arg :vl-literal))) :vl-multiconcat (and (vl-expr-resolved-p rhs.reps) (tuplep 1 rhs.parts) (let ((arg (first rhs.parts))) (vl-expr-case arg :vl-literal))) :otherwise nil)))
Theorem:
(defthm booleanp-of-vl-duperhs-too-trivial-p (b* ((trivial-p (vl-duperhs-too-trivial-p rhs))) (booleanp trivial-p)) :rule-classes :type-prescription)
Theorem:
(defthm vl-duperhs-too-trivial-p-of-vl-expr-fix-rhs (equal (vl-duperhs-too-trivial-p (vl-expr-fix rhs)) (vl-duperhs-too-trivial-p rhs)))
Theorem:
(defthm vl-duperhs-too-trivial-p-vl-expr-equiv-congruence-on-rhs (implies (vl-expr-equiv rhs rhs-equiv) (equal (vl-duperhs-too-trivial-p rhs) (vl-duperhs-too-trivial-p rhs-equiv))) :rule-classes :congruence)