Parse an
(vl-parse-assertion-item &key (tokstream 'tokstream) (config 'config)) → (mv errmsg? value new-tokstream)
SystemVerilog-2012 grammar:
assertion_item ::= concurrent_assertion_item | deferred_immediate_assertion_item deferred_immediate_assertion_item ::= [ block_identifier ':' ] deferred_immediate_assertion_statement concurrent_assertion_item ::= [ block_identifier ':' ] concurrent_assertion_statement | checker_instantiation
Function:
(defun vl-parse-assertion-item-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (declare (xargs :guard (vl-plausible-start-of-assertion-item-p))) (let ((__function__ 'vl-parse-assertion-item)) (declare (ignorable __function__)) (seq tokstream (when (vl-is-token? :vl-idtoken) (blockid := (vl-match)) (:= (vl-match))) (when (vl-parse-assertion-item-looks-concurrent-p) (cassertion := (vl-parse-concurrent-assertion-statement)) (return (list (if blockid (change-vl-cassertion cassertion :name (vl-idtoken->name blockid)) cassertion)))) (assertion := (vl-parse-immediate-assertion-statement)) (unless (vl-assertion->deferral assertion) (return-raw (vl-parse-error "Top level assertion needs a deferral (i.e., '#0' or 'final')."))) (return (list (if blockid (change-vl-assertion assertion :name (vl-idtoken->name blockid)) assertion))))))
Theorem:
(defthm vl-parse-assertion-item-fails-gracefully (implies (mv-nth 0 (vl-parse-assertion-item)) (not (mv-nth 1 (vl-parse-assertion-item)))))
Theorem:
(defthm vl-warning-p-of-vl-parse-assertion-item (iff (vl-warning-p (mv-nth 0 (vl-parse-assertion-item))) (mv-nth 0 (vl-parse-assertion-item))))
Theorem:
(defthm vl-parse-assertion-item-result (implies (and (force (vl-plausible-start-of-assertion-item-p))) (vl-modelementlist-p (mv-nth 1 (vl-parse-assertion-item)))))
Theorem:
(defthm vl-parse-assertion-item-true-listp (true-listp (mv-nth 1 (vl-parse-assertion-item))) :rule-classes :type-prescription)
Theorem:
(defthm vl-parse-assertion-item-count-strong (and (<= (vl-tokstream-measure :tokstream (mv-nth 2 (vl-parse-assertion-item))) (vl-tokstream-measure)) (implies (not (mv-nth 0 (vl-parse-assertion-item))) (< (vl-tokstream-measure :tokstream (mv-nth 2 (vl-parse-assertion-item))) (vl-tokstream-measure)))) :rule-classes ((:rewrite) (:linear)))