• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
        • Warnings
        • Primitives
        • Use-set
        • Syntax
          • Vl-module
          • Vl-vardecl
          • Expressions
          • Vl-fundecl
          • Vl-assign
          • Vl-gateinst
          • Vl-modinst
          • Vl-commentmap
          • Vl-portdecl
            • Vl-portdecl-p
            • Vl-portdecl-fix
            • Vl-portdecl-equiv
            • Make-vl-portdecl
            • Change-vl-portdecl
            • Vl-portdecl->nettype
            • Vl-portdecl->name
            • Vl-portdecl->type
            • Vl-portdecl->loc
            • Vl-portdecl->dir
            • Vl-portdecl->atts
          • Vl-taskdecl
          • Vl-design
          • Vl-interface
          • Vl-plainarglist->exprs
          • Vl-taskdecllist->names
          • Vl-fundecllist->names
          • Vl-package
          • Vl-port
          • Vl-udp
          • Vl-paramdecl
          • Vl-genelement
          • Vl-cycledelayrange
          • Vl-namedarg
          • Vl-sort-blockitems-aux
          • Vl-distitem
          • Vl-gatedelay
          • Vl-repetition
          • Vl-typedef
          • Vl-range
          • Vl-gatestrength
          • Vl-program
          • Vl-config
          • Vl-always
          • Vl-datatype-update-dims
          • Vl-import
          • Vl-enumbasetype
          • Vl-repeateventcontrol
          • Vl-paramargs
          • Vl-initial
          • Vl-eventcontrol
          • Vl-udpsymbol-p
          • Vl-maybe-range
          • Vl-maybe-nettypename
          • Vl-maybe-gatestrength
          • Vl-maybe-gatedelay
          • Vl-maybe-delayoreventcontrol
          • Vl-alias
          • Maybe-string-fix
          • Vl-maybe-packeddimension
          • Vl-fwdtypedef
          • Vl-evatom
          • Vl-packeddimension-p
          • Vl-maybe-udpsymbol
          • Vl-maybe-module
          • Vl-maybe-direction
          • Vl-maybe-datatype
          • Vl-maybe-cstrength
          • Vl-direction-p
          • Vl-arguments
          • Vl-maybe-design
          • Vl-udpline
          • Vl-exprdist
          • Vl-context1
          • Vl-genvar
          • Vl-enumitem
          • Vl-datatype-update-udims
          • Vl-datatype-update-pdims
          • Vl-modelement
          • Vl-udpedge
          • Vl-delaycontrol
          • Vl-context
          • Vl-sort-blockitems
          • Vl-distweighttype-p
          • Vl-ctxelement->loc
          • Vl-blockitem
          • Vl-vardecllist
          • Vl-module->ifports
          • Vl-modelement->loc
          • Vl-ctxelement
          • Vl-coretypename-p
          • Vl-packeddimensionlist
          • Vl-modelementlist->genelements
          • Vl-gatetype-p
          • Vl-paramdecllist
          • Vl-lifetime-p
          • Vl-datatype->udims
          • Vl-datatype->pdims
          • Vl-timeunit-p
          • Vl-repetitiontype-p
          • Vl-port->name
          • Vl-importlist
          • Vl-genelement->loc
          • Vl-delayoreventcontrol
          • Vl-cstrength-p
          • Statements
          • Vl-udpentry-p
          • Vl-packeddimension-fix
          • Vl-nettypename-p
          • Vl-portdecllist
          • Vl-port->loc
          • Vl-enumbasekind-fix
          • Vl-arguments->args
          • Vl-taskdecllist
          • Vl-portlist
          • Vl-importpart-p
          • Vl-importpart-fix
          • Vl-fundecllist
          • Vl-blockstmt-p
          • Vl-assignlist
          • Vl-alwaystype-p
          • Vl-typedeflist
          • Vl-syntaxversion-p
          • Vl-randomqualifier-p
          • Vl-modinstlist
          • Vl-gateinstlist
          • Vl-blockitemlist
          • Vl-udptable
          • Vl-udplist
          • Vl-udpentrylist
          • Vl-programlist
          • Vl-paramvaluelist
          • Vl-packagelist
          • Vl-namedparamvaluelist
          • Vl-namedarglist
          • Vl-modulelist
          • Vl-modportlist
          • Vl-modport-portlist
          • Vl-interfacelist
          • Vl-initiallist
          • Vl-genvarlist
          • Vl-fwdtypedeflist
          • Vl-evatomlist
          • Vl-enumitemlist
          • Vl-distlist
          • Vl-configlist
          • Vl-alwayslist
          • Vl-aliaslist
          • Vl-regularportlist
          • Vl-rangelist-list
          • Vl-rangelist
          • Vl-paramdecllist-list
          • Vl-modelementlist
          • Vl-maybe-range-list
          • Vl-interfaceportlist
          • Vl-argumentlist
          • Data-types
        • Getting-started
        • Utilities
        • Loader
        • Transforms
        • Lint
        • Mlib
        • Server
        • Kit
        • Printer
        • Esim-vl
        • Well-formedness
      • Sv
      • Fgl
      • Vwsim
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Syntax

