Matches
(vl-parse-tf-port-item prev &key (tokstream 'tokstream) (config 'config)) → (mv errmsg? value new-tokstream)
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
function foo (input int a, logic [3:0] b, c); ... endfunction
The
The type of each
SystemVerilog-2012 gives rules for inferring data types
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."
Per 13.3 (Page 287), regarding tasks:
"There is a default direction ofinput if no direction has been specified. Once a direction is given, subsequent formals default to the same direction."
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'
Function:
(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:
(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:
(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:
(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:
(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)))