• 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
            • Expression-sizing-minutia
            • Expression-sizing-intro
            • Vl-keyvalue-pattern-collect-array-replacements
            • Vl-assignpattern-positional-replacement
            • Vl-plainarg-exprsize
            • Vl-assignpattern-keyvalue-replacement
            • Vl-keyvalue-pattern-collect-struct-replacements
            • Vl-modulelist-exprsize
            • Vl-expr-assignpattern-extend/truncate
            • Vl-structmemberlist->types
            • Vl-expr-size
            • Vl-expr-selfdetermine-type
            • Vl-assignpattern-multi-replacement
            • Vl-parse-keyval-pattern-struct
            • Vl-plainarglist-exprsize
            • Vl-parse-keyval-pattern-array
            • Vl-warn-about-implicit-extension
            • Vl-assigncontext-size
            • Vl-arguments-exprsize
            • Vl-assignpattern-replacement
            • Vl-packeddimensionlist-exprsize
            • Vl-namedparamvaluelist-exprsize
            • Vl-maybe-delayoreventcontrol-exprsize
            • Vl-repeateventcontrol-exprsize
            • Vl-paramvaluelist-exprsize
            • Vl-maybe-packeddimension-exprsize
            • Vl-delayoreventcontrol-exprsize
            • Vl-namedparamvalue-exprsize
            • Vl-namedarglist-exprsize
            • Vl-enumitemlist-exprsize
            • Vl-packeddimension-exprsize
            • Vl-maybe-paramvalue-exprsize
            • Vl-evatomlist-exprsize
            • Vl-atom-selfdetermine-type
            • Vl-rangelist-exprsize
            • Vl-maybe-gatedelay-exprsize
            • Vl-maybe-datatype-exprsize
            • Vl-gatedelay-exprsize
            • Vl-paramargs-exprsize
            • Vl-namedarg-exprsize
            • Vl-eventcontrol-exprsize
            • Vl-enumbasetype-exprsize
            • Vl-delaycontrol-exprsize
            • Vl-paramvalue-exprsize
            • Vl-maybe-range-exprsize
            • Vl-enumitem-exprsize
            • Vl-range-exprsize
            • Vl-paramdecl-exprsize
            • Vl-paramdecllist-exprsize
            • Vl-maybe-expr-size
            • Vl-evatom-exprsize
            • Vl-vardecllist-exprsize
            • Vl-portdecllist-exprsize
            • Vl-modinstlist-exprsize
            • Vl-initiallist-exprsize
            • Vl-gateinstlist-exprsize
            • Vl-fundecllist-exprsize
            • Vl-assign-exprsize
            • Vl-interfaceport-exprsize
            • Vl-assignlist-exprsize
            • Vl-alwayslist-exprsize
            • Vl-portlist-exprsize
            • Vl-modinst-exprsize
            • Vl-gateinst-exprsize
            • Vl-fundecl-exprsize
            • Vl-vardecl-exprsize
            • Vl-regularport-exprsize
            • Vl-portdecl-exprsize
            • Vl-initial-exprsize
            • Vl-always-exprsize
            • Vl-port-exprsize
            • Vl-lvalue-type
            • Vl-classify-extension-warning-hook
            • Welltyped
            • Vl-castexpr->datatype
            • Vl-expr-size-assigncontext
            • Vl-type-expr-pairs-sum-datatype-sizes
            • Vl-basictype->datatype
            • Vl-expr-replace-assignpatterns
            • Vl-design-exprsize
            • Vl-op-simple-vector-p
            • Vl-expr-val-alist-max-count
            • Vl-expr-has-patterns
            • Vl-exprlist-max-count
            • Vl-unsigned-when-size-zero-lst
            • Vl-type-expr-pairs
            • Append-n
            • Vl-expr-val-alist
            • Vl-datatypelist
          • Occform
          • Oprewrite
          • Expand-functions
          • Delayredux
          • Unparameterization
          • Caseelim
          • Split
          • 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

Expression-sizing

Calculate the widths and types of expressions.

