Ensure that a function's statement conforms to the Function Rules in 10.4.4.
(vl-fun-stmt-okp x warnings function) → (mv okp warnings)
We check to see if the statement conforms to the Function Rules in 10.4.4. In particular, we want to ensure that the function's body:
Practically speaking there are a lot of other things that our function expansion code doesn't support (complex case statements, loops, functions that don't write to variables before reading them, etc.) but that the Verilog-2005 standard doesn't prohibit, so this is not a very complete check as far as VL is concerned. But, I think it's nice to at least explicitly check for the "officially forbidden" stuff first.
Theorem:
(defthm return-type-of-vl-fun-stmt-okp.okp (b* (((mv ?okp ?warnings) (vl-fun-stmt-okp x warnings function))) (booleanp okp)) :rule-classes :type-prescription)
Theorem:
(defthm return-type-of-vl-fun-stmt-okp.warnings (b* (((mv ?okp ?warnings) (vl-fun-stmt-okp x warnings function))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-fun-stmtlist-okp.okp (b* (((mv ?okp ?warnings) (vl-fun-stmtlist-okp x warnings function))) (booleanp okp)) :rule-classes :type-prescription)
Theorem:
(defthm return-type-of-vl-fun-stmtlist-okp.warnings (b* (((mv ?okp ?warnings) (vl-fun-stmtlist-okp x warnings function))) (vl-warninglist-p warnings)) :rule-classes :rewrite)