• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
        • Svex-stvs
        • Svex-decomposition-methodology
        • Sv-versus-esim
        • Svex-decomp
        • Svex-compose-dfs
        • Svex-compilation
        • Moddb
        • Svmods
        • Svstmt
        • Sv-tutorial
        • Expressions
        • Symbolic-test-vector
        • Vl-to-svex
          • Vl-to-sv
          • Vl-design->sv-design
            • Vl-simpconfig
              • Vl-simpconfig-p
              • Make-vl-simpconfig
              • Vl-simpconfig-fix
              • Change-vl-simpconfig
              • Vl-simpconfig-equiv
              • Vl-simpconfig->suppress-fatal-warning-types
              • Vl-simpconfig->user-paramsettings-mode
              • Vl-simpconfig->unparam-bad-instance-fatalp
              • Vl-simpconfig->name-without-default-params
              • Vl-simpconfig->user-paramsettings
              • Vl-simpconfig->uniquecase-constraints
              • Vl-simpconfig->uniquecase-conservative
              • Vl-simpconfig->sv-simplify-verbosep
              • Vl-simpconfig->post-elab-topmods
              • Vl-simpconfig->nb-latch-delay-hack
              • Vl-simpconfig->sv-include-atts
              • Vl-simpconfig->pre-elab-topmods
              • Vl-simpconfig->pre-elab-filter
              • Vl-simpconfig->post-elab-filter
              • Vl-simpconfig->defer-argresolve
              • Vl-simpconfig->already-annotated
              • Vl-simpconfig->allow-bad-topmods
              • Vl-simpconfig->unroll-limit
              • Vl-simpconfig->sv-simplify
              • Vl-simpconfig->problem-mods
              • Vl-simpconfig->compress-p
              • Vl-simpconfig->sc-limit
              • Vl-simpconfig->elab-limit
              • Vl-simpconfig->enum-constraints
              • Vl-simpconfig->enum-fixups
            • Vl-hierarchy-sv-translation
            • Vl-expr-svex-translation
            • Vl-design->svex-modalist
            • Vl-svstmt
          • Vl-to-sv-main
          • Vl-simplify-sv
          • Vl-user-paramsettings->unparam-names
          • Vl-user-paramsettings->modnames
      • Fgl
      • Vwsim
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Vl-design->sv-design

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.