Match a whole
(vl-2012-parse-block-item-declaration-noatts atts &key (tokstream 'tokstream) (config 'config)) → (mv errmsg? value new-tokstream)
SystemVerilog-2012 Grammar:
block_item_declaration ::= {attribute_instance} data_declaration // no semicolon | {attribute_instance} local_parameter_declaration ';' | {attribute_instance} parameter_declaration ';' | {attribute_instance} overload_declaration // no semicolon | {attribute_instance} let_declaration // no semicolon
The data_declaration subsumes the reg, integer, time, real, realtime, and event cases in Verilog-2005.
We don't yet support overload or let declarations, but we have:
overload_declaration ::= 'bind' ... let_declaration ::= 'let' ...
So we can easily identify when these things occur. Moreover we know that a parameter or local parameter declaration always starts with 'parameter' or 'localparam', so we can at least gracefully fail if we encounter anything we don't support.
Function:
(defun vl-2012-parse-block-item-declaration-noatts-fn (atts tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (declare (xargs :guard (vl-atts-p atts))) (let ((__function__ 'vl-2012-parse-block-item-declaration-noatts)) (declare (ignorable __function__)) (seq tokstream (when (vl-is-token? :vl-kwd-bind) (return-raw (vl-parse-error "overload declarations (\"bind ...\") are not yet supported"))) (when (vl-is-some-token? '(:vl-kwd-localparam :vl-kwd-parameter)) (elems := (vl-parse-param-or-localparam-declaration atts '(:vl-kwd-localparam :vl-kwd-parameter))) (:= (vl-match-token :vl-semi)) (return elems)) (when (vl-is-token? :vl-kwd-import) (return-raw (if (vl-plausible-start-of-package-import-p) (vl-parse-package-import-declaration atts) (vl-parse-error "Expected package name after import.")))) (when (vl-is-token? :vl-kwd-typedef) (ans := (vl-parse-type-declaration atts)) (return-raw (if (eq (tag ans) :vl-typedef) (mv nil (list ans) tokstream) (vl-parse-error "Not implemented: forward typedefs as block items.")))) (when (vl-is-token? :vl-kwd-let) (ans := (vl-parse-let-declaration atts)) (return (list ans))) (elems := (vl-parse-main-data-declaration atts)) (return elems))))
Theorem:
(defthm vl-2012-parse-block-item-declaration-noatts-fails-gracefully (implies (mv-nth 0 (vl-2012-parse-block-item-declaration-noatts atts)) (not (mv-nth 1 (vl-2012-parse-block-item-declaration-noatts atts)))))
Theorem:
(defthm vl-warning-p-of-vl-2012-parse-block-item-declaration-noatts (iff (vl-warning-p (mv-nth 0 (vl-2012-parse-block-item-declaration-noatts atts))) (mv-nth 0 (vl-2012-parse-block-item-declaration-noatts atts))))
Theorem:
(defthm vl-2012-parse-block-item-declaration-noatts-result (implies (and (force (vl-atts-p atts))) (vl-blockitemlist-p (mv-nth 1 (vl-2012-parse-block-item-declaration-noatts atts)))))
Theorem:
(defthm vl-2012-parse-block-item-declaration-noatts-true-listp (true-listp (mv-nth 1 (vl-2012-parse-block-item-declaration-noatts atts))) :rule-classes :type-prescription)
Theorem:
(defthm vl-2012-parse-block-item-declaration-noatts-count-strong (and (<= (vl-tokstream-measure :tokstream (mv-nth 2 (vl-2012-parse-block-item-declaration-noatts atts))) (vl-tokstream-measure)) (implies (not (mv-nth 0 (vl-2012-parse-block-item-declaration-noatts atts))) (< (vl-tokstream-measure :tokstream (mv-nth 2 (vl-2012-parse-block-item-declaration-noatts atts))) (vl-tokstream-measure)))) :rule-classes ((:rewrite) (:linear)))