Match a whole
(vl-2005-parse-block-item-declaration-noatts atts &key (tokstream 'tokstream) (config 'config)) → (mv errmsg? value new-tokstream)
Verilog-2005 Grammar:
block_item_declaration ::= {attribute_instance} 'reg' ['signed'] [range] list_of_block_variable_identifiers ';' | {attribute_instance} 'integer' list_of_block_variable_identifiers ';' | {attribute_instance} 'time' list_of_block_variable_identifiers ';' | {attribute_instance} 'real' list_of_block_variable_identifiers ';' | {attribute_instance} 'realtime' list_of_block_variable_identifiers ';' | {attribute_instance} event_declaration | {attribute_instance} local_parameter_declaration ';' | {attribute_instance} parameter_declaration ';' list_of_block_variable_identifiers ::= block_variable_type { ',' block_variable_type } block_variable_type ::= identifier { dimension }
Of particular note is that the rules for
With this in mind, our approach is to reuse our module-level parsers, but then walk through to ensure that none of the variables have been given initial values.
Function:
(defun vl-2005-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-2005-parse-block-item-declaration-noatts)) (declare (ignorable __function__)) (seq tokstream (type := (mv nil (let ((tokens (vl-tokstream->tokens))) (and (consp tokens) (vl-token->type (car tokens)))) tokstream)) (elements := (case type (:vl-kwd-reg (vl-parse-reg-declaration atts)) (:vl-kwd-integer (vl-parse-integer-declaration atts)) (:vl-kwd-time (vl-parse-time-declaration atts)) (:vl-kwd-real (vl-parse-real-declaration atts)) (:vl-kwd-realtime (vl-parse-realtime-declaration atts)) (:vl-kwd-event (vl-parse-event-declaration atts)) ((:vl-kwd-localparam :vl-kwd-parameter) (seq tokstream (elems := (vl-parse-param-or-localparam-declaration atts '(:vl-kwd-localparam :vl-kwd-parameter))) (:= (vl-match-token :vl-semi)) (return elems))) (t (vl-parse-error "Invalid block item.")))) (return-raw (let ((search (case type ((:vl-kwd-reg :vl-kwd-integer :vl-kwd-time :vl-kwd-real :vl-kwd-realtime) (vl-find-vardecl-with-initval elements)) (t nil)))) (if search (vl-parse-error "Block item declarations are not allowed to have initial values.") (mv nil elements tokstream)))))))
Theorem:
(defthm vl-2005-parse-block-item-declaration-noatts-fails-gracefully (implies (mv-nth 0 (vl-2005-parse-block-item-declaration-noatts atts)) (not (mv-nth 1 (vl-2005-parse-block-item-declaration-noatts atts)))))
Theorem:
(defthm vl-warning-p-of-vl-2005-parse-block-item-declaration-noatts (iff (vl-warning-p (mv-nth 0 (vl-2005-parse-block-item-declaration-noatts atts))) (mv-nth 0 (vl-2005-parse-block-item-declaration-noatts atts))))
Theorem:
(defthm vl-2005-parse-block-item-declaration-noatts-result (implies (and (force (vl-atts-p atts))) (vl-blockitemlist-p (mv-nth 1 (vl-2005-parse-block-item-declaration-noatts atts)))))
Theorem:
(defthm vl-2005-parse-block-item-declaration-noatts-true-listp (true-listp (mv-nth 1 (vl-2005-parse-block-item-declaration-noatts atts))) :rule-classes :type-prescription)
Theorem:
(defthm vl-2005-parse-block-item-declaration-noatts-count-strong (and (<= (vl-tokstream-measure :tokstream (mv-nth 2 (vl-2005-parse-block-item-declaration-noatts atts))) (vl-tokstream-measure)) (implies (not (mv-nth 0 (vl-2005-parse-block-item-declaration-noatts atts))) (< (vl-tokstream-measure :tokstream (mv-nth 2 (vl-2005-parse-block-item-declaration-noatts atts))) (vl-tokstream-measure)))) :rule-classes ((:rewrite) (:linear)))