• 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

Make-vl-simpconfig

Basic constructor macro for vl-simpconfig structures.

Syntax

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

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.

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-simpconfig

(defmacro make-vl-simpconfig (&rest args)
  (std::make-aggregate 'vl-simpconfig
                       args
                       '((:compress-p)
                         (:problem-mods)
                         (:clean-params-p . t)
                         (:unroll-limit . 1000))
                       'make-vl-simpconfig
                       nil))

Function: vl-simpconfig

(defun vl-simpconfig (compress-p problem-mods
                                 clean-params-p unroll-limit)
 (declare (xargs :guard (and (booleanp compress-p)
                             (string-listp problem-mods)
                             (booleanp clean-params-p)
                             (natp unroll-limit))))
 (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))
       (clean-params-p (mbe :logic (acl2::bool-fix clean-params-p)
                            :exec clean-params-p))
       (unroll-limit (mbe :logic (nfix unroll-limit)
                          :exec unroll-limit)))
   (cons :vl-simpconfig (list (cons 'compress-p compress-p)
                              (cons 'problem-mods problem-mods)
                              (cons 'clean-params-p clean-params-p)
                              (cons 'unroll-limit unroll-limit))))))