		Search-engine friendly clone of the ACL2 documentation.

Parse-statements

Vl-parse-procedural-continuous-assignments

Parse a procedural_continuous_assignment.

Signature
(vl-parse-procedural-continuous-assignments atts &key (tokstream 'tokstream) (config 'config)) → (mv errmsg? value new-tokstream)
Arguments: config — Guard (vl-loadconfig-p config).

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 net_assignment is a subset of a variable_assignment, and a net_lvalue is a subset of a variable_lvalue, so we just use the variable versions in each case.

Definitions and Theorems

Function: vl-parse-procedural-continuous-assignments-fn

(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: vl-parse-procedural-continuous-assignments-fails-gracefully

(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: vl-warning-p-of-vl-parse-procedural-continuous-assignments

(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: vl-parse-procedural-continuous-assignments-result

(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: vl-parse-procedural-continuous-assignments-count-strong

(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)))