Parse a
(vl-parse-procedural-continuous-assignments atts &key (tokstream 'tokstream) (config 'config)) → (mv errmsg? value new-tokstream)
For Verilog-2005:
procedural_continuous_assignments ::= 'assign' variable_assignment | 'deassign' variable_lvalue | 'force' variable_assignment | 'force' net_assignment | 'release' variable_lvalue | 'release' net_lvalue
SystemVerilog-2012 is identical. Note that a
Function:
(defun vl-parse-procedural-continuous-assignments-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-parse-procedural-continuous-assignments)) (declare (ignorable __function__)) (seq tokstream (when (vl-is-some-token? '(:vl-kwd-assign :vl-kwd-force)) (type := (vl-match)) ((lvalue . expr) := (vl-parse-variable-assignment)) (return (make-vl-assignstmt :type (if (eq (vl-token->type type) :vl-kwd-assign) :vl-assign :vl-force) :lvalue lvalue :rhs (make-vl-rhsexpr :guts expr) :ctrl nil :atts atts :loc (vl-token->loc type)))) (type := (vl-match-some-token '(:vl-kwd-deassign :vl-kwd-release))) (lvalue := (vl-parse-variable-lvalue)) (return (make-vl-deassignstmt :type (if (eq (vl-token->type type) :vl-kwd-deassign) :vl-deassign :vl-release) :lvalue lvalue :atts atts)))))
Theorem:
(defthm vl-parse-procedural-continuous-assignments-fails-gracefully (implies (mv-nth 0 (vl-parse-procedural-continuous-assignments atts)) (not (mv-nth 1 (vl-parse-procedural-continuous-assignments atts)))))
Theorem:
(defthm vl-warning-p-of-vl-parse-procedural-continuous-assignments (iff (vl-warning-p (mv-nth 0 (vl-parse-procedural-continuous-assignments atts))) (mv-nth 0 (vl-parse-procedural-continuous-assignments atts))))
Theorem:
(defthm vl-parse-procedural-continuous-assignments-result (implies (and (force (vl-atts-p atts))) (equal (vl-stmt-p (mv-nth 1 (vl-parse-procedural-continuous-assignments atts))) (not (mv-nth 0 (vl-parse-procedural-continuous-assignments atts))))))
Theorem:
(defthm vl-parse-procedural-continuous-assignments-count-strong (and (<= (vl-tokstream-measure :tokstream (mv-nth 2 (vl-parse-procedural-continuous-assignments atts))) (vl-tokstream-measure)) (implies (not (mv-nth 0 (vl-parse-procedural-continuous-assignments atts))) (< (vl-tokstream-measure :tokstream (mv-nth 2 (vl-parse-procedural-continuous-assignments atts))) (vl-tokstream-measure)))) :rule-classes ((:rewrite) (:linear)))