Search-engine friendly clone of the
ACL2 documentation
.
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-limits-p
Propagate-limits->max-ops
Access the
max-ops
field of a
propagate-limits-p
structure.