		Search-engine friendly clone of the ACL2 documentation.

Expression-sizing

Expression-sizing-intro

Introduction to Verilog's expression sizing/typing algorithm.

Sizing expressions in Verilog is a two-phase process.

We inspect the expression to determine what final size and signedness it should have. To a first approximation: the final size of the expression will be the maximum size of any of its operands, and the final signedness will be unsigned unless all operands are signed. But the real story involves many operand-specific rules and corner cases.
We then "propagate" the final size and signedness down to the operands. Approximately true: if the final signedness is signed, then we globally sign-extend every operand to the final width; if the final signedness is unsigned, we instead always zero-extend the operands. After this extension, the operands all agree on a size, and the inputs to operators like + will have the same width, and the output of the operator will also have this same width. But again, the real story has many rules and corner cases to cover.

Stop! Carefully read the above steps again. Understanding the two phases is a critical first step to making any sense of the rules.

Let us now begin making these steps more precise.

Final-Size Computation

First, the claim that "final size of the expression is the maximum size of any of its operands" is basically true for expressions like a + b. But it is completely wrong for, e.g., |foo or foo == bar, which basically produce one-bit wide answers. Another example is concatenations like {foo, bar} where the width should be the sum of its arguments widths.

The actual rules for computing the final width of an expression are given in Table 5-22 of the Verilog spec, which we now reproduce:

Expression                     Bit Length         Notes
-----------------------------------------------------------------------------
Unsized constants              "Same as integer"  (see ** below)
Sized constants                As given
i [+ - * / % & | ^ ^~ ~^] j    max{L(i),L(j)}
[+ - ~] i                      L(i)
i [=== !== == != > >= < <=] j  1 bit              i,j sized to max(L(i),L(j))
i [&& ||] j                    1 bit              i,j self-determined
[& ~& | ~| ^ ~^ ^~ !] i        1 bit              i self-determined
i [>> << ** >>> <<<] j         L(i)               j self-determined
i ? j : k                      max(L(j),L(k))     i self-determined
{i, ..., j}                    L(i)+...+L(j)      all self-determined
{i {j, ..., k}}                i*(L(j)+...+L(k))  all self-determined
-----------------------------------------------------------------------------

(**) What does "same as integer" mean? From Section 4.8: Verilog implementations may limit the size of integer variables. The limit must be at least 32 bits, but is not otherwise unconstrained. Hence, expressions involving unsized constants may have implementation-dependent sizes (and can in fact have implementation-dependent results).

VL acts like a 32-bit implementation, so effectively any unsized constant is treated as if it has size 32. I historically tried to directly support abstract "integer-sized" expressions so that we could warn about expressions whose behavior might be implementation-dependent. But I eventually decided that this approach overly complicated the sizing code. Today, the VL lexer automatically treats unsized constants as if they were 32 bits so the whole matter of "how large is integer-size?" is effectively settle a priori. But the lexer also marks any unsized constants with the :wasunsized property, which allows us to still carry out this compatibility checking.

At any rate, the "bit length" column in the above table gives an almost full story about how to determine the finalwidth of an expression. But as a final twist, when assignment statements are sized, the bit-length of the left-hand side of the assignment also plays a role in the finalwidth computation. Essentially, the finalwidth of rhs in assign lhs = rhs is max{L(lhs), L(rhs)}.

Our main function for computing the desired finalwidth of an expression is vl-expr-selfsize.

Signedness Computation

The above claim that "the final signedness will be unsigned unless all operands are signed" is basically true for expressions like a + b. For instance, if the full expression is (3 + 4) + 0, then its final signedness is signed because all of its operands are signed. On the other hand, if we change this to (3 + 4) + 1'b0, then the final signedness is unsigned because 1'b0 is unsigned.

The Verilog rules for signedness are covered in Section 5.5.1 and 5.5.4. We summarize these rules here:

Constants are either signed or unsigned depending upon how they are written in the source code, e.g., plain numbers like 5 are signed, and otherwise the signedness is controlled by the base specifier, e.g., 10'b0 is unsigned but 10'sb0 is signed. (All of this is handled by our lexer and built into the :origtype field of our vl-constint-p and vl-weirdint-p atomguts.)
Bit-selects, part-selects, concatenations (and presumably multiple concatenations), and comparison results (e.g., from a == b) are always unsigned.
Reals converted to integers are signed (but we don't handle reals, so this doesn't affect us).
The signedness of self-determined subexpressions is determined by the subexpression itself, and doesn't depend on any other terms from the expression, e.g., { 3, 1'b0 } is a concatenation with one signed and one unsigned subexpression.
For nonself-determined operands, if any operand is real the result is real; if any operand is unsigned the result is unsigned; otherwise all operands are signed and the result is "signed, regardless of operator, except when specified otherwise." (This is particularly unclear).

Another rule is found in 5.1.12, which says the right-hand side of a shift is always treated as unsigned.

Some additional technical questions and investigations may be found in expression-sizing-minutia.

In VL, our main function for computing the final signedness of an expression is vl-expr-typedecide.

Propagating the Context

BOZO document this.