		Search-engine friendly clone of the ACL2 documentation.

Parse-statements

Vl-parse-system-tf-call

Parse a system_tf_call. SystemVerilog-2012 only.

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

Original grammar rules:

system_tf_call ::= system_tf_identifier [ '(' list_of_arguments ')' ]
                 | system_tf_identifier [ '(' data_type [ ',' expression ] ')'

system_tf_identifier ::= $[a-zA-Z0-9_$]{[a-zA-Z0-9_$]}

Definitions and Theorems

Function: vl-parse-system-tf-call-fn

(defun vl-parse-system-tf-call-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (declare (xargs :guard (vl-is-token? :vl-sysidtoken)))
 (let ((__function__ 'vl-parse-system-tf-call))
  (declare (ignorable __function__))
  (seq
   tokstream
   (fn := (vl-match-token :vl-sysidtoken))
   (when (vl-is-token? :vl-lparen)
         (:= (vl-match))
         (unless (vl-is-token? :vl-rparen)
                 (arg1 := (vl-parse-expression-without-failure))
                 (when (not arg1)
                       (typearg := (vl-parse-simple-type)))
                 (when (vl-is-token? :vl-comma)
                       (:= (vl-match))
                       (args := (vl-parse-sysfuncall-args))))
         (:= (vl-match-token :vl-rparen)))
   (return (let* ((fname (vl-sysidtoken->name fn))
                  (id (make-vl-scopeexpr-end
                           :hid (make-vl-hidexpr-end :name fname))))
             (make-vl-callstmt :id id
                               :systemp t
                               :typearg typearg
                               :args (if arg1 (cons arg1 args) args)
                               :voidp nil
                               :atts nil
                               :loc (vl-token->loc fn)))))))

Theorem: vl-parse-system-tf-call-fails-gracefully

(defthm vl-parse-system-tf-call-fails-gracefully
  (implies (mv-nth 0 (vl-parse-system-tf-call))
           (not (mv-nth 1 (vl-parse-system-tf-call)))))

Theorem: vl-warning-p-of-vl-parse-system-tf-call

(defthm vl-warning-p-of-vl-parse-system-tf-call
  (iff (vl-warning-p (mv-nth 0 (vl-parse-system-tf-call)))
       (mv-nth 0 (vl-parse-system-tf-call))))

Theorem: vl-parse-system-tf-call-result

(defthm vl-parse-system-tf-call-result
  (implies (and (force (vl-is-token? :vl-sysidtoken)))
           (equal (vl-stmt-p (mv-nth 1 (vl-parse-system-tf-call)))
                  (not (mv-nth 0 (vl-parse-system-tf-call))))))

Theorem: vl-parse-system-tf-call-count-strong

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

Theorem: vl-stmt-kind-of-vl-parse-system-tf-call

(defthm vl-stmt-kind-of-vl-parse-system-tf-call
  (b* (((mv err stmt ?tokstream)
        (vl-parse-system-tf-call)))
    (implies (not err)
             (equal (vl-stmt-kind stmt)
                    :vl-callstmt))))