• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • 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-simpconfig

    Vl-simpconfig->elab-limit

    Get the elab-limit field from a vl-simpconfig.

    Signature
    (vl-simpconfig->elab-limit x) → elab-limit
    Arguments
    x — Guard (vl-simpconfig-p x).
    Returns
    elab-limit — Type (natp elab-limit).

    This is an ordinary field accessor created by defprod.

    Definitions and Theorems

    Function: vl-simpconfig->elab-limit$inline

    (defun vl-simpconfig->elab-limit$inline (x)
      (declare (xargs :guard (vl-simpconfig-p x)))
      (declare (xargs :guard t))
      (let ((__function__ 'vl-simpconfig->elab-limit))
        (declare (ignorable __function__))
        (mbe :logic
             (b* ((x (and t x)))
               (nfix (std::da-nth 5 (cdr x))))
             :exec (std::da-nth 5 (cdr x)))))

    Theorem: natp-of-vl-simpconfig->elab-limit

    (defthm natp-of-vl-simpconfig->elab-limit
      (b* ((elab-limit (vl-simpconfig->elab-limit$inline x)))
        (natp elab-limit))
      :rule-classes :type-prescription)

    Theorem: vl-simpconfig->elab-limit$inline-of-vl-simpconfig-fix-x

    (defthm vl-simpconfig->elab-limit$inline-of-vl-simpconfig-fix-x
      (equal (vl-simpconfig->elab-limit$inline (vl-simpconfig-fix x))
             (vl-simpconfig->elab-limit$inline x)))

    Theorem: vl-simpconfig->elab-limit$inline-vl-simpconfig-equiv-congruence-on-x

    (defthm
     vl-simpconfig->elab-limit$inline-vl-simpconfig-equiv-congruence-on-x
     (implies (vl-simpconfig-equiv x x-equiv)
              (equal (vl-simpconfig->elab-limit$inline x)
                     (vl-simpconfig->elab-limit$inline x-equiv)))
     :rule-classes :congruence)