• 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
    • Expression-sizing

    Expression-sizing-minutia

    Specific issues and questions related to the expression sizing and typing of expressions.

    There are several ways in which the spec seems unclear or seems to contradict what Verilog implementations do.

    Q1. Does a self-determined operand affect the types of the expressions in which it is involved?

    I ask this question only about the shifting operators, power operator, and conditional operators; the other operators that have self-determined operands are: concatenation and multiple-concatenation operators (which are unambiguously defined to be unsigned in 5.5.1), and logical/reduction operations which are discussed below in Q2.

    What does the spec say? In 5.5.1, we are told The sign and size of any self-determined operand are determined by the operand itself and independent of the remainder of the expression.. From this, and from the discussion of what it means to be a self-determined expression in 5.4.1, I think it is clear that we are supposed to compute the size/type of the subexpression without considering the sizes and types of other operands in the containing expression. But what is not clear is: does the resulting size and type of the subexpression have any bearing on the width/type of the containing expression?

    The width question is unambiguously answered "no" in all cases by Table 5-22. The type question is unambiguously answered "no" by for shift operators in Section 5.1.12, where we are told the right operand is always treated as an unsigned number and has no effect on the signedness of the result. But the type question is not addressed in 5.1.13 for the conditional operator, and while there is some discussion in 5.1.5 about the type of a power operator when its operands are real, the section just refers us to 5.4.1 and 5.5.1 for the integer cases.

    Well, 5.4.1 doesn't really say anything about types, except that it contains Table 5-22 that says which operands are self-determined, and 5.5.1 is back where we started. So the only things we have to go on for the conditional operator and power operator are:

    • R1. The sign and size of any self-determined operand are determined by the operand itself and independent of the remainder of the expression.
    • R2. For nonself-determined operands, the following rules apply:
      • If any operand is real, the result is real
      • If any operand is unsigned, the result is unsigned, regardless of the operator
      • If all operands are signed, the result will be signed, regardless of operator, except when specified otherwise.

    We have already looked at the R1---indeed, we're trying to figure out just what it means by independent. So, we are left with R2, which almost seems to provide a clear answer. In particular, if any operand really means any operand then it is clear that we should include the types of these self-determined operands really do affect the results.

    But there is this damn header, For nonself-determined operands, which suggests this maybe any operand here only refers to any nonself-determined operand. And if this is the case, then we still have no idea what we are supposed to do with conditional and power operations, which have a mixture of self and nonself-determined operands.

    We conclude that the spec is ambiguous and revert to testing with other Verilog implementations to see what they seem to do.

    Conditional Operator

    Verilog-XL and NCVerilog agree that the answer for both of the following expressions are 1111101. This can only happen if the branch operands are being sign-extended. Hence, it seems that these implementations treat the sign of the condition as irrelevant to the result type.

    wire [6:0] y0 = 1'b0 ? 3'sb 100 : 3'sb 101;
    wire [6:0] y1 = 1'sb0 ? 3'sb 100 : 3'sb 101;

    Power Operator

    Unfortunately Verilog-XL does not seem to support the power operator, so we only are able to test with NCVerilog. NCVerilog reports 1984 (-64) as the result for both of the following,

    wire [10:0] p2 = (3'sb100 ** 2'b11);
    wire [10:0] p3 = (3'sb100 ** 2'sb11);

    Hence it seems that the type of the exponent is not relevant to the result type. If it were, then in p2 we would have to zero-extend the base to 4, rather than sign-extend it to -4, and the result for p2 would be 64 instead of 1984.

    Shift Operators

    For good measure we also tried a shift-operator, even though we think the spec is clear here.

    wire [4:0] v1 = 1'sd 1 >> 1'b0;

    Here, ignoring the sign of the right-hand side would produce 11111, since the left-hand side would be sign-extended to 5 bits and then unchanged by the shift. On the other hand, if we allow the right-hand side to play a role, then the result is unsigned and we would zero-extend the left-hand side instead, producing a final result of 1. Both Verilog-XL and NCVerilog get 11111, which we think is correct.

    Conclusions

    The implementations seem to agree that the types of these operands should not matter. Since we think the spec is vague and does not say one way or another, we mimick their behavior. However, we also issue warnings when we encounter one of these operands with an unsigned self-determined operand and signed nonself-determined operands, since this is a case that other implementations might be confused about. See vl-expr-typedecide-aux for details.

    Q2. What is the type of a reduction or logical operation?

    The ambiguity in Q1 is also a problem for:

    • the logical operators (&&, ||, and !) and
    • the reduction operators (&, ~&, |, ~|, ^, ~^, and ^~).

    In these cases, there are no nonself-determined operators that R2 might allow us to use to get an answer. 5.1.11 (reduction operators) doesn't provide any help, and neither does 5.1.9 (logical operators). So, we are again reduced to testing. Here are some simple cases:

    wire [4:0] q0 = | 17;
    wire [4:0] q1 = ! 3'sd 0;
    wire [4:0] q2 = & 5'sb11111;
    wire [4:0] q3 = 3 && 5;

    In Verilog-XL and NCVerilog, all of these expressions produce 00001, meaning that in each case they are being zero-extended instead of sign extended. This is somewhat further evidence that R2 is not supposed to apply to self-determined operands.

    Some internet searching revealed Issue 1072 at the EDA.org "mantis" site, which seems to suggests that the spec is wrong and should say reduction operators and logical operators produce unsigned 1-bit values.

    We therefore treat these as unsigned 1-bit values, but we take special care to generate warnings if this treatment affects the final signedness of an expression. See vl-expr-typedecide for details.

    Q3. What does shifting by a negative number mean?

    This question is silly because it seems that the Verilog specification somewhat clearly says in 5.1.12 that the right operand is always treated as an unsigned number.

    Unfortunately, Verilog-XL and NCVerilog produce different results for:

    wire [9:0] v0 = 10'b 0000_11_0000 >> ( 2'sd 0 + 1'sd 1 );

    In Verilog-XL, the answer is 0001_10_0000, i.e., the result appears to have been left-shifted by one place; in NCVerilog, the answer is 0000_00_0110, i.e., the result appears to have been right-shifted by 3 places.

    In both cases, the right-hand side seems to indeed be self-determined and yields 2'sd 3. And, since we are supposed to "treat the right-hand side as an unsigned number," it seems like we should shift the left-hand side by 3 places to the right like NCVerilog.

    I found some discussion from the IEEE 1364 Behavioral Task Force Mailing List Archives, specifically a signed shift errata? thread started by Stuart Sutherland on Monday, July 19, 1999, the followup to which suggests that Verilog-XL is in the wrong and that this is one area where NCVerilog was designed to match the Verilog-2005 standard instead of Verilog-XL.

    We follow NCVerilog's behavior, but issue a warning if we see a signed right-hand side (unless it is a signed constant whose sign-bit is zero) so that the difference does not matter. See vl-expr-typedecide-aux for details.