		Search-engine friendly clone of the ACL2 documentation.

Parse-functions

Vl-parse-task-declaration-2005

Verilog-2005 only. Matches task_declaration except for the attributes.

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

Relevant grammar rules:

task_declaration ::=

   'task' [ 'automatic' ] identifier ';'         ;; variant 1
      { task_item_declaration }
      statement_or_null
   'endtask'

 | 'task' [ 'automatic' ] identifier '(' [task_port_list] ')' ';'
      { block_item_declaration }
      statement_or_null
   'endtask'

Definitions and Theorems

Function: vl-parse-task-declaration-2005-fn

(defun vl-parse-task-declaration-2005-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-declaration-2005))
  (declare (ignorable __function__))
  (seq
   tokstream
   (task := (vl-match-token :vl-kwd-task))
   (when (vl-is-token? :vl-kwd-automatic)
         (automatic := (vl-match-token :vl-kwd-automatic)))
   (name := (vl-match-token :vl-idtoken))
   (return-raw
    (b*
     (((mv err val tokstream)
       (seq
        tokstream
        (when
         (vl-is-token? :vl-semi)
         (:= (vl-match-token :vl-semi))
         (decls := (vl-parse-0+-task-item-declarations))
         (stmt := (vl-parse-statement-or-null))
         (:= (vl-match-token :vl-kwd-endtask))
         (return
           (b* (((mv ports blockitems)
                 (vl-filter-portdecl-or-blockitem-list decls))
                (ans (vl-make-taskdecl-for-parser
                          :name (vl-idtoken->name name)
                          :lifetime (if automatic :vl-automatic nil)
                          :ports ports
                          :decls blockitems
                          :loaditems decls
                          :body stmt
                          :atts atts
                          :loc (vl-token->loc task))))
             (list ans))))
        (:= (vl-match-token :vl-lparen))
        (unless (vl-is-token? :vl-rparen)
                (ports := (vl-parse-taskport-list)))
        (:= (vl-match-token :vl-rparen))
        (:= (vl-match-token :vl-semi))
        (blockitems := (vl-parse-0+-block-item-declarations))
        (stmt := (vl-parse-statement-or-null))
        (:= (vl-match-token :vl-kwd-endtask))
        (return
             (list (vl-make-taskdecl-for-parser
                        :name (vl-idtoken->name name)
                        :lifetime (if automatic :vl-automatic nil)
                        :ports ports
                        :decls blockitems
                        :loaditems (append ports blockitems)
                        :body stmt
                        :atts atts
                        :loc (vl-token->loc task))))))
      ((unless err) (mv nil val tokstream)))
     (seq
      tokstream
      (end := (vl-skip-through-endtask))
      (return-raw
       (b*
        ((warning
          (make-vl-warning
           :type :vl-parse-error
           :msg "~a0: ignoring everything through 'endtask' at ~a1."
           :args (list (vl-idtoken->name name)
                       (vl-token->loc end))
           :fatalp t
           :fn __function__))
         (tokstream (vl-tokstream-add-warning err))
         (tokstream (vl-tokstream-add-warning warning)))
        (mv nil nil tokstream)))))))))

Theorem: vl-parse-task-declaration-2005-fails-gracefully

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

Theorem: vl-warning-p-of-vl-parse-task-declaration-2005

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

Theorem: vl-parse-task-declaration-2005-result

(defthm vl-parse-task-declaration-2005-result
  (implies (and (force (vl-atts-p atts)))
           (vl-taskdecllist-p
                (mv-nth 1
                        (vl-parse-task-declaration-2005 atts)))))

Theorem: vl-parse-task-declaration-2005-true-listp

(defthm vl-parse-task-declaration-2005-true-listp
  (true-listp (mv-nth 1
                      (vl-parse-task-declaration-2005 atts)))
  :rule-classes :type-prescription)

Theorem: vl-parse-task-declaration-2005-count-strong

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