Parses everything in
(vl-parse-dpi-import atts &key (tokstream 'tokstream) (config 'config)) → (mv errmsg? value new-tokstream)
SystemVerilog-2012:
dpi_import_export ::= 'import' dpi_spec_string [dpi_function_import_property] [ c_identifier '=' ] dpi_function_proto ';' | 'import' dpi_spec_string [dpi_task_import_property] [ c_identifier '=' ] dpi_task_proto ';' | ... export cases ... dpi_function_import_property ::= 'context' | 'pure' dpi_task_import_property ::= 'context' dpi_function_proto ::= function_prototype dpi_task_proto ::= task_prototype function_prototype ::= 'function' data_type_or_void function_identifier [ '(' [tf_port_list] ')' ] task_prototype ::= 'task' task_identifier [ '(' [tf_port_list] ')' ]
We assume we've just eaten the
Function:
(defun vl-parse-dpi-import-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-dpi-import)) (declare (ignorable __function__)) (seq tokstream (:= (vl-match-token :vl-kwd-import)) (spec := (vl-parse-dpi-spec-string)) (prop := (vl-parse-optional-dpi-function-import-property)) (when (vl-is-token? :vl-idtoken) (c-name := (vl-parse-c-identifier)) (:= (vl-match-token :vl-equalsign))) (fntask := (vl-match-some-token '(:vl-kwd-function :vl-kwd-task))) (when (and (eq (vl-token->type fntask) :vl-kwd-task) (vl-dpiprop-equiv prop :vl-dpi-pure)) (return-raw (vl-parse-error "Can't declare DPI imported task to be pure."))) (when (eq (vl-token->type fntask) :vl-kwd-function) (rettype := (vl-parse-datatype-or-void))) (name := (vl-match-token :vl-idtoken)) (:= (vl-warn-about-deprecated-dpi spec name t)) (portdecls := (vl-parse-very-optional-tf-port-list)) (:= (vl-match-token :vl-semi)) (return (make-vl-dpiimport :name (vl-idtoken->name name) :c-name (or c-name (vl-idtoken->name name)) :spec spec :prop prop :rettype rettype :portdecls portdecls :atts atts :loc (vl-token->loc name))))))
Theorem:
(defthm vl-parse-dpi-import-fails-gracefully (implies (mv-nth 0 (vl-parse-dpi-import atts)) (not (mv-nth 1 (vl-parse-dpi-import atts)))))
Theorem:
(defthm vl-warning-p-of-vl-parse-dpi-import (iff (vl-warning-p (mv-nth 0 (vl-parse-dpi-import atts))) (mv-nth 0 (vl-parse-dpi-import atts))))
Theorem:
(defthm vl-parse-dpi-import-result (implies (and (force (vl-atts-p atts))) (equal (vl-dpiimport-p (mv-nth 1 (vl-parse-dpi-import atts))) (not (mv-nth 0 (vl-parse-dpi-import atts))))))
Theorem:
(defthm vl-parse-dpi-import-count-strong (and (<= (vl-tokstream-measure :tokstream (mv-nth 2 (vl-parse-dpi-import atts))) (vl-tokstream-measure)) (implies (not (mv-nth 0 (vl-parse-dpi-import atts))) (< (vl-tokstream-measure :tokstream (mv-nth 2 (vl-parse-dpi-import atts))) (vl-tokstream-measure)))) :rule-classes ((:rewrite) (:linear)))