Create the hidden vl-vardecls corresponding to the vl-portdecls of a function or task.
(vl-make-hidden-variable-for-portdecl x) → var
See the description of the
Function:
(defun vl-make-hidden-variable-for-portdecl (x) (declare (xargs :guard (vl-portdecl-p x))) (let ((__function__ 'vl-make-hidden-variable-for-portdecl)) (declare (ignorable __function__)) (b* (((vl-portdecl x))) (make-vl-vardecl :name x.name :type x.type :atts (cons (list (hons-copy "VL_HIDDEN_DECL_FOR_TASKPORT")) x.atts) :loc x.loc))))
Theorem:
(defthm vl-vardecl-p-of-vl-make-hidden-variable-for-portdecl (b* ((var (vl-make-hidden-variable-for-portdecl x))) (vl-vardecl-p var)) :rule-classes :rewrite)