Basic constructor macro for svtv-data-obj structures.
(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.
This is an ordinary
Macro:
(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:
(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))))