Determine the net type to use for a port.
(vl-nettype-for-parsed-ansi-port dir head) → nettype
From SystemVerilog-2012 23.2.2.3, "the term "port kind" is used to mean any of the net type keywords, or the keyword var, which are used to explicitly declare a port of one of these kinds..."
For ports in an ANSI port list, the rules for determining the port kind appear to be the same for the first port and for subsequent ports. (Pages 667 and 668).
The rules depend on the direction of the port.
Function:
(defun vl-nettype-for-parsed-ansi-port (dir head) (declare (xargs :guard (and (vl-direction-p dir) (vl-parsed-portdecl-head-p head)))) (let ((__function__ 'vl-nettype-for-parsed-ansi-port)) (declare (ignorable __function__)) (b* (((vl-parsed-portdecl-head head))) (cond (head.nettype head.nettype) (head.var-p nil) ((eq dir :vl-output) (if head.explicit-p nil :vl-wire)) (t :vl-wire)))))
Theorem:
(defthm vl-maybe-nettypename-p-of-vl-nettype-for-parsed-ansi-port (b* ((nettype (vl-nettype-for-parsed-ansi-port dir head))) (vl-maybe-nettypename-p nettype)) :rule-classes :rewrite)