		Search-engine friendly clone of the ACL2 documentation.

Vl-funtemplate-p

Vl-funinput-to-vardecl

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

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

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

We implement a special hack for Verilog-2005 compatibility. In particular, consider a basic function such as:

function [3:0] AndFn(input [3:0] a, input [3:0] b);
  AndFn = a & b;
endfunction

Our internal representation of function inputs now uses logic types for a and b, which is perfectly fine and sensible. But, when we are trying to cosimulate our simplified modules against the original modules, e.g., in the VL systest directory, then this can cause problems because plain Verilog-2005 simulators don't know about logic types.

To avoid this, when we convert function inputs into wires, we'll just go ahead and ensure the net type is :vl-wire.

Definitions and Theorems

Function: vl-funinput-to-vardecl

(defun vl-funinput-to-vardecl (x)
 (declare (xargs :guard (vl-portdecl-p x)))
 (let ((__function__ 'vl-funinput-to-vardecl))
  (declare (ignorable __function__))
  (b*
   (((vl-portdecl x) x)
    (name-atom (make-vl-atom :guts (make-vl-string :value x.name))))
   (make-vl-vardecl
        :name x.name
        :type x.type
        :nettype :vl-wire
        :atts (acons "VL_FUNCTION_INPUT" name-atom x.atts)
        :loc x.loc))))

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

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