		Search-engine friendly clone of the ACL2 documentation.

Svtv-data-obj

Make-svtv-data-obj

Basic constructor macro for svtv-data-obj structures.

Syntax

(make-svtv-data-obj [:design <design>] 
                    [:user-names <user-names>] 
                    [:namemap <namemap>] 
                    [:namemap-validp <namemap-validp>] 
                    [:flatten <flatten>] 
                    [:flatten-validp <flatten-validp>] 
                    [:flatnorm-setup <flatnorm-setup>] 
                    [:flatnorm <flatnorm>] 
                    [:flatnorm-validp <flatnorm-validp>] 
                    [:phase-fsm-setup <phase-fsm-setup>] 
                    [:phase-fsm <phase-fsm>] 
                    [:phase-fsm-validp <phase-fsm-validp>] 
                    [:cycle-phases <cycle-phases>] 
                    [:cycle-fsm <cycle-fsm>] 
                    [:cycle-fsm-validp <cycle-fsm-validp>] 
                    [:pipeline-setup <pipeline-setup>] 
                    [:pipeline <pipeline>] 
                    [:pipeline-validp <pipeline-validp>])

This is the usual way to construct svtv-data-obj structures. It simply conses together a structure with the specified fields.

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-svtv-data-obj

(defmacro make-svtv-data-obj (&rest args)
  (std::make-aggregate 'svtv-data-obj
                       args
                       '((:design)
                         (:user-names)
                         (:namemap)
                         (:namemap-validp)
                         (:flatten)
                         (:flatten-validp)
                         (:flatnorm-setup)
                         (:flatnorm)
                         (:flatnorm-validp)
                         (:phase-fsm-setup)
                         (:phase-fsm)
                         (:phase-fsm-validp)
                         (:cycle-phases)
                         (:cycle-fsm)
                         (:cycle-fsm-validp)
                         (:pipeline-setup)
                         (:pipeline)
                         (:pipeline-validp))
                       'make-svtv-data-obj
                       nil))

Function: svtv-data-obj

(defun svtv-data-obj
       (design user-names namemap namemap-validp
               flatten flatten-validp flatnorm-setup
               flatnorm flatnorm-validp phase-fsm-setup
               phase-fsm phase-fsm-validp
               cycle-phases cycle-fsm cycle-fsm-validp
               pipeline-setup pipeline pipeline-validp)
 (declare (xargs :guard (and (design-p design)
                             (svtv-namemap-p user-names)
                             (svtv-name-lhs-map-p namemap)
                             (booleanp namemap-validp)
                             (flatten-res-p flatten)
                             (booleanp flatten-validp)
                             (flatnorm-setup-p flatnorm-setup)
                             (flatnorm-res-p flatnorm)
                             (booleanp flatnorm-validp)
                             (phase-fsm-config-p phase-fsm-setup)
                             (fsm-p phase-fsm)
                             (booleanp phase-fsm-validp)
                             (svtv-cyclephaselist-p cycle-phases)
                             (fsm-p cycle-fsm)
                             (booleanp cycle-fsm-validp)
                             (pipeline-setup-p pipeline-setup)
                             (svex-alist-p pipeline)
                             (booleanp pipeline-validp))))
 (declare (xargs :guard t))
 (let ((__function__ 'svtv-data-obj))
  (declare (ignorable __function__))
  (b*
   ((design (mbe :logic (design-fix design)
                 :exec design))
    (user-names (mbe :logic (svtv-namemap-fix user-names)
                     :exec user-names))
    (namemap (mbe :logic (svtv-name-lhs-map-fix namemap)
                  :exec namemap))
    (namemap-validp (mbe :logic (bool-fix namemap-validp)
                         :exec namemap-validp))
    (flatten (mbe :logic (flatten-res-fix flatten)
                  :exec flatten))
    (flatten-validp (mbe :logic (bool-fix flatten-validp)
                         :exec flatten-validp))
    (flatnorm-setup (mbe :logic (flatnorm-setup-fix flatnorm-setup)
                         :exec flatnorm-setup))
    (flatnorm (mbe :logic (flatnorm-res-fix flatnorm)
                   :exec flatnorm))
    (flatnorm-validp (mbe :logic (bool-fix flatnorm-validp)
                          :exec flatnorm-validp))
    (phase-fsm-setup
         (mbe :logic (phase-fsm-config-fix phase-fsm-setup)
              :exec phase-fsm-setup))
    (phase-fsm (mbe :logic (fsm-fix phase-fsm)
                    :exec phase-fsm))
    (phase-fsm-validp (mbe :logic (bool-fix phase-fsm-validp)
                           :exec phase-fsm-validp))
    (cycle-phases (mbe :logic (svtv-cyclephaselist-fix cycle-phases)
                       :exec cycle-phases))
    (cycle-fsm (mbe :logic (fsm-fix cycle-fsm)
                    :exec cycle-fsm))
    (cycle-fsm-validp (mbe :logic (bool-fix cycle-fsm-validp)
                           :exec cycle-fsm-validp))
    (pipeline-setup (mbe :logic (pipeline-setup-fix pipeline-setup)
                         :exec pipeline-setup))
    (pipeline (mbe :logic (svex-alist-fix pipeline)
                   :exec pipeline))
    (pipeline-validp (mbe :logic (bool-fix pipeline-validp)
                          :exec pipeline-validp)))
   (list design user-names namemap
         namemap-validp flatten flatten-validp
         flatnorm-setup flatnorm flatnorm-validp
         phase-fsm-setup phase-fsm
         phase-fsm-validp cycle-phases cycle-fsm
         cycle-fsm-validp pipeline-setup
         pipeline pipeline-validp))))