Obtain the vl-wirealist-p for an E module produced by VL.
(esim-vl-wirealist mod) returns a
This is the "final" wirealist for the module, and typically will include
temporary wires introduced by VL. The wirealist will be
Run-time checks ensure the
(defun esim-vl-wirealist (mod) (declare (xargs :guard t)) (b* ((name (gpl :n mod)) (annotations (esim-vl-annotations mod)) (lookup (assoc :wire-alist annotations)) ((unless lookup) (if (gpl :x mod) nil (cw "Note: E module ~s0 has no :wire-alist annotation!~%" name))) (walist (cdr lookup)) ((unless (vl-wirealist-p walist)) (er hard? 'esim-vl-wirealist "In E module ~s0, :wire-alist fails vl-wirealist-p check" name))) walist))
(defthm vl-wirealist-p-of-esim-vl-wirealist (vl-wirealist-p (esim-vl-wirealist mod)))