		Search-engine friendly clone of the ACL2 documentation.

Vl-modinst

Make-vl-modinst

Basic constructor macro for vl-modinst structures.

Syntax

(make-vl-modinst [:instname <instname>] 
                 [:modname <modname>] 
                 [:range <range>] 
                 [:paramargs <paramargs>] 
                 [:portargs <portargs>] 
                 [:str <str>] 
                 [:delay <delay>] 
                 [:atts <atts>] 
                 [:loc <loc>])

This is the usual way to construct vl-modinst structures. It simply conses together a structure with the specified fields.

This macro generates a new vl-modinst structure from scratch. See also change-vl-modinst, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-modinst

(defmacro make-vl-modinst (&rest args)
  (std::make-aggregate 'vl-modinst
                       args
                       '((:instname)
                         (:modname)
                         (:range)
                         (:paramargs)
                         (:portargs)
                         (:str)
                         (:delay)
                         (:atts)
                         (:loc))
                       'make-vl-modinst
                       nil))

Function: vl-modinst

(defun vl-modinst (instname modname range
                            paramargs portargs str delay atts loc)
 (declare (xargs :guard (and (maybe-stringp instname)
                             (stringp modname)
                             (vl-maybe-range-p range)
                             (vl-paramargs-p paramargs)
                             (vl-arguments-p portargs)
                             (vl-maybe-gatestrength-p str)
                             (vl-maybe-gatedelay-p delay)
                             (vl-atts-p atts)
                             (vl-location-p loc))))
 (declare (xargs :guard t))
 (let ((__function__ 'vl-modinst))
  (declare (ignorable __function__))
  (b* ((instname (mbe :logic (maybe-string-fix instname)
                      :exec instname))
       (modname (mbe :logic (str-fix modname)
                     :exec modname))
       (range (mbe :logic (vl-maybe-range-fix range)
                   :exec range))
       (paramargs (mbe :logic (vl-paramargs-fix paramargs)
                       :exec paramargs))
       (portargs (mbe :logic (vl-arguments-fix portargs)
                      :exec portargs))
       (str (mbe :logic (vl-maybe-gatestrength-fix str)
                 :exec str))
       (delay (mbe :logic (vl-maybe-gatedelay-fix delay)
                   :exec delay))
       (atts (mbe :logic (vl-atts-fix atts)
                  :exec atts))
       (loc (mbe :logic (vl-location-fix loc)
                 :exec loc)))
   (cons
    :vl-modinst
    (std::prod-cons
         (std::prod-cons (std::prod-cons instname modname)
                         (std::prod-cons range paramargs))
         (std::prod-cons
              (std::prod-cons portargs str)
              (std::prod-cons delay (std::prod-cons atts loc))))))))