(vl-parse-net-declaration-finish nettype loc strength rtype type atts &key (tokstream 'tokstream) (config 'config)) → (mv errmsg? value new-tokstream)
Function:
(defun vl-parse-net-declaration-finish-fn (nettype loc strength rtype type atts tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (declare (xargs :guard (and (vl-nettypename-p nettype) (vl-location-p loc) (or (not strength) (vl-gatestrength-p strength) (vl-cstrength-p strength)) (or (not rtype) (vl-token-p rtype)) (vl-datatype-p type) (vl-atts-p atts)))) (let ((__function__ 'vl-parse-net-declaration-finish)) (declare (ignorable __function__)) (seq tokstream (when (vl-is-token? :vl-pound) (delay := (vl-parse-delay3))) (declassigns := (vl-parse-1+-variable-decl-assignments-separated-by-commas)) (:= (vl-match-token :vl-semi)) (return-raw (b* ((vectoredp (vl-is-token-of-type-p rtype :vl-kwd-vectored)) (scalaredp (vl-is-token-of-type-p rtype :vl-kwd-scalared)) (gstrength (vl-disabled-gstrength strength)) (cstrength (vl-disabled-cstrength strength)) (errorstr (vl-netdecls-error nettype cstrength gstrength vectoredp scalaredp type delay declassigns)) ((when errorstr) (vl-parse-error errorstr)) ((mv decls assigns) (vl-build-netdecls loc declassigns nettype type atts vectoredp scalaredp delay cstrength gstrength))) (mv nil (cons assigns decls) tokstream))))))
Theorem:
(defthm vl-parse-net-declaration-finish-fails-gracefully (implies (mv-nth 0 (vl-parse-net-declaration-finish nettype loc strength rtype type atts)) (not (mv-nth 1 (vl-parse-net-declaration-finish nettype loc strength rtype type atts)))))
Theorem:
(defthm vl-warning-p-of-vl-parse-net-declaration-finish (iff (vl-warning-p (mv-nth 0 (vl-parse-net-declaration-finish nettype loc strength rtype type atts))) (mv-nth 0 (vl-parse-net-declaration-finish nettype loc strength rtype type atts))))
Theorem:
(defthm vl-parse-net-declaration-finish-result (implies (and (not (mv-nth 0 (vl-parse-net-declaration-finish nettype loc strength rtype type atts))) (and (and (force (vl-nettypename-p nettype)) (force (vl-location-p loc)) (force (or (not strength) (vl-gatestrength-p strength) (vl-cstrength-p strength))) (force (or (not rtype) (vl-token-p rtype))) (force (vl-datatype-p type)) (force (vl-atts-p atts))))) (and (consp (mv-nth 1 (vl-parse-net-declaration-finish nettype loc strength rtype type atts))) (vl-assignlist-p (car (mv-nth 1 (vl-parse-net-declaration-finish nettype loc strength rtype type atts)))) (vl-vardecllist-p (cdr (mv-nth 1 (vl-parse-net-declaration-finish nettype loc strength rtype type atts)))))))
Theorem:
(defthm vl-parse-net-declaration-finish-count-strong (and (<= (vl-tokstream-measure :tokstream (mv-nth 2 (vl-parse-net-declaration-finish nettype loc strength rtype type atts))) (vl-tokstream-measure)) (implies (not (mv-nth 0 (vl-parse-net-declaration-finish nettype loc strength rtype type atts))) (< (vl-tokstream-measure :tokstream (mv-nth 2 (vl-parse-net-declaration-finish nettype loc strength rtype type atts))) (vl-tokstream-measure)))) :rule-classes ((:rewrite) (:linear)))