		Search-engine friendly clone of the ACL2 documentation.

Vl-gateinst

Make-vl-gateinst

Basic constructor macro for vl-gateinst structures.

Syntax

(make-vl-gateinst [:type <type>] 
                  [:args <args>] 
                  [:loc <loc>] 
                  [:name <name>] 
                  [:atts <atts>] 
                  [:range <range>] 
                  [:strength <strength>] 
                  [:delay <delay>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-gateinst

(defmacro make-vl-gateinst (&rest args)
  (std::make-aggregate 'vl-gateinst
                       args
                       '((:type)
                         (:args)
                         (:loc)
                         (:name)
                         (:atts)
                         (:range)
                         (:strength)
                         (:delay))
                       'make-vl-gateinst
                       nil))

Function: vl-gateinst

(defun vl-gateinst (type args loc name atts range strength delay)
 (declare (xargs :guard (and (vl-gatetype-p type)
                             (vl-plainarglist-p args)
                             (vl-location-p loc)
                             (maybe-stringp name)
                             (vl-atts-p atts)
                             (vl-maybe-range-p range)
                             (vl-maybe-gatestrength-p strength)
                             (vl-maybe-gatedelay-p delay))))
 (declare (xargs :guard t))
 (let ((__function__ 'vl-gateinst))
  (declare (ignorable __function__))
  (b* ((type (mbe :logic (vl-gatetype-fix type)
                  :exec type))
       (args (mbe :logic (vl-plainarglist-fix args)
                  :exec args))
       (loc (mbe :logic (vl-location-fix loc)
                 :exec loc))
       (name (mbe :logic (maybe-string-fix name)
                  :exec name))
       (atts (mbe :logic (vl-atts-fix atts)
                  :exec atts))
       (range (mbe :logic (vl-maybe-range-fix range)
                   :exec range))
       (strength (mbe :logic (vl-maybe-gatestrength-fix strength)
                      :exec strength))
       (delay (mbe :logic (vl-maybe-gatedelay-fix delay)
                   :exec delay)))
    (cons :vl-gateinst
          (std::prod-cons
               (std::prod-cons (std::prod-cons type args)
                               (std::prod-cons loc name))
               (std::prod-cons (std::prod-cons atts range)
                               (std::prod-cons strength delay)))))))