		Search-engine friendly clone of the ACL2 documentation.

Parse-statements

Vl-parse-blocking-or-nonblocking-assignment

Parse a blocking_assignment or nonblocking_assignment.

Signature
(vl-parse-blocking-or-nonblocking-assignment atts &key (tokstream 'tokstream) (config 'config)) → (mv errmsg? value new-tokstream)
Arguments: config — Guard (vl-loadconfig-p config).

Verilog-2005 syntax:

blocking_assignment ::=
  variable_lvalue '=' [delay_or_event_control] expression

nonblocking_assignment ::=
  variable_lvalue '<=' [delay_or_event_control] expression

BOZO SystemVerilog-2012 extends blocking_assignment in several ways which we do not yet implement.

Definitions and Theorems

Function: vl-parse-blocking-or-nonblocking-assignment-fn

(defun vl-parse-blocking-or-nonblocking-assignment-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-blocking-or-nonblocking-assignment))
  (declare (ignorable __function__))
  (seq
   tokstream (loc := (vl-current-loc))
   (lvalue := (vl-parse-variable-lvalue))
   (type := (vl-match-some-token '(:vl-equalsign :vl-lte)))
   (when (vl-is-some-token? '(:vl-pound :vl-atsign :vl-kwd-repeat))
         (delay := (vl-parse-delay-or-event-control)))
   (rhs := (vl-parse-rhs))
   (return
    (make-vl-assignstmt :type
                        (if (eq (vl-token->type type) :vl-equalsign)
                            :vl-blocking
                          :vl-nonblocking)
                        :lvalue lvalue
                        :rhs rhs
                        :ctrl delay
                        :atts atts
                        :loc loc)))))

Theorem: vl-parse-blocking-or-nonblocking-assignment-fails-gracefully

(defthm vl-parse-blocking-or-nonblocking-assignment-fails-gracefully
 (implies
  (mv-nth 0
          (vl-parse-blocking-or-nonblocking-assignment atts))
  (not
      (mv-nth 1
              (vl-parse-blocking-or-nonblocking-assignment atts)))))

Theorem: vl-warning-p-of-vl-parse-blocking-or-nonblocking-assignment

(defthm vl-warning-p-of-vl-parse-blocking-or-nonblocking-assignment
 (iff
   (vl-warning-p
        (mv-nth 0
                (vl-parse-blocking-or-nonblocking-assignment atts)))
   (mv-nth 0
           (vl-parse-blocking-or-nonblocking-assignment atts))))

Theorem: vl-parse-blocking-or-nonblocking-assignment-result

(defthm vl-parse-blocking-or-nonblocking-assignment-result
 (implies
  (and (force (vl-atts-p atts)))
  (equal
   (vl-stmt-p
        (mv-nth 1
                (vl-parse-blocking-or-nonblocking-assignment atts)))
   (not
     (mv-nth 0
             (vl-parse-blocking-or-nonblocking-assignment atts))))))

Theorem: vl-parse-blocking-or-nonblocking-assignment-count-strong

(defthm vl-parse-blocking-or-nonblocking-assignment-count-strong
 (and
  (<=
   (vl-tokstream-measure
        :tokstream
        (mv-nth 2
                (vl-parse-blocking-or-nonblocking-assignment atts)))
   (vl-tokstream-measure))
  (implies
   (not (mv-nth 0
                (vl-parse-blocking-or-nonblocking-assignment atts)))
   (<
    (vl-tokstream-measure
        :tokstream
        (mv-nth 2
                (vl-parse-blocking-or-nonblocking-assignment atts)))
    (vl-tokstream-measure))))
 :rule-classes ((:rewrite) (:linear)))