Expression sizing and typing is possibly the most complex, error-prone, and subtle aspect of processing Verilog expressions. One reason for this is that the size and signedness of subexpressions depends upon the other terms in the expressions that contain them. For instance, the result of ((4'd14 + 4'd3) >> 4'd1) might be either 8 or 0, depending on where it is being used. Another reason is just how elaborate the rules for sizing are, and how many corner cases there are.

These issues mean that great care must be taken even when writing simple-looking reductions like constant folding. Moreover, you really need to understand how sizing works if you are going to safely write any code that generates Verilog expressions.

I have put together a gentle expression-sizing-intro which describes Verilog's basic algorithm for how sizes and types are determined. You may also wish to familiarize yourself with the VL notion of well-typed expressions.

The expression-sizing transformation attempts to determine expression sizes and types throughout a module. Prerequisite transformations:

  • portdecl-sign, so we get can signedness right,
  • unparameterization, so there are no paramterized widths, and
  • rangeresolve, so the ranges of wires and selects have been determined.

BOZO follow-hids might also be a prerequisite when we add support for HIDs.

It is valid to run this transformation any time after the above transforms have been run. It is also "idempotent," so it is perfectly valid to run the transform more than once on the same module (e.g., perhaps your subsequent transformation wishes to add some assignment statements, and subsequently wants to determine their sizes.

Subtopics

Expression-sizing-minutia
Specific issues and questions related to the expression sizing and typing of expressions.
Expression-sizing-intro
Introduction to Verilog's expression sizing/typing algorithm.
Vl-keyvalue-pattern-collect-array-replacements
Vl-assignpattern-positional-replacement
Return the list of type/expression pairs to concatenate together to replace a positional assignment pattern.
Vl-plainarg-exprsize
Compute sizes and types of expressions throughout a vl-plainarg-p
Vl-assignpattern-keyvalue-replacement
Return the list of type/expression pairs to concatenate together to replace a key/value assignment pattern.
Vl-keyvalue-pattern-collect-struct-replacements
Vl-modulelist-exprsize
(vl-modulelist-exprsize x ss) maps vl-module-exprsize across a list.
Vl-expr-assignpattern-extend/truncate
Vl-structmemberlist->types
(vl-structmemberlist->types x) maps vl-structmember->type across a list.
Vl-expr-size
Determine sizes for a top-level or self-determined expression.
Vl-expr-selfdetermine-type
Determine the (unpacked) type of an expression.
Vl-assignpattern-multi-replacement
Return the list of type/expression pairs to concatenate together to replace a positional assignment pattern.
Vl-parse-keyval-pattern-struct
Vl-plainarglist-exprsize
Compute sizes and types of expressions throughout a vl-plainarglist-p.
Vl-parse-keyval-pattern-array
Vl-warn-about-implicit-extension
Lint-like warnings about right hand sides being extended.
Vl-assigncontext-size
Vl-arguments-exprsize
Compute sizes and types of expressions throughout a vl-arguments-p
Vl-assignpattern-replacement
Vl-packeddimensionlist-exprsize
Compute sizes and types of expressions throughout a vl-packeddimensionlist-p.
Vl-namedparamvaluelist-exprsize
Compute sizes and types of expressions throughout a vl-namedparamvaluelist-p.
Vl-maybe-delayoreventcontrol-exprsize
Compute sizes and types of expressions throughout a vl-maybe-delayoreventcontrol-p
Vl-repeateventcontrol-exprsize
Compute sizes and types of expressions throughout a vl-repeateventcontrol-p
Vl-paramvaluelist-exprsize
Compute sizes and types of expressions throughout a vl-paramvaluelist-p.
Vl-maybe-packeddimension-exprsize
Compute sizes and types of expressions throughout a vl-maybe-packeddimension-p
Vl-delayoreventcontrol-exprsize
Compute sizes and types of expressions throughout a vl-delayoreventcontrol-p
Vl-namedparamvalue-exprsize
Compute sizes and types of expressions throughout a vl-namedparamvalue-p
Vl-namedarglist-exprsize
Compute sizes and types of expressions throughout a vl-namedarglist-p.
Vl-enumitemlist-exprsize
Compute sizes and types of expressions throughout a vl-enumitemlist-p.
Vl-packeddimension-exprsize
Compute sizes and types of expressions throughout a vl-packeddimension-p
Vl-maybe-paramvalue-exprsize
Compute sizes and types of expressions throughout a vl-maybe-paramvalue-p
Vl-evatomlist-exprsize
Compute sizes and types of expressions throughout a vl-evatomlist-p.
Vl-atom-selfdetermine-type
Vl-rangelist-exprsize
Compute sizes and types of expressions throughout a vl-rangelist-p.
Vl-maybe-gatedelay-exprsize
Compute sizes and types of expressions throughout a vl-maybe-gatedelay-p
Vl-maybe-datatype-exprsize
Compute sizes and types of expressions throughout a vl-maybe-datatype-p
Vl-gatedelay-exprsize
Compute sizes and types of expressions throughout a vl-gatedelay-p
Vl-paramargs-exprsize
Compute sizes and types of expressions throughout a vl-paramargs-p
Vl-namedarg-exprsize
Compute sizes and types of expressions throughout a vl-namedarg-p
Vl-eventcontrol-exprsize
Compute sizes and types of expressions throughout a vl-eventcontrol-p
Vl-enumbasetype-exprsize
Compute sizes and types of expressions throughout a vl-enumbasetype-p
Vl-delaycontrol-exprsize
Compute sizes and types of expressions throughout a vl-delaycontrol-p
Vl-paramvalue-exprsize
Compute sizes and types of expressions throughout a vl-paramvalue-p
Vl-maybe-range-exprsize
Compute sizes and types of expressions throughout a vl-maybe-range-p
Vl-enumitem-exprsize
Compute sizes and types of expressions throughout a vl-enumitem-p
Vl-range-exprsize
Compute sizes and types of expressions throughout a vl-range-p
Vl-paramdecl-exprsize
Compute sizes and types of expressions throughout a vl-paramdecl-p
Vl-paramdecllist-exprsize
Compute sizes and types of expressions throughout a vl-paramdecllist-p.
Vl-maybe-expr-size
Compute sizes and types of expressions throughout a vl-maybe-expr-p
Vl-evatom-exprsize
Compute sizes and types of expressions throughout a vl-evatom-p
Vl-vardecllist-exprsize
Compute sizes and types of expressions throughout a vl-vardecllist-p.
Vl-portdecllist-exprsize
Compute sizes and types of expressions throughout a vl-portdecllist-p.
Vl-modinstlist-exprsize
Compute sizes and types of expressions throughout a vl-modinstlist-p.
Vl-initiallist-exprsize
Compute sizes and types of expressions throughout a vl-initiallist-p.
Vl-gateinstlist-exprsize
Compute sizes and types of expressions throughout a vl-gateinstlist-p.
Vl-fundecllist-exprsize
Compute sizes and types of expressions throughout a vl-fundecllist-p.
Vl-assign-exprsize
Compute sizes and types of expressions throughout a vl-assign-p
Vl-interfaceport-exprsize
Compute sizes and types of expressions throughout a vl-interfaceport-p
Vl-assignlist-exprsize
Compute sizes and types of expressions throughout a vl-assignlist-p.
Vl-alwayslist-exprsize
Compute sizes and types of expressions throughout a vl-alwayslist-p.
Vl-portlist-exprsize
Compute sizes and types of expressions throughout a vl-portlist-p.
Vl-modinst-exprsize
Compute sizes and types of expressions throughout a vl-modinst-p
Vl-gateinst-exprsize
Compute sizes and types of expressions throughout a vl-gateinst-p
Vl-fundecl-exprsize
Compute sizes and types of expressions throughout a vl-fundecl-p
Vl-vardecl-exprsize
Compute sizes and types of expressions throughout a vl-vardecl-p
Vl-regularport-exprsize
Compute sizes and types of expressions throughout a vl-regularport-p
Vl-portdecl-exprsize
Compute sizes and types of expressions throughout a vl-portdecl-p
Vl-initial-exprsize
Compute sizes and types of expressions throughout a vl-initial-p
Vl-always-exprsize
Compute sizes and types of expressions throughout a vl-always-p
Vl-port-exprsize
Compute sizes and types of expressions throughout a vl-port-p
Vl-lvalue-type
Vl-classify-extension-warning-hook
Configurable hook for classifying extension warnings.
Welltyped
Expressions whose sizes and types are sensible.
Vl-castexpr->datatype
Vl-expr-size-assigncontext
Size and resolve assignment patterns in an expression, given the type of its LHS.
Vl-type-expr-pairs-sum-datatype-sizes
Vl-basictype->datatype
Vl-expr-replace-assignpatterns
Rewrite an expression to replace assignment patterns with concatenations.
Vl-design-exprsize
Top-level expression-sizing transform.
Vl-op-simple-vector-p
Vl-expr-val-alist-max-count
Vl-expr-has-patterns
Vl-exprlist-max-count
Vl-unsigned-when-size-zero-lst
Vl-type-expr-pairs
An alist mapping vl-datatype-p to vl-expr-p.
Append-n
Vl-expr-val-alist
An alist mapping anything to vl-expr-p.
Vl-datatypelist
A list of vl-datatype-p objects.