• 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
            • 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
      • Fgl
      • Vwsim
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Transforms

Propagate

Eliminate assignments to simple "intermediate" wires. (UNSOUND)

This is a basic assignment-propagation simplification. The idea is to reduce modules that have lots of intermediate wires by just replacing the wire with its expression. For instance, a module that had assignments like:

assign a1 = ~a2;
assign a2 = ~a3;
assign a3 = ~a4;
assign a4 = ~a5;

Could presumably be propagated into:

assign a1 = ~(~(~(~a5)));

Which we could then reduce in other ways.

This transformation is generally unsound. We aren't really doing any checking to make sure that we are substituting into contexts with compatible widths, etc. We're also relying on the :DIR fields on module instance arguments, which is probably not safe when ports are incorrectly marked as inputs instead of outputs, etc.

Prerequisites: arguments need to be resolved so we can tell directions on module/gate instance ports.

Subtopics

Vl-modulelist-propagate
(vl-modulelist-propagate x limits) maps vl-module-propagate across a list.
Too-hard-to-propagate
Identify wires that are too hard to propagate.
Vl-maybe-driven-by-modinsts
(vl-maybe-driven-by-modinsts x) applies vl-maybe-driven-by-modinst to every member of the list x, and appends together all the resulting lists.
Vl-maybe-driven-by-gateinsts
(vl-maybe-driven-by-gateinsts x) applies vl-maybe-driven-by-gateinst to every member of the list x, and appends together all the resulting lists.
Vl-driven-by-assigns
(vl-driven-by-assigns x) applies vl-driven-by-assign to every member of the list x, and appends together all the resulting lists.
Propagate-limits-p
Limits on the assignments to consider.
Vl-maybe-driven-by-args
Approximately collects the names of wires that are driven by the arguments to a gate/module instance. (unsound)
Candidates-for-propagation
Gather initial candidates for propagation.
Remove-simple-assigns-to
Remove all assignments to these wires (we do this after we've propagated the assignments.
Propagation-sigma
Determine what wires to use for one round of propagation.
Vl-propagation-round
One single round of propagation.
Vl-propagation-fixpoint
Vl-maybe-driven-by-modinst
Approxpimately the wires driven by a module instance (unsound).
Vl-maybe-driven-by-gateinst
Approximately the wires driven by a gate instance.
Vl-module-propagate
Repeatedly propagate assignments in a module.
Propagate-expr-limits-okp
Check whether an expression is simple enough to propagate.
Vl-driven-by-assign
Approximate the wires driven by an assignment.
Vl-design-propagate