		Search-engine friendly clone of the ACL2 documentation.

Vl-funtemplate-p

Vl-fun-vardecl-to-vardecl

Convert a function's var declaration into a net declaration for its funtemplate.

Signature
(vl-fun-vardecl-to-vardecl x) → vardecl
Arguments: x — Guard (vl-vardecl-p x).
Returns: vardecl — Type (vl-vardecl-p vardecl).

We assume the input is okay in the sense of vl-fun-vardecllist-types-okp.

Definitions and Theorems

Function: vl-fun-vardecl-to-vardecl

(defun vl-fun-vardecl-to-vardecl (x)
 (declare (xargs :guard (vl-vardecl-p x)))
 (declare (xargs :guard (vl-simplereg-p x)))
 (let ((__function__ 'vl-fun-vardecl-to-vardecl))
  (declare (ignorable __function__))
  (b*
   (((vl-vardecl x) x)
    (name-atom (make-vl-atom :guts (make-vl-string :value x.name)))
    (range (vl-simplereg->range x))
    (type (make-vl-coretype :name :vl-logic
                            :pdims (and range (list range))
                            :signedp (vl-simplereg->signedp x))))
   (make-vl-vardecl :name x.name
                    :type type
                    :nettype :vl-wire
                    :atts (acons "VL_FUNCTION_VAR" name-atom x.atts)
                    :loc x.loc))))

Theorem: vl-vardecl-p-of-vl-fun-vardecl-to-vardecl

(defthm vl-vardecl-p-of-vl-fun-vardecl-to-vardecl
  (b* ((vardecl (vl-fun-vardecl-to-vardecl x)))
    (vl-vardecl-p vardecl))
  :rule-classes :rewrite)