(vl-parse-udp-body head &key (tokstream 'tokstream) (config 'config)) → (mv errmsg? value new-tokstream)
Function:
(defun vl-parse-udp-body-fn (head tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (declare (xargs :guard (vl-udp-head-p head))) (let ((__function__ 'vl-parse-udp-body)) (declare (ignorable __function__)) (seq tokstream (unless (vl-udp-head->sequentialp head) (table := (vl-parse-combinational-body)) (return (make-vl-udp-body :init nil :table table))) (when (vl-is-token? :vl-kwd-initial) (init := (vl-parse-udp-initial-statement (vl-portdecl->name (vl-udp-head->output head))))) (table := (vl-parse-sequential-table)) (return (make-vl-udp-body :init init :table table)))))
Theorem:
(defthm vl-parse-udp-body-fails-gracefully (implies (mv-nth 0 (vl-parse-udp-body head)) (not (mv-nth 1 (vl-parse-udp-body head)))))
Theorem:
(defthm vl-warning-p-of-vl-parse-udp-body (iff (vl-warning-p (mv-nth 0 (vl-parse-udp-body head))) (mv-nth 0 (vl-parse-udp-body head))))
Theorem:
(defthm vl-parse-udp-body-result (implies (and (force (vl-udp-head-p head))) (equal (vl-udp-body-p (mv-nth 1 (vl-parse-udp-body head))) (not (mv-nth 0 (vl-parse-udp-body head))))))
Theorem:
(defthm vl-parse-udp-body-count-strong (and (<= (vl-tokstream-measure :tokstream (mv-nth 2 (vl-parse-udp-body head))) (vl-tokstream-measure)) (implies (not (mv-nth 0 (vl-parse-udp-body head))) (< (vl-tokstream-measure :tokstream (mv-nth 2 (vl-parse-udp-body head))) (vl-tokstream-measure)))) :rule-classes ((:rewrite) (:linear)))