		Search-engine friendly clone of the ACL2 documentation.

Defsvtv-args

Make-defsvtv-args

Basic constructor macro for defsvtv-args structures.

Syntax

(make-defsvtv-args [:name <name>] 
                   [:stages <stages>] 
                   [:inputs <inputs>] 
                   [:overrides <overrides>] 
                   [:outputs <outputs>] 
                   [:internals <internals>] 
                   [:design <design>] 
                   [:design-const <design-const>] 
                   [:labels <labels>] 
                   [:phase-config <phase-config>] 
                   [:clocks <clocks>] 
                   [:phase-scc-limit <phase-scc-limit>] 
                   [:monotonify <monotonify>] 
                   [:simplify <simplify>] 
                   [:pre-simplify <pre-simplify>] 
                   [:pipe-simp <pipe-simp>] 
                   [:cycle-phases <cycle-phases>] 
                   [:cycle-phases-p <cycle-phases-p>] 
                   [:cycle-simp <cycle-simp>] 
                   [:initial-state-vars <initial-state-vars>] 
                   [:define-macros <define-macros>] 
                   [:define-mod <define-mod>] 
                   [:parents <parents>] 
                   [:short <short>] 
                   [:long <long>] 
                   [:form <form>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-defsvtv-args

(defmacro make-defsvtv-args (&rest args)
 (std::make-aggregate
   'defsvtv-args
   args
   '((:name)
     (:stages)
     (:inputs)
     (:overrides)
     (:outputs)
     (:internals)
     (:design)
     (:design-const)
     (:labels)
     (:phase-config
          make-phase-fsm-config
          :override-config (make-svtv-assigns-override-config-omit))
     (:clocks)
     (:phase-scc-limit)
     (:monotonify . t)
     (:simplify . t)
     (:pre-simplify . t)
     (:pipe-simp)
     (:cycle-phases)
     (:cycle-phases-p)
     (:cycle-simp)
     (:initial-state-vars)
     (:define-macros . t)
     (:define-mod)
     (:parents)
     (:short)
     (:long)
     (:form))
   'make-defsvtv-args
   nil))

Function: defsvtv-args

(defun defsvtv-args (name stages
                          inputs overrides outputs internals
                          design design-const labels phase-config
                          clocks phase-scc-limit monotonify
                          simplify pre-simplify pipe-simp
                          cycle-phases cycle-phases-p cycle-simp
                          initial-state-vars define-macros
                          define-mod parents short long form)
 (declare (xargs :guard (and (symbolp name)
                             (true-list-listp stages)
                             (true-list-listp inputs)
                             (true-list-listp overrides)
                             (true-list-listp outputs)
                             (true-list-listp internals)
                             (design-p design)
                             (symbolp design-const)
                             (symbol-listp labels)
                             (phase-fsm-config-p phase-config)
                             (svarlist-p clocks)
                             (maybe-natp phase-scc-limit)
                             (booleanp monotonify)
                             (booleanp simplify)
                             (booleanp pre-simplify)
                             (svex-simpconfig-p pipe-simp)
                             (svtv-cyclephaselist-p cycle-phases)
                             (svex-simpconfig-p cycle-simp)
                             (booleanp initial-state-vars))))
 (declare (xargs :guard t))
 (let ((__function__ 'defsvtv-args))
  (declare (ignorable __function__))
  (b*
   ((name (mbe :logic (acl2::symbol-fix name)
               :exec name))
    (stages (mbe :logic (true-list-list-fix stages)
                 :exec stages))
    (inputs (mbe :logic (true-list-list-fix inputs)
                 :exec inputs))
    (overrides (mbe :logic (true-list-list-fix overrides)
                    :exec overrides))
    (outputs (mbe :logic (true-list-list-fix outputs)
                  :exec outputs))
    (internals (mbe :logic (true-list-list-fix internals)
                    :exec internals))
    (design (mbe :logic (design-fix design)
                 :exec design))
    (design-const (mbe :logic (acl2::symbol-fix design-const)
                       :exec design-const))
    (labels (mbe :logic (acl2::symbol-list-fix labels)
                 :exec labels))
    (phase-config (mbe :logic (phase-fsm-config-fix phase-config)
                       :exec phase-config))
    (clocks (mbe :logic (svarlist-fix clocks)
                 :exec clocks))
    (phase-scc-limit
         (mbe :logic (acl2::maybe-natp-fix phase-scc-limit)
              :exec phase-scc-limit))
    (monotonify (mbe :logic (bool-fix monotonify)
                     :exec monotonify))
    (simplify (mbe :logic (bool-fix simplify)
                   :exec simplify))
    (pre-simplify (mbe :logic (bool-fix pre-simplify)
                       :exec pre-simplify))
    (pipe-simp (mbe :logic (svex-simpconfig-fix pipe-simp)
                    :exec pipe-simp))
    (cycle-phases (mbe :logic (svtv-cyclephaselist-fix cycle-phases)
                       :exec cycle-phases))
    (cycle-simp (mbe :logic (svex-simpconfig-fix cycle-simp)
                     :exec cycle-simp))
    (initial-state-vars (mbe :logic (bool-fix initial-state-vars)
                             :exec initial-state-vars)))
   (list name stages
         inputs overrides outputs internals
         design design-const labels phase-config
         clocks phase-scc-limit monotonify
         simplify pre-simplify pipe-simp
         cycle-phases cycle-phases-p cycle-simp
         initial-state-vars define-macros
         define-mod parents short long form))))