Produce a flat vl-emodwirelist-p that contains the E names of every bit that is visible in the original Verilog module.
(esim-vl-designwires mod) is given an E module and returns an vl-emodwirelist-p.
This list should include the E names for every bit that is declared in the
original Verilog module; see VL's designwires transform. It should
not include the new, intermediate wire names that VL generates during
transformations like split and occform. Note that some of the
names in this list might be unused, and hence might not occur in the
Run-time checks ensure that the
(defun esim-vl-designwires (mod) (declare (xargs :guard t)) (b* ((name (gpl :n mod)) (annotations (esim-vl-annotations mod)) (lookup (assoc :design-wires annotations)) ((unless lookup) (if (gpl :x mod) nil (cw "Note: E module ~s0 has no :design-wires annotation!~%" name))) (dwires (cdr lookup)) ((unless (vl-emodwirelist-p dwires)) (er hard? 'esim-vl-designwires "In E module ~s0, :design-wires fails vl-emodwirelist-p check" name))) dwires))
(defthm vl-emodwirelist-p-of-esim-vl-designwires (vl-emodwirelist-p (esim-vl-designwires mod)))