Matches
(vl-parse-port-declaration-head-2012 &key (tokstream 'tokstream) (config 'config)) → (mv errmsg? value new-tokstream)
Here is the grammar we are implementing:
net_port_type ::= [net_type] data_type | [net_type] [signing] {packed_dimension} | identifier (*) | 'interconnect' [signing] {packed_dimension} (**) variable_port_type ::= data_type | 'var' data_type | 'var' [signing] {packed_dimension}
We assume that we have already ruled out interface ports.
(*) Since VL doesn't support user-defined net types, we don't implement the
second
(**) We do not yet implement
Function:
(defun vl-parse-port-declaration-head-2012-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-port-declaration-head-2012)) (declare (ignorable __function__)) (seq tokstream (when (vl-is-token? :vl-kwd-interconnect) (return-raw (vl-parse-error "BOZO implement interconnect ports!"))) (when (vl-is-token? :vl-kwd-var) (:= (vl-match)) (when (vl-is-some-token? '(:vl-kwd-signed :vl-kwd-unsigned)) (signing := (vl-match))) (when (vl-is-token? :vl-lbrack) (ranges := (vl-parse-0+-ranges))) (when (or signing ranges) (return (make-vl-parsed-portdecl-head :nettype nil :var-p t :explicit-p nil :implicit-p t :type (make-vl-coretype :name :vl-logic :signedp (and signing (eq (vl-token->type signing) :vl-kwd-signed)) :pdims ranges)))) (when (and (vl-is-token? :vl-idtoken) (not (vl-parsestate-is-user-defined-type-p (vl-idtoken->name (car (vl-tokstream->tokens))) (vl-tokstream->pstate)))) (return (make-vl-parsed-portdecl-head :nettype nil :var-p t :explicit-p nil :implicit-p nil :type (make-vl-coretype :name :vl-logic :signedp nil :pdims nil)))) (type := (vl-parse-datatype)) (return (make-vl-parsed-portdecl-head :nettype nil :var-p t :explicit-p t :implicit-p nil :type type))) (nettype := (vl-parse-optional-nettype)) (when (vl-is-some-token? '(:vl-kwd-signed :vl-kwd-unsigned)) (signing := (vl-match))) (when (vl-is-token? :vl-lbrack) (ranges := (vl-parse-0+-ranges))) (when (or signing ranges) (return (make-vl-parsed-portdecl-head :nettype nettype :var-p nil :explicit-p nil :implicit-p t :type (make-vl-coretype :name :vl-logic :signedp (and signing (eq (vl-token->type signing) :vl-kwd-signed)) :pdims ranges)))) (when (and (vl-is-token? :vl-idtoken) (not (vl-parsestate-is-user-defined-type-p (vl-idtoken->name (car (vl-tokstream->tokens))) (vl-tokstream->pstate)))) (return (make-vl-parsed-portdecl-head :nettype nettype :var-p nil :explicit-p nil :implicit-p nil :type (make-vl-coretype :name :vl-logic :signedp nil :pdims nil)))) (type := (vl-parse-datatype)) (return (make-vl-parsed-portdecl-head :nettype nettype :var-p nil :explicit-p t :implicit-p nil :type type)))))
Theorem:
(defthm vl-parse-port-declaration-head-2012-fails-gracefully (implies (mv-nth 0 (vl-parse-port-declaration-head-2012)) (not (mv-nth 1 (vl-parse-port-declaration-head-2012)))))
Theorem:
(defthm vl-warning-p-of-vl-parse-port-declaration-head-2012 (iff (vl-warning-p (mv-nth 0 (vl-parse-port-declaration-head-2012))) (mv-nth 0 (vl-parse-port-declaration-head-2012))))
Theorem:
(defthm vl-parse-port-declaration-head-2012-result (implies (and t) (equal (vl-parsed-portdecl-head-p (mv-nth 1 (vl-parse-port-declaration-head-2012))) (not (mv-nth 0 (vl-parse-port-declaration-head-2012))))))
Theorem:
(defthm vl-parse-port-declaration-head-2012-count-weak (<= (vl-tokstream-measure :tokstream (mv-nth 2 (vl-parse-port-declaration-head-2012))) (vl-tokstream-measure)) :rule-classes ((:rewrite) (:linear)))