• 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
            • Vl-modulelist-split
            • Vl-plainarg-split
            • Vl-assign-split
            • Vl-expr-split
            • Vl-arguments-split
            • Vl-plainarglist-split
            • Vl-gateinstlist-split
            • Vl-modinstlist-split
            • Vl-assignlist-split
            • Vl-module-split
            • Vl-modinst-split
            • Vl-gateinst-split
            • Vl-nosplitlist-p
            • Vl-nosplit-p
            • Vl-design-split
            • *vl-tmp-wire-atts*
          • Selresolve
          • Weirdint-elim
          • Vl-delta
          • Replicate-insts
          • Rangeresolve
          • 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

Split

Split up expressions by generating new wires.

The basic idea of this transformation is to introduce temporary variables for sub-expressions, e.g., we might split up:

assign w = a + b * c + d;

into a series of simpler assignments, e.g.,

assign t1 = b * c;
assign t2 = a + t1;
assign w = t2 + d;

Almost true: we split up expressions until they involve either 0 or 1 operations. The twist is that we don't split up expressions that consist of "mere wiring", e.g., concatenation and bit- or part-selects. More precisely, we don't split up expressions that are already atomic or sliceable; see expr-slicing.

Splitting up expressions involves creating new wire declarations and assignments to those wires. Sometimes the new modules are much bigger than the old modules. We have seen cases where tens of thousands of new wires are introduced. In fact, this transform was one of our initial motivations for name factories.

Context. I usually think of expression splitting as a kind of preprocessing step that leads toward occform; occform replaces simple assignments (e.g., like those to the temporary wires above) with module instances, but can't deal with complex expressions.

Prerequisites. We expect that argresolve has been run and that expression-sizing has already been done. Unsized expressions or named arguments will generally lead to fatal warnings being added to the module.

Soundness Concerns. If submodule ports are mislabeled, we might end up splitting up an input to a module instance that has backflow. That is, we could do somethign like this:

submod foo ( ..., .i(a + b), ...);
  --->
wire[3:0] tmp = a + b;
submod foo ( ..., .i(tmp), ...);

And if foo drives i, then we might end up with tmp being X sometimes. Worse would be if the expression was somethign like a ? b : 1'bz, in which case the submodule could actually end up putting out a value onto tmp.

I don't really think this is a problem. I think we're saved because, since a new, fresh temporary wire is going to be used, whether or not that temporary is driven from both sides isn't really relevant. It can't be used anywhere else in the module or affect anything except for exactly this port.

Subtopics

Vl-modulelist-split
(vl-modulelist-split x) maps vl-module-split across a list.
Vl-plainarg-split
Maybe split up an argument to a gate/module instances.
Vl-assign-split
Split up assignments with complex right-hand sides.
Vl-expr-split
Split up complex subexpressions throughout an expression.
Vl-arguments-split
Vl-plainarglist-split
Vl-gateinstlist-split
Vl-modinstlist-split
Vl-assignlist-split
Vl-module-split
Split up complex expressions throughout a module's assignments, module instances, and gate instances.
Vl-modinst-split
Vl-gateinst-split
Vl-nosplitlist-p
(vl-nosplitlist-p x) recognizes lists where every element satisfies vl-nosplit-p.
Vl-nosplit-p
Recognize an expression that is may as well be atomic for the purposes of split.
Vl-design-split
Top-level split transform.
*vl-tmp-wire-atts*