Vl-simpconfig
Options for how to simplify Verilog modules.
This is a product type introduced by defprod.
Fields
- compress-p — booleanp
- Hons the modules at various points. This takes some time, but can produce
smaller translation files.
- problem-mods — string-listp
- Names of modules that should thrown out, perhaps because they cause some kind
of problems.
- already-annotated — booleanp
- Denotes that we've already annotated the design and shouldn't do it
again.
- unroll-limit — natp
- Maximum number of iterations to unroll for loops, etc., when rewriting statements.
This is just a safety valve.
- sc-limit — natp
- Recursion limit for compiling statements, e.g., unrolling loops and
figuring out when they terminate. You might hit this if loops have
non-trivial finishing conditions. Small limits may be preferable for
applications like linting where you don't want a single troublesome loop
to waste inordinate amounts of time. Larger limits may be needed if
you're trying to model a design that has long-running loops.
- elab-limit — natp
- Recursion limit for elaboration. This usually shouldn't matter or need tinkering.
It's a safety valve against possible loops in elaboration, e.g., to
resolve parameter P you need to evaluate parameter Q, which might require
you to resolve R, which might depend hierarchically on P, and so on. So if
you hit this there's probably something wrong with your design.
- uniquecase-conservative — natp
- For unique case and unique0 case statements, a synthesis tool is
allowed to assume that the cases are mutually exclusive and simplify the logic
accordingly. For unique they can assume that exactly one of the tests
will be true. This configuration flag is a natural number that sets the degree
of conservativity, as follows: When 0 (the default), the logic we generate
emulates a simulator, which always executes the first matching case. When
1, if uniqueness is violated, then we pretend that all tests that were 1 instead
evaluated to X, or if all tests were 0 then we pretend all instead evaluated
to X. When 2 or greater, when the condition is violated we pretend all tests
evaluated to X. When 3 or greater, we additionally pretend that all assignments
within the case statement write X instead of the given value. The intention
behind this is to make it likely that our logic is conservative with respect
to anything a synthesis tool might produce.
- uniquecase-constraints — booleanp
- Generate constraints for unique case and unique0 case statements.
Likely you do not want both this and uniquecase-conservative to be set,
because they are two different approaches for dealing with a synthesis tool's
flexibility in dealing with unique and unique0 case statements. When this
is set, we separately store a constraint saying that the cases are one-hot
or one/zero-hot, respectively. This constraint is stored in the SV modules
when they are generated by vl-design->sv-design.
- enum-constraints
- Generate constraints for variables of enum datatypes, or compound datatypes
that have enum subfields. These constraints are saved in the SV modules
when they are generated by vl-design->sv-design. Each constraint
says that an enum field's value is one of the proper values of an enum type.
If NIL (the default), these constraints are not generated. If T or any nonnil
object other than the keyword :ALL, then the constraints are generated except
for port variables. If :ALL, then these are generated for ports as well.
- enum-fixups
- Generate fixups for variables of enum datatypes, or compound datatypes
that have enum subfields. These cause svex compilation to fix up enum
values to be X if not one of the allowed values. If NIL (the default), this
fixing will not be done. Similar to the enum-constraints option, fixups
are only done for non-port variables unless this option is set to the keyword
:ALL.
- sv-simplify — booleanp
- Apply svex rewriting to the results of compiling procedural blocks.
- sv-simplify-verbosep — booleanp
- Verbosely report svex rewriting statistics.
- sv-include-atts — string-listp
- Translate SystemVerilog attributes on variable declarations into sv modules.
- nb-latch-delay-hack — booleanp
- Artificially add a delay to nonblocking assignments in latch-like contexts.
- name-without-default-params — booleanp
- Omit non-overridden parameters from module names generated by unparameterization.
- unparam-bad-instance-fatalp — booleanp
- Make a fatal warning when a nonexistent parameter is overridden by a module instance.
- defer-argresolve — booleanp
- Don't run the argresolve transform before elaborate; instead, do it once
the parameters for the given module are resolved. This may avoid errors
when a module conditionally instantiates another module that hasn't been
found, but the condition under which it instantiates that module is never
satisfied.
- suppress-fatal-warning-types — ACL2::symbol-list
- Treat the listed warnings as non-fatal during vl-design-propagate-errors.
Such warnings will still show up as fatal, but the modules in which they exist
will not be labeled "bad".
- user-paramsettings — vl-user-paramsettings
- Gives a list of modules to build with particular parameter settings. The
argument should be list of vl-user-paramsetting objects, containing a
module name (string), a name for the module after elaboration (string),
and an alist mapping parameter names (strings) to integer values.
Currently this doesn't allow for setting parameters to non-integer values,
e.g. type parameters. Modules may be listed more than once with different
parameter settings.
- user-paramsettings-mode — vl-user-paramsettings-mode-p
- Determines how top-level modules are parameterized in elaboration. The
default setting is :default, under which each top-level module is
elaborated with its default parameters unless that module is listed in the
user-paramsettings. With the :user-only setting, top-level modules
are only elaborated according to the user-paramsettings; if a top-level
module doesn't appear in the user-paramsettings, it isn't elaborated at
all and is omitted from the design after elaboration. With the
:include-toplevel setting, top-level modules are built with their
default parameter settings as well as whatever settings they appear with
in the user-paramsettings. Note that the top-level modules present at
elaboration time is influenced by the settings of pre-elab-topmods
and pre-elab-filter.
- pre-elab-topmods — string-listp
- List of module names to be preserved after annotation and before
elaboration. When pre-elab-filter is set, a pass of vl-remove-unnecessary-elements will be used to omit from the design any
elements not used by one of these modules. The module names in the
user-paramsettings are automatically included in this list.
- pre-elab-filter — booleanp
- Filter out unnecessary elements (according to pre-elab-topmods and
user-paramsettings) before elaboration.
- post-elab-topmods — string-listp
- List of module names to be preserved after elaboration. When
post-elab-filter is set, a pass of vl-remove-unnecessary-elements will be used to omit from the design any
elements not used by one of these modules. Note that these names may need
to have parameter settings appended. The unparam-names included in the
user-paramsettings are automatically included in this list.
- post-elab-filter — booleanp
- Filter out unnecessary elements (according to post-elab-topmods and
user-paramsettings) after elaboration.
- allow-bad-topmods — booleanp
- In vl-to-sv, return an error message after elaboration if any
modules required by post-elab-topmods or user-paramsettings had
fatal warnings.
Subtopics
- Vl-simpconfig-p
- Recognizer for vl-simpconfig structures.
- Make-vl-simpconfig
- Basic constructor macro for vl-simpconfig structures.
- Vl-simpconfig-fix
- Fixing function for vl-simpconfig structures.
- Change-vl-simpconfig
- Modifying constructor for vl-simpconfig structures.
- Vl-simpconfig-equiv
- Basic equivalence relation for vl-simpconfig structures.
- Vl-simpconfig->suppress-fatal-warning-types
- Get the suppress-fatal-warning-types field from a vl-simpconfig.
- Vl-simpconfig->user-paramsettings-mode
- Get the user-paramsettings-mode field from a vl-simpconfig.
- Vl-simpconfig->unparam-bad-instance-fatalp
- Get the unparam-bad-instance-fatalp field from a vl-simpconfig.
- Vl-simpconfig->name-without-default-params
- Get the name-without-default-params field from a vl-simpconfig.
- Vl-simpconfig->user-paramsettings
- Get the user-paramsettings field from a vl-simpconfig.
- Vl-simpconfig->uniquecase-constraints
- Get the uniquecase-constraints field from a vl-simpconfig.
- Vl-simpconfig->uniquecase-conservative
- Get the uniquecase-conservative field from a vl-simpconfig.
- Vl-simpconfig->sv-simplify-verbosep
- Get the sv-simplify-verbosep field from a vl-simpconfig.
- Vl-simpconfig->post-elab-topmods
- Get the post-elab-topmods field from a vl-simpconfig.
- Vl-simpconfig->nb-latch-delay-hack
- Get the nb-latch-delay-hack field from a vl-simpconfig.
- Vl-simpconfig->sv-include-atts
- Get the sv-include-atts field from a vl-simpconfig.
- Vl-simpconfig->pre-elab-topmods
- Get the pre-elab-topmods field from a vl-simpconfig.
- Vl-simpconfig->pre-elab-filter
- Get the pre-elab-filter field from a vl-simpconfig.
- Vl-simpconfig->post-elab-filter
- Get the post-elab-filter field from a vl-simpconfig.
- Vl-simpconfig->defer-argresolve
- Get the defer-argresolve field from a vl-simpconfig.
- Vl-simpconfig->already-annotated
- Get the already-annotated field from a vl-simpconfig.
- Vl-simpconfig->allow-bad-topmods
- Get the allow-bad-topmods field from a vl-simpconfig.
- Vl-simpconfig->unroll-limit
- Get the unroll-limit field from a vl-simpconfig.
- Vl-simpconfig->sv-simplify
- Get the sv-simplify field from a vl-simpconfig.
- Vl-simpconfig->problem-mods
- Get the problem-mods field from a vl-simpconfig.
- Vl-simpconfig->compress-p
- Get the compress-p field from a vl-simpconfig.
- Vl-simpconfig->sc-limit
- Get the sc-limit field from a vl-simpconfig.
- Vl-simpconfig->elab-limit
- Get the elab-limit field from a vl-simpconfig.
- Vl-simpconfig->enum-constraints
- Get the enum-constraints field from a vl-simpconfig.
- Vl-simpconfig->enum-fixups
- Get the enum-fixups field from a vl-simpconfig.