Vl-portdecl

Representation of Verilog port declarations.

This is a product type introduced by defprod.

Fields
name — stringp
An ordinary string that should agree with some identifier used in the "internal" wiring expressions from some port(s) in the module.
dir — vl-direction-p
Says whether this port is an input, output, or bidirectional (inout) port.
nettype — vl-maybe-nettypename
type — vl-datatype
The type and size information for this port. Warning: per Verilog-2005 page 175, port declarations and net/reg declarations must be checked against one another: if either declaration includes the signed keyword, then both are to be considered signed. The loader DOES NOT do this cross-referencing automatically; instead the portdecl-sign transformation needs to be run. See also vl-portdecl-and-moduleitem-compatible-p which is part of our notion of reasonable modules.
atts — vl-atts
Any attributes associated with this declaration.
loc — vl-location
Where the port was declared in the source code.

See vl-port for related background. Port declarations, described in Section 12.3.3 of the Verilog-2005 standard, ascribe certain properties (direction, signedness, size, and so on) to the ports of a module. Here is an example:

module m(a, b) ;
  input [3:0] a ;  // <--- port declaration
  ...
endmodule

Although Verilog allows multiple ports to be declared simultaneously, i.e., input w1, w2;, our parser splits these merged declarations to create separate vl-portdecl-p objects for each port. Because of this, every vl-portdecl-p has only a single name.

Most of the time, e.g., for a in module m above, the resulting vl-module will have:

  • A vl-port for a,
  • A corresponding vl-portdecl that has the direction/type information, and
  • A corresponding vl-vardecl that looks like an ordinary variable.

The exceptions to this are:

  • Interface ports have no corresponding port/vardecl.
  • The ports/portdecls do not necessarily line up when complex ports are used, see vl-port for details.

Subtopics

Vl-portdecl-p
Recognizer for vl-portdecl structures.
Vl-portdecl-fix
Fixing function for vl-portdecl structures.
Vl-portdecl-equiv
Basic equivalence relation for vl-portdecl structures.
Make-vl-portdecl
Basic constructor macro for vl-portdecl structures.
Change-vl-portdecl
Modifying constructor for vl-portdecl structures.
Vl-portdecl->nettype
Get the nettype field from a vl-portdecl.
Vl-portdecl->name
Get the name field from a vl-portdecl.
Vl-portdecl->type
Get the type field from a vl-portdecl.
Vl-portdecl->loc
Get the loc field from a vl-portdecl.
Vl-portdecl->dir
Get the dir field from a vl-portdecl.
Vl-portdecl->atts
Get the atts field from a vl-portdecl.