• 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-simpconfig

    Change-vl-simpconfig

    Modifying constructor for vl-simpconfig structures.

    Syntax
    (change-vl-simpconfig x 
                          [:compress-p <compress-p>] 
                          [:problem-mods <problem-mods>] 
                          [:clean-params-p <clean-params-p>] 
                          [:unroll-limit <unroll-limit>]) 
    

    This is an often useful alternative to make-vl-simpconfig.

    We construct a new vl-simpconfig structure that is a copy of x, except that you can explicitly change some particular fields. Any fields you don't mention just keep their values from x.

    Definition

    This is an ordinary change- macro introduced by defprod.

    Macro: change-vl-simpconfig

    (defmacro change-vl-simpconfig (x &rest args)
      (std::change-aggregate
           'vl-simpconfig
           x args
           '((:compress-p . vl-simpconfig->compress-p)
             (:problem-mods . vl-simpconfig->problem-mods)
             (:clean-params-p . vl-simpconfig->clean-params-p)
             (:unroll-limit . vl-simpconfig->unroll-limit))
           'change-vl-simpconfig
           'nil))