• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
        • Warnings
        • Primitives
        • Use-set
        • Syntax
        • Getting-started
        • Utilities
        • Loader
        • Transforms
          • Expression-sizing
          • Occform
          • Oprewrite
          • Expand-functions
          • Delayredux
          • Unparameterization
          • Caseelim
          • Split
          • Selresolve
          • Weirdint-elim
          • Vl-delta
          • Replicate-insts
          • Rangeresolve
          • Propagate
            • Vl-modulelist-propagate
            • Too-hard-to-propagate
            • Vl-maybe-driven-by-modinsts
            • Vl-maybe-driven-by-gateinsts
            • Vl-driven-by-assigns
            • Propagate-limits-p
              • Propagate-limits
              • Make-propagate-limits
              • Change-propagate-limits
              • Make-honsed-propagate-limits
              • Honsed-propagate-limits
              • Propagate-limits->max-ops
            • Vl-maybe-driven-by-args
            • Candidates-for-propagation
            • Remove-simple-assigns-to
            • Propagation-sigma
            • Vl-propagation-round
            • Vl-propagation-fixpoint
            • Vl-maybe-driven-by-modinst
            • Vl-maybe-driven-by-gateinst
            • Vl-module-propagate
            • Propagate-expr-limits-okp
            • Vl-driven-by-assign
            • Vl-design-propagate
          • Clean-selects
          • Clean-params
          • Blankargs
          • Inline-mods
          • Expr-simp
          • Trunc
          • Always-top
          • Gatesplit
          • Gate-elim
          • Expression-optimization
          • Elim-supplies
          • Wildelim
          • Drop-blankports
          • Clean-warnings
          • Addinstnames
          • Custom-transform-hooks
          • Annotate
          • Latchcode
          • Elim-unused-vars
          • Problem-modules
        • Lint
        • Mlib
        • Server
        • Kit
        • Printer
        • Esim-vl
        • Well-formedness
      • Sv
      • Vwsim
      • Fgl
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Propagate

Propagate-limits-p

Limits on the assignments to consider.

(propagate-limits-p x) is a defaggregate of the following fields.

  • max-ops — Invariant (maybe-natp max-ops).

Source link: propagate-limits-p

We put this in an aggregate just to make it easy to extend.

Subtopics

Propagate-limits
Raw constructor for propagate-limits-p structures.
Make-propagate-limits
Constructor macro for propagate-limits-p structures.
Change-propagate-limits
A copying macro that lets you create new propagate-limits-p structures, based on existing structures.
Make-honsed-propagate-limits
Constructor macro for honsed propagate-limits-p structures.
Honsed-propagate-limits
Raw constructor for honsed propagate-limits-p structures.
Propagate-limits->max-ops
Access the max-ops field of a propagate-limits-p structure.