Generate the initial template for expanding a function.
(vl-fundecl-expansion-template x warnings) → (mv template? warnings)
We try to generate a vl-funtemplate-p corresponding to
Creating the template for a function is a pretty elaborate process which involves a lot of sanity checking, and will fail if the function includes unsupported constructs or doesn't meet our other sanity criteria.
Function:
(defun vl-fundecl-expansion-template (x warnings) (declare (xargs :guard (and (vl-fundecl-p x) (vl-warninglist-p warnings)))) (let ((__function__ 'vl-fundecl-expansion-template)) (declare (ignorable __function__)) (b* (((vl-fundecl x) x) (vardecls (vl-remove-fake-function-vardecls x.vardecls)) ((mv okp warnings) (vl-fun-vardecllist-types-okp vardecls warnings x)) ((unless okp) (mv nil warnings)) ((mv okp warnings) (vl-portdecllist-types-okp x.portdecls warnings x)) ((unless okp) (mv nil warnings)) ((mv okp warnings assigns) (vl-funbody-to-assignments x warnings)) ((unless okp) (mv nil warnings)) (funname-atom (make-vl-atom :guts (make-vl-funname :name x.name))) (result-var (make-vl-vardecl :name x.name :type x.rettype :nettype :vl-wire :atts (list (cons "VL_FUNCTION_RETURN" funname-atom)) :loc x.loc)) (template (make-vl-funtemplate :name x.name :inputs (vl-funinputlist-to-vardecls x.portdecls) :locals (vl-fun-vardecllist-to-vardecls vardecls) :out result-var :assigns assigns))) (mv template warnings))))
Theorem:
(defthm return-type-of-vl-fundecl-expansion-template.template? (b* (((mv ?template? ?warnings) (vl-fundecl-expansion-template x warnings))) (equal (vl-funtemplate-p template?) (if template? t nil))) :rule-classes :rewrite)
Theorem:
(defthm vl-warninglist-p-of-vl-fundecl-expansion-template.warnings (b* (((mv ?template? ?warnings) (vl-fundecl-expansion-template x warnings))) (vl-warninglist-p warnings)) :rule-classes :rewrite)