• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
        • Symbolic-test-vectors
        • Esim-primitives
        • E-conversion
        • Esim-steps
        • Patterns
        • Mod-internal-paths
        • Defmodules
          • Vl-translation-p
          • Vl-simplify
            • Vl-warn-problem-modulelist
            • Propagating-errors
            • Vl-simpconfig
              • Vl-simpconfig-fix
              • Vl-simpconfig-equiv
              • Make-vl-simpconfig
              • Vl-simpconfig->problem-mods
              • Vl-simpconfig->clean-params-p
              • Vl-simpconfig->unroll-limit
              • Vl-simpconfig->compress-p
              • Vl-simpconfig-p
              • Change-vl-simpconfig
            • Vl-simplify-main
            • Vl-warn-problem-module
            • Vl-design-problem-mods
          • Defmodules-fn
        • Esim-simplify-update-fns
        • Esim-tutorial
        • Esim-vl
      • Vl2014
      • Sv
      • Fgl
      • Vwsim
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Vl-simplify

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.
clean-params-p — booleanp
Should we clean parameters with the clean-params transform before unparameterizing?
unroll-limit — natp
Maximum number of iterations to unroll for loops, etc., when rewriting statements. This is just a safety valve.

Subtopics

Vl-simpconfig-fix
Fixing function for vl-simpconfig structures.
Vl-simpconfig-equiv
Basic equivalence relation for vl-simpconfig structures.
Make-vl-simpconfig
Basic constructor macro for vl-simpconfig structures.
Vl-simpconfig->problem-mods
Get the problem-mods field from a vl-simpconfig.
Vl-simpconfig->clean-params-p
Get the clean-params-p field from a vl-simpconfig.
Vl-simpconfig->unroll-limit
Get the unroll-limit field from a vl-simpconfig.
Vl-simpconfig->compress-p
Get the compress-p field from a vl-simpconfig.
Vl-simpconfig-p
Recognizer for vl-simpconfig structures.
Change-vl-simpconfig
Modifying constructor for vl-simpconfig structures.