Matches
(vl-parse-function-statements &key (tokstream 'tokstream) (config 'config)) → (mv errmsg? value new-tokstream)
In Verilog-2005 a function's body can be a single statement. However, in SystemVerilog this is extended to a list of:
function_statement_or_null ::= function_statement | { attribute_instance } ';' function_statement ::= statement
For greater compatibility between Verilog-2005 and SystemVerilog-2012, if we encounter a function whose body is a list of statements, we convert it into an implicit begin/end block.
In the case of tasks, there is evidence that this begin/end treatment is reasonable. From Page 287:
"Multiple statements can be written between the task declaration and endtask. Statements are executed sequentially, the same as if they were enclosed in abegin .... end group. It shall also be legal to have no statements at all."
Similar language is used to describe functions on page 291.
Function:
(defun vl-parse-function-statements-fn (tokstream config) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (vl-loadconfig-p config))) (declare (ignorable config)) (let ((__function__ 'vl-parse-function-statements)) (declare (ignorable __function__)) (seq tokstream (stmts := (vl-parse-function-statements-aux)) (when (atom stmts) (return (make-vl-nullstmt))) (when (atom (cdr stmts)) (return (car stmts))) (return (make-vl-blockstmt :sequentialp t :stmts stmts)))))
Theorem:
(defthm vl-parse-function-statements-fails-gracefully (implies (mv-nth 0 (vl-parse-function-statements)) (not (mv-nth 1 (vl-parse-function-statements)))))
Theorem:
(defthm vl-warning-p-of-vl-parse-function-statements (iff (vl-warning-p (mv-nth 0 (vl-parse-function-statements))) (mv-nth 0 (vl-parse-function-statements))))
Theorem:
(defthm vl-parse-function-statements-result (implies (and t) (equal (vl-stmt-p (mv-nth 1 (vl-parse-function-statements))) (not (mv-nth 0 (vl-parse-function-statements))))))
Theorem:
(defthm vl-parse-function-statements-count-weak (<= (vl-tokstream-measure :tokstream (mv-nth 2 (vl-parse-function-statements))) (vl-tokstream-measure)) :rule-classes ((:rewrite) (:linear)))