Strip more from a vl-gateinst for duplicate-detect.
(vl-duplicate-detect-strip-gateinst x) → stripped-x
We could just use vl-gateinst-strip to eliminate attributes and location info, but then gates could still differ by names and delays. It seems like we probably still want to warn about things like
and g1 (o, a, b); and g2 (o, a, b);
Also note that annotate adds names to gate instances anyway, so unnamed gates wouldn't be flagged as duplicates unless we do something more here.
Function:
(defun vl-duplicate-detect-strip-gateinst (x) (declare (xargs :guard (vl-gateinst-p x))) (let ((__function__ 'vl-duplicate-detect-strip-gateinst)) (declare (ignorable __function__)) (change-vl-gateinst (vl-gateinst-strip x) :name nil :delay nil)))
Theorem:
(defthm vl-gateinst-p-of-vl-duplicate-detect-strip-gateinst (b* ((stripped-x (vl-duplicate-detect-strip-gateinst x))) (vl-gateinst-p stripped-x)) :rule-classes :rewrite)