Verilog-2005 Only. Matches port_declaration in ansi-style port lists.
(vl-parse-port-declaration-atts-2005 &key (tokstream 'tokstream) (config 'config)) → (mv errmsg? value new-tokstream)
We force these to be complete declarations because, per Verilog-2005 Section 12.3.4, in this syntax "Each declared port provides the complete information about the port...", which strongly suggests (when paired with the description of "completely declared" ports on Page 174) that it should not be declared again.
Function:
(defun vl-parse-port-declaration-atts-2005-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-port-declaration-atts-2005)) (declare (ignorable __function__)) (seq tokstream (atts := (vl-parse-0+-attribute-instances)) (result := (vl-parse-port-declaration-noatts-2005 atts t)) (return result))))
Theorem:
(defthm vl-parse-port-declaration-atts-2005-fails-gracefully (implies (mv-nth 0 (vl-parse-port-declaration-atts-2005)) (not (mv-nth 1 (vl-parse-port-declaration-atts-2005)))))
Theorem:
(defthm vl-warning-p-of-vl-parse-port-declaration-atts-2005 (iff (vl-warning-p (mv-nth 0 (vl-parse-port-declaration-atts-2005))) (mv-nth 0 (vl-parse-port-declaration-atts-2005))))
Theorem:
(defthm vl-parse-port-declaration-atts-2005-result (implies (and t) (equal (consp (mv-nth 1 (vl-parse-port-declaration-atts-2005))) (not (mv-nth 0 (vl-parse-port-declaration-atts-2005))))))
Theorem:
(defthm vl-parse-port-declaration-atts-2005-count-strong (and (<= (vl-tokstream-measure :tokstream (mv-nth 2 (vl-parse-port-declaration-atts-2005))) (vl-tokstream-measure)) (implies (not (mv-nth 0 (vl-parse-port-declaration-atts-2005))) (< (vl-tokstream-measure :tokstream (mv-nth 2 (vl-parse-port-declaration-atts-2005))) (vl-tokstream-measure)))) :rule-classes ((:rewrite) (:linear)))
Theorem:
(defthm true-listp-of-vl-parse-port-declaration-atts-2005-1 (true-listp (car (mv-nth 1 (vl-parse-port-declaration-atts-2005)))) :rule-classes :type-prescription)
Theorem:
(defthm true-listp-of-vl-parse-port-declaration-atts-2005-2 (true-listp (cdr (mv-nth 1 (vl-parse-port-declaration-atts-2005)))) :rule-classes :type-prescription)
Theorem:
(defthm vl-parse-port-declaration-atts-2005-basics (and (vl-portdecllist-p (car (mv-nth 1 (vl-parse-port-declaration-atts-2005)))) (vl-vardecllist-p (cdr (mv-nth 1 (vl-parse-port-declaration-atts-2005))))))