		Search-engine friendly clone of the ACL2 documentation.

Transforms

Weirdint-elim

Replace integer literals with X and Z values with concatenations of generated wires.

In this transformation, we replace any vl-weirdint-p atoms with concatenations of the special wires vl-x-value and vl-z-value (for X and Z bits), and one-bit constants 1'b0 and 1'b1 (for 1 and 0 bits). If necessary, we then add instances of the primitive *vl-1-bit-x* and *vl-1-bit-z* modules to drive the X and Z wires.

The net effect is that after this transformation, no modules besides VL_1_BIT_X and VL_1_BIT_Z will contain any weird literals. This transformation is convenient for our conversion to E, where X and Z are not valid literals.

Order Considerations

This must be done after occform, or it will interfere with the creation of Z muxes.

Subtopics

Vl-repeateventcontrol-weirdint-elim
Vl-maybe-delayoreventcontrol-weirdint-elim
Vl-module-add-x/z-wire: Extend mod with a wire declaration for vl-x-wire or vl-z-wire, and a module instance that drives it.
Vl-delayoreventcontrol-weirdint-elim
Vl-plainarglist-weirdint-elim
Vl-namedarglist-weirdint-elim
Vl-modinstlist-weirdint-elim
Vl-initiallist-weirdint-elim
Vl-gateinstlist-weirdint-elim
Vl-eventcontrol-weirdint-elim
Vl-delaycontrol-weirdint-elim
Vl-arguments-weirdint-elim
Vl-evatomlist-weirdint-elim
Vl-assignlist-weirdint-elim
Vl-alwayslist-weirdint-elim
Vl-plainarg-weirdint-elim
Vl-namedarg-weirdint-elim
Vl-module-weirdint-elim
Vl-gateinst-weirdint-elim
Vl-assign-weirdint-elim
Vl-modinst-weirdint-elim
Vl-maybe-expr-weirdint-elim
Vl-initial-weirdint-elim
Vl-evatom-weirdint-elim
Vl-always-weirdint-elim
Vl-weirdint-to-concat
Vl-weirdint-bits-to-exprs: Translate MSB-first bits from a weirdint into expressions, which will become the arguments to a concatenation.
Vl-modulelist-weirdint-elim-aux
Vl-modulelist-weirdint-elim
Vl-design-weirdint-elim: Top-level weirdint-elim transform.
*vl-z-wire-expr*
*vl-x-wire-expr*