Parse a
(vl-parse-case-keyword &key (tokstream 'tokstream) (config 'config)) → (mv errmsg? value new-tokstream)
The rule from SystemVerilog-2012 is:
case_keyword ::= 'case' | 'casez' | 'casex'
This is also useful in Verilog-2005, but isn't a named rule in the Verilog-2005 grammar.
Function:
(defun vl-parse-case-keyword-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-case-keyword)) (declare (ignorable __function__)) (seq tokstream (type := (vl-match-some-token '(:vl-kwd-case :vl-kwd-casez :vl-kwd-casex))) (return (cons (case (vl-token->type type) (:vl-kwd-case nil) (:vl-kwd-casez :vl-casez) (:vl-kwd-casex :vl-casex)) (vl-token->loc type))))))
Theorem:
(defthm vl-parse-case-keyword-fails-gracefully (implies (mv-nth 0 (vl-parse-case-keyword)) (not (mv-nth 1 (vl-parse-case-keyword)))))
Theorem:
(defthm vl-warning-p-of-vl-parse-case-keyword (iff (vl-warning-p (mv-nth 0 (vl-parse-case-keyword))) (mv-nth 0 (vl-parse-case-keyword))))
Theorem:
(defthm vl-parse-case-keyword-result (implies (and (not (mv-nth 0 (vl-parse-case-keyword))) (and t)) (and (consp (mv-nth 1 (vl-parse-case-keyword))) (vl-casetype-p (car (mv-nth 1 (vl-parse-case-keyword)))) (vl-location-p (cdr (mv-nth 1 (vl-parse-case-keyword)))))))
Theorem:
(defthm vl-parse-case-keyword-count-strong (and (<= (vl-tokstream-measure :tokstream (mv-nth 2 (vl-parse-case-keyword))) (vl-tokstream-measure)) (implies (not (mv-nth 0 (vl-parse-case-keyword))) (< (vl-tokstream-measure :tokstream (mv-nth 2 (vl-parse-case-keyword))) (vl-tokstream-measure)))) :rule-classes ((:rewrite) (:linear)))