		Search-engine friendly clone of the ACL2 documentation.

Port-resolve

Vl-nettype-for-parsed-ansi-port

Determine the net type to use for a port.

Signature
(vl-nettype-for-parsed-ansi-port dir x) → nettype
Arguments: dir — Guard (vl-direction-p dir).; x — Guard (vl-ansi-portdecl-p x).
Returns: nettype — Type (vl-maybe-nettypename-p 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.

"For input and inout ports, the port shall default to a net of the default net type." In VL the default nettype is always wire so this is easy.
"For output ports, the default port kind depends on how the data type is specified.
- If the data type is omitted or declared with the implicit_data_type syntax, the port kind shall default to a net of the default net type.
- If the data type is declared with the explicit datatype syntax, the port shall default to a variable."

Definitions and Theorems

Function: vl-nettype-for-parsed-ansi-port

(defun vl-nettype-for-parsed-ansi-port (dir x)
  (declare (xargs :guard (and (vl-direction-p dir)
                              (vl-ansi-portdecl-p x))))
  (let ((__function__ 'vl-nettype-for-parsed-ansi-port))
    (declare (ignorable __function__))
    (b* (((vl-ansi-portdecl x)))
      (cond (x.nettype x.nettype)
            (x.varp nil)
            ((eq (vl-direction-fix dir) :vl-output)
             (if x.type nil :vl-wire))
            (t :vl-wire)))))

Theorem: vl-maybe-nettypename-p-of-vl-nettype-for-parsed-ansi-port

(defthm vl-maybe-nettypename-p-of-vl-nettype-for-parsed-ansi-port
  (b* ((nettype (vl-nettype-for-parsed-ansi-port dir x)))
    (vl-maybe-nettypename-p nettype))
  :rule-classes :rewrite)

Theorem: vl-nettype-for-parsed-ansi-port-of-vl-direction-fix-dir

(defthm vl-nettype-for-parsed-ansi-port-of-vl-direction-fix-dir
  (equal (vl-nettype-for-parsed-ansi-port (vl-direction-fix dir)
                                          x)
         (vl-nettype-for-parsed-ansi-port dir x)))

Theorem: vl-nettype-for-parsed-ansi-port-vl-direction-equiv-congruence-on-dir

(defthm
 vl-nettype-for-parsed-ansi-port-vl-direction-equiv-congruence-on-dir
 (implies (vl-direction-equiv dir dir-equiv)
          (equal (vl-nettype-for-parsed-ansi-port dir x)
                 (vl-nettype-for-parsed-ansi-port dir-equiv x)))
 :rule-classes :congruence)

Theorem: vl-nettype-for-parsed-ansi-port-of-vl-ansi-portdecl-fix-x

(defthm vl-nettype-for-parsed-ansi-port-of-vl-ansi-portdecl-fix-x
 (equal
      (vl-nettype-for-parsed-ansi-port dir (vl-ansi-portdecl-fix x))
      (vl-nettype-for-parsed-ansi-port dir x)))

Theorem: vl-nettype-for-parsed-ansi-port-vl-ansi-portdecl-equiv-congruence-on-x

(defthm
 vl-nettype-for-parsed-ansi-port-vl-ansi-portdecl-equiv-congruence-on-x
 (implies (vl-ansi-portdecl-equiv x x-equiv)
          (equal (vl-nettype-for-parsed-ansi-port dir x)
                 (vl-nettype-for-parsed-ansi-port dir x-equiv)))
 :rule-classes :congruence)