		Search-engine friendly clone of the ACL2 documentation.

Parse-functions

Vl-parse-function-declaration-2005

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

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

Relevant grammar rules:

function_declaration ::=

     'function' [ 'automatic' ] [ function_range_or_type ]         ; variant 1
       identifier ';'
       function_item_declaration { function_item_declaration }
       statement
     'endfunction'

   | 'function' [ 'automatic' ] [ function_range_or_type ]         ; variant 2
      identifier '(' function_port_list ')' ';'
      { block_item_declaration }
      statement
     'endfunction'

Definitions and Theorems

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

(defun vl-parse-function-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-function-declaration-2005))
  (declare (ignorable __function__))
  (seq
   tokstream
   (function := (vl-match-token :vl-kwd-function))
   (when (vl-is-token? :vl-kwd-automatic)
         (automatic := (vl-match-token :vl-kwd-automatic)))
   (rettype := (vl-parse-optional-function-range-or-type))
   (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))
         (:= (vl-match-token :vl-kwd-endfunction))
         (return-raw
          (b*
           (((mv inputs blockitems)
             (vl-filter-portdecl-or-blockitem-list decls))
            (non-input (vl-portdecllist-find-noninput inputs))
            ((when non-input)
             (vl-parse-error
                  (cat "Functions may only have inputs, but port "
                       (vl-portdecl->name non-input)
                       " has direction "
                       (symbol-name (vl-portdecl->dir non-input)))))
            ((unless (consp inputs))
             (vl-parse-error "Function has no inputs."))
            (ret (vl-make-fundecl-for-parser
                      :name (vl-idtoken->name name)
                      :lifetime (if automatic :vl-automatic nil)
                      :rettype rettype
                      :inputs inputs
                      :decls blockitems
                      :loaditems decls
                      :body stmt
                      :atts atts
                      :loc (vl-token->loc function))))
           (mv nil (list ret) tokstream))))
        (:= (vl-match-token :vl-lparen))
        (inputs := (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))
        (:= (vl-match-token :vl-kwd-endfunction))
        (return-raw
          (b*
           ((non-input (vl-portdecllist-find-noninput inputs))
            ((when non-input)
             (vl-parse-error
                  (cat "Functions may only have inputs, but port "
                       (vl-portdecl->name non-input)
                       " has direction "
                       (symbol-name (vl-portdecl->dir non-input)))))
            (loaditems (append inputs blockitems))
            (ret (vl-make-fundecl-for-parser
                      :name (vl-idtoken->name name)
                      :lifetime (if automatic :vl-automatic nil)
                      :rettype rettype
                      :inputs inputs
                      :decls blockitems
                      :loaditems loaditems
                      :body stmt
                      :atts atts
                      :loc (vl-token->loc function))))
           (mv nil (list ret) tokstream)))))
      ((unless err) (mv nil val tokstream)))
     (seq
      tokstream
      (end := (vl-skip-through-endfunction))
      (return-raw
       (b*
        ((warning
          (make-vl-warning
            :type :vl-parse-error
            :msg
            "~a0: ignoring everything through 'endfunction' 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-function-declaration-2005-fails-gracefully

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

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

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

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

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

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

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

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

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