		Search-engine friendly clone of the ACL2 documentation.

Vl-clkdecl

Make-vl-clkdecl

Basic constructor macro for vl-clkdecl structures.

Syntax

(make-vl-clkdecl [:defaultp <defaultp>] 
                 [:name <name>] 
                 [:event <event>] 
                 [:iskew <iskew>] 
                 [:oskew <oskew>] 
                 [:clkassigns <clkassigns>] 
                 [:properties <properties>] 
                 [:sequences <sequences>] 
                 [:loc <loc>] 
                 [:atts <atts>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-clkdecl

(defmacro make-vl-clkdecl (&rest args)
  (std::make-aggregate 'vl-clkdecl
                       args
                       '((:defaultp)
                         (:name)
                         (:event)
                         (:iskew)
                         (:oskew)
                         (:clkassigns)
                         (:properties)
                         (:sequences)
                         (:loc)
                         (:atts))
                       'make-vl-clkdecl
                       nil))

Function: vl-clkdecl

(defun vl-clkdecl (defaultp name event iskew oskew clkassigns
                            properties sequences loc atts)
 (declare (xargs :guard (and (booleanp defaultp)
                             (maybe-stringp name)
                             (vl-evatomlist-p event)
                             (vl-maybe-clkskew-p iskew)
                             (vl-maybe-clkskew-p oskew)
                             (vl-clkassignlist-p clkassigns)
                             (vl-propertylist-p properties)
                             (vl-sequencelist-p sequences)
                             (vl-location-p loc)
                             (vl-atts-p atts))))
 (declare (xargs :guard t))
 (let ((__function__ 'vl-clkdecl))
  (declare (ignorable __function__))
  (b* ((defaultp (mbe :logic (acl2::bool-fix defaultp)
                      :exec defaultp))
       (name (mbe :logic (maybe-string-fix name)
                  :exec name))
       (event (mbe :logic (vl-evatomlist-fix event)
                   :exec event))
       (iskew (mbe :logic (vl-maybe-clkskew-fix iskew)
                   :exec iskew))
       (oskew (mbe :logic (vl-maybe-clkskew-fix oskew)
                   :exec oskew))
       (clkassigns (mbe :logic (vl-clkassignlist-fix clkassigns)
                        :exec clkassigns))
       (properties (mbe :logic (vl-propertylist-fix properties)
                        :exec properties))
       (sequences (mbe :logic (vl-sequencelist-fix sequences)
                       :exec sequences))
       (loc (mbe :logic (vl-location-fix loc)
                 :exec loc))
       (atts (mbe :logic (vl-atts-fix atts)
                  :exec atts)))
   (cons
      :vl-clkdecl
      (std::prod-cons
           (std::prod-cons
                (std::prod-cons defaultp name)
                (std::prod-cons event (std::prod-cons iskew oskew)))
           (std::prod-cons
                (std::prod-cons clkassigns properties)
                (std::prod-cons sequences
                                (std::prod-cons loc atts))))))))