|
|
|---|
|
|
|
|---|
Basic constructor macro for vl-simpconfig structures.
(make-vl-simpconfig [:compress-p <compress-p>]
[:problem-mods <problem-mods>]
[:already-annotated <already-annotated>]
[:unroll-limit <unroll-limit>]
[:sc-limit <sc-limit>]
[:elab-limit <elab-limit>]
[:uniquecase-conservative <uniquecase-conservative>]
[:uniquecase-constraints <uniquecase-constraints>]
[:enum-constraints <enum-constraints>]
[:enum-fixups <enum-fixups>]
[:sv-simplify <sv-simplify>]
[:sv-simplify-verbosep <sv-simplify-verbosep>]
[:sv-include-atts <sv-include-atts>]
[:nb-latch-delay-hack <nb-latch-delay-hack>]
[:name-without-default-params <name-without-default-params>]
[:unparam-bad-instance-fatalp <unparam-bad-instance-fatalp>]
[:defer-argresolve <defer-argresolve>]
[:suppress-fatal-warning-types <suppress-fatal-warning-types>]
[:user-paramsettings <user-paramsettings>]
[:user-paramsettings-mode <user-paramsettings-mode>]
[:pre-elab-topmods <pre-elab-topmods>]
[:pre-elab-filter <pre-elab-filter>]
[:post-elab-topmods <post-elab-topmods>]
[:post-elab-filter <post-elab-filter>]
[:allow-bad-topmods <allow-bad-topmods>])
This is the usual way to construct vl-simpconfig structures. It simply conses together a structure with the specified fields.
This macro generates a new vl-simpconfig structure from scratch. See also change-vl-simpconfig, which can "change" an existing structure, instead.
This is an ordinary
Macro:
(defmacro make-vl-simpconfig (&rest args) (std::make-aggregate 'vl-simpconfig args '((:compress-p) (:problem-mods) (:already-annotated) (:unroll-limit . 1000) (:sc-limit . 1000) (:elab-limit . 10000) (:uniquecase-conservative . 0) (:uniquecase-constraints) (:enum-constraints) (:enum-fixups) (:sv-simplify . t) (:sv-simplify-verbosep) (:sv-include-atts) (:nb-latch-delay-hack) (:name-without-default-params) (:unparam-bad-instance-fatalp . t) (:defer-argresolve) (:suppress-fatal-warning-types) (:user-paramsettings) (:user-paramsettings-mode quote :default) (:pre-elab-topmods) (:pre-elab-filter . t) (:post-elab-topmods) (:post-elab-filter . t) (:allow-bad-topmods)) 'make-vl-simpconfig nil))
Function:
(defun vl-simpconfig (compress-p problem-mods already-annotated unroll-limit sc-limit elab-limit uniquecase-conservative uniquecase-constraints enum-constraints enum-fixups sv-simplify sv-simplify-verbosep sv-include-atts nb-latch-delay-hack name-without-default-params unparam-bad-instance-fatalp defer-argresolve suppress-fatal-warning-types user-paramsettings user-paramsettings-mode pre-elab-topmods pre-elab-filter post-elab-topmods post-elab-filter allow-bad-topmods) (declare (xargs :guard (and (booleanp compress-p) (string-listp problem-mods) (booleanp already-annotated) (natp unroll-limit) (natp sc-limit) (natp elab-limit) (natp uniquecase-conservative) (booleanp uniquecase-constraints) (booleanp sv-simplify) (booleanp sv-simplify-verbosep) (string-listp sv-include-atts) (booleanp nb-latch-delay-hack) (booleanp name-without-default-params) (booleanp unparam-bad-instance-fatalp) (booleanp defer-argresolve) (symbol-listp suppress-fatal-warning-types) (vl-user-paramsettings-p user-paramsettings) (vl-user-paramsettings-mode-p user-paramsettings-mode) (string-listp pre-elab-topmods) (booleanp pre-elab-filter) (string-listp post-elab-topmods) (booleanp post-elab-filter) (booleanp allow-bad-topmods)))) (declare (xargs :guard t)) (let ((__function__ 'vl-simpconfig)) (declare (ignorable __function__)) (b* ((compress-p (mbe :logic (acl2::bool-fix compress-p) :exec compress-p)) (problem-mods (mbe :logic (string-list-fix problem-mods) :exec problem-mods)) (already-annotated (mbe :logic (acl2::bool-fix already-annotated) :exec already-annotated)) (unroll-limit (mbe :logic (nfix unroll-limit) :exec unroll-limit)) (sc-limit (mbe :logic (nfix sc-limit) :exec sc-limit)) (elab-limit (mbe :logic (nfix elab-limit) :exec elab-limit)) (uniquecase-conservative (mbe :logic (nfix uniquecase-conservative) :exec uniquecase-conservative)) (uniquecase-constraints (mbe :logic (acl2::bool-fix uniquecase-constraints) :exec uniquecase-constraints)) (sv-simplify (mbe :logic (acl2::bool-fix sv-simplify) :exec sv-simplify)) (sv-simplify-verbosep (mbe :logic (acl2::bool-fix sv-simplify-verbosep) :exec sv-simplify-verbosep)) (sv-include-atts (mbe :logic (string-list-fix sv-include-atts) :exec sv-include-atts)) (nb-latch-delay-hack (mbe :logic (acl2::bool-fix nb-latch-delay-hack) :exec nb-latch-delay-hack)) (name-without-default-params (mbe :logic (acl2::bool-fix name-without-default-params) :exec name-without-default-params)) (unparam-bad-instance-fatalp (mbe :logic (acl2::bool-fix unparam-bad-instance-fatalp) :exec unparam-bad-instance-fatalp)) (defer-argresolve (mbe :logic (acl2::bool-fix defer-argresolve) :exec defer-argresolve)) (suppress-fatal-warning-types (mbe :logic (acl2::symbol-list-fix suppress-fatal-warning-types) :exec suppress-fatal-warning-types)) (user-paramsettings (mbe :logic (vl-user-paramsettings-fix user-paramsettings) :exec user-paramsettings)) (user-paramsettings-mode (mbe :logic (vl-user-paramsettings-mode-fix user-paramsettings-mode) :exec user-paramsettings-mode)) (pre-elab-topmods (mbe :logic (string-list-fix pre-elab-topmods) :exec pre-elab-topmods)) (pre-elab-filter (mbe :logic (acl2::bool-fix pre-elab-filter) :exec pre-elab-filter)) (post-elab-topmods (mbe :logic (string-list-fix post-elab-topmods) :exec post-elab-topmods)) (post-elab-filter (mbe :logic (acl2::bool-fix post-elab-filter) :exec post-elab-filter)) (allow-bad-topmods (mbe :logic (acl2::bool-fix allow-bad-topmods) :exec allow-bad-topmods))) (cons :vl-simpconfig (list compress-p problem-mods already-annotated unroll-limit sc-limit elab-limit uniquecase-conservative uniquecase-constraints enum-constraints enum-fixups sv-simplify sv-simplify-verbosep sv-include-atts nb-latch-delay-hack name-without-default-params unparam-bad-instance-fatalp defer-argresolve suppress-fatal-warning-types user-paramsettings user-paramsettings-mode pre-elab-topmods pre-elab-filter post-elab-topmods post-elab-filter allow-bad-topmods)))))