		Search-engine friendly clone of the ACL2 documentation.

Parse-statements

Vl-parse-task-enable

Parse a task_enable. Verilog-2005 Only.

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

Verilog-2005 Syntax:

task_enable ::=
   hierarchical_task_identifier [ '(' expression { ',' expression } ')' ] ';'

hierarchical_task_identifier ::= hierarchical_identifier

In SystemVerilog-2012 this goes away and is replaced by the subroutine_call_statement case. Per Section 13.3, ``A call to a task is also referred to as a task enable (see Section 13.5 for more details on calling tasks); and Section 13.5 is about subroutine calls and argument passing, and describes the subroutine_call_statement, which has a tf_call production that is very similar to the Verilog-2005 task_enable.

Definitions and Theorems

Function: vl-parse-task-enable-fn

(defun vl-parse-task-enable-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-task-enable))
  (declare (ignorable __function__))
  (seq
   tokstream (loc := (vl-current-loc))
   (hid := (vl-parse-hierarchical-identifier nil))
   (unless
      (vl-is-token? :vl-lparen)
      (:= (vl-match-token :vl-semi))
      (return (make-vl-callstmt :id (make-vl-scopeexpr-end :hid hid)
                                :typearg nil
                                :systemp nil
                                :voidp nil
                                :args nil
                                :atts atts
                                :loc loc)))
   (:= (vl-match))
   (args := (vl-parse-1+-expressions-separated-by-commas))
   (:= (vl-match-token :vl-rparen))
   (:= (vl-match-token :vl-semi))
   (return (make-vl-callstmt :id (make-vl-scopeexpr-end :hid hid)
                             :typearg nil
                             :systemp nil
                             :voidp nil
                             :args args
                             :atts atts
                             :loc loc)))))

Theorem: vl-parse-task-enable-fails-gracefully

(defthm vl-parse-task-enable-fails-gracefully
  (implies (mv-nth 0 (vl-parse-task-enable atts))
           (not (mv-nth 1 (vl-parse-task-enable atts)))))

Theorem: vl-warning-p-of-vl-parse-task-enable

(defthm vl-warning-p-of-vl-parse-task-enable
  (iff (vl-warning-p (mv-nth 0 (vl-parse-task-enable atts)))
       (mv-nth 0 (vl-parse-task-enable atts))))

Theorem: vl-parse-task-enable-result

(defthm vl-parse-task-enable-result
  (implies (and (force (vl-atts-p atts)))
           (equal (vl-stmt-p (mv-nth 1 (vl-parse-task-enable atts)))
                  (not (mv-nth 0 (vl-parse-task-enable atts))))))

Theorem: vl-parse-task-enable-count-strong

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