		Search-engine friendly clone of the ACL2 documentation.

Parse-functions-sv2012

Vl-parse-tf-port-item

Matches tf_port_item, not for prototypes.

Signature
(vl-parse-tf-port-item prev &key (tokstream 'tokstream) (config 'config)) → (mv errmsg? value new-tokstream)
Arguments: config — Guard (vl-loadconfig-p config).

If we ever implement prototypes, this isn't the right function, because we assume that we have names for the items.

These items occur in tf_port_list in a C-style function declaration such as:

function foo (input int a, logic [3:0] b, c); ... endfunction

The tf_port_items here are input int a, logic [3:0] b, and c. We will represent these using vl-portdecls.

Type Determination

The type of each tf_port_item may be explicitly declared or inherited from the previous argument. To support this, we take as input the previously parsed port, if there is a previous port, so that we can infer our type from it, if necessary.

SystemVerilog-2012 gives rules for inferring data types

For tasks arguments in Section 13.3, Page 287, and
For function arguments in Section 13.4, page 291.

In both cases identical language is used:

"If the data type is not explicitly declared, then the default data type is logic if it is the first argument or if the argument direction is explicitly specified. Otherwise the data type is inherited from the previous argument."

Direction Determination

Per 13.3 (Page 287), regarding tasks:

"There is a default direction of input if no direction has been specified. Once a direction is given, subsequent formals default to the same direction."

Grammar rules:

tf_port_item ::= {attribute_instance}
                 [tf_port_direction] ['var'] data_type_or_implicit
                 [ identifier {variable_dimension} [ = expression ] ]

   ((footnote: it shall be illegal to omit the explicit port_identifier
               except within a function_prototype or task_prototype.))

tf_port_direction ::= direction | 'const' 'ref'

Definitions and Theorems

Function: vl-parse-tf-port-item-fn

(defun vl-parse-tf-port-item-fn (prev tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (declare (xargs :guard (or (not prev) (vl-portdecl-p prev))))
 (let ((__function__ 'vl-parse-tf-port-item))
  (declare (ignorable __function__))
  (seq
   tokstream
   (atts := (vl-parse-0+-attribute-instances))
   (dir := (vl-parse-optional-port-direction))
   (when
    (vl-is-token? :vl-kwd-const)
    (return-raw
     (vl-parse-error
      "BOZO need to implement 'const ref' port on tasks/functions.")))
   (when (vl-is-token? :vl-kwd-var)
         (var := (vl-match)))
   ((type . name)
    := (vl-parse-function-data-type-and-name nil))
   (udims := (vl-parse-0+-variable-dimensions))
   (when (vl-is-token? :vl-equalsign)
         (:= (vl-match))
         (default := (vl-parse-expression)))
   (return
    (make-vl-portdecl
     :name (vl-idtoken->name name)
     :loc (vl-token->loc name)
     :dir
     (cond (dir dir)
           (prev (vl-portdecl->dir prev))
           (t :vl-input))
     :type
     (b* (((vl-datatype-or-implicit type)))
      (vl-datatype-update-udims
       udims
       (if
        (or (not type.implicitp)
            var dir (not prev)
            (vl-datatype-case
                 type.type
                 :vl-coretype (or type.type.pdims type.type.signedp)
                 :otherwise nil))
        type.type
        (vl-portdecl->type prev))))
     :default default
     :atts atts
     :nettype nil)))))

Theorem: vl-parse-tf-port-item-fails-gracefully

(defthm vl-parse-tf-port-item-fails-gracefully
  (implies (mv-nth 0 (vl-parse-tf-port-item prev))
           (not (mv-nth 1 (vl-parse-tf-port-item prev)))))

Theorem: vl-warning-p-of-vl-parse-tf-port-item

(defthm vl-warning-p-of-vl-parse-tf-port-item
  (iff (vl-warning-p (mv-nth 0 (vl-parse-tf-port-item prev)))
       (mv-nth 0 (vl-parse-tf-port-item prev))))

Theorem: vl-parse-tf-port-item-result

(defthm vl-parse-tf-port-item-result
 (implies
      (and (force (or (not prev) (vl-portdecl-p prev))))
      (equal (vl-portdecl-p (mv-nth 1 (vl-parse-tf-port-item prev)))
             (not (mv-nth 0 (vl-parse-tf-port-item prev))))))

Theorem: vl-parse-tf-port-item-count-strong

(defthm vl-parse-tf-port-item-count-strong
 (and
    (<= (vl-tokstream-measure
             :tokstream (mv-nth 2 (vl-parse-tf-port-item prev)))
        (vl-tokstream-measure))
    (implies
         (not (mv-nth 0 (vl-parse-tf-port-item prev)))
         (< (vl-tokstream-measure
                 :tokstream (mv-nth 2 (vl-parse-tf-port-item prev)))
            (vl-tokstream-measure))))
 :rule-classes ((:rewrite) (:linear)))