Matches
(vl-parse-ansi-port-header &key (tokstream 'tokstream) (config 'config)) → (mv errmsg? value new-tokstream)
See especially the discussion of "ruling out interfaces" in parse-port-types.
Function:
(defun vl-parse-ansi-port-header-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-ansi-port-header)) (declare (ignorable __function__)) (seq tokstream (when (vl-is-token? :vl-kwd-interface) (return-raw (vl-parse-error "BOZO implement explicit 'interface' ports."))) (when (and (vl-is-token? :vl-idtoken) (vl-lookahead-is-token? :vl-dot (cdr (vl-tokstream->tokens))) (vl-lookahead-is-token? :vl-idtoken (cddr (vl-tokstream->tokens)))) (iface := (vl-match)) (:= (vl-match)) (modport := (vl-match)) (return (make-vl-parsed-interface-head :ifname (vl-idtoken->name iface) :modport (vl-idtoken->name modport)))) (when (and (vl-is-token? :vl-idtoken) (vl-lookahead-is-token? :vl-idtoken (cdr (vl-tokstream->tokens))) (not (vl-parsestate-is-user-defined-type-p (vl-idtoken->name (car (vl-tokstream->tokens))) (vl-tokstream->pstate)))) (iface := (vl-match)) (return (make-vl-parsed-interface-head :ifname (vl-idtoken->name iface) :modport nil))) (ans := (vl-parse-port-declaration-head-2012)) (return ans))))
Theorem:
(defthm vl-parse-ansi-port-header-fails-gracefully (implies (mv-nth 0 (vl-parse-ansi-port-header)) (not (mv-nth 1 (vl-parse-ansi-port-header)))))
Theorem:
(defthm vl-warning-p-of-vl-parse-ansi-port-header (iff (vl-warning-p (mv-nth 0 (vl-parse-ansi-port-header))) (mv-nth 0 (vl-parse-ansi-port-header))))
Theorem:
(defthm vl-parse-ansi-port-header-result (implies (and t) (equal (vl-parsed-ansi-head-p (mv-nth 1 (vl-parse-ansi-port-header))) (not (mv-nth 0 (vl-parse-ansi-port-header))))))
Theorem:
(defthm vl-parse-ansi-port-header-count-weak (<= (vl-tokstream-measure :tokstream (mv-nth 2 (vl-parse-ansi-port-header))) (vl-tokstream-measure)) :rule-classes ((:rewrite) (:linear)))