• 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
          • Vl-module
          • Vl-vardecl
          • Expressions
          • Vl-fundecl
          • Vl-assign
          • Vl-gateinst
          • Vl-modinst
          • Vl-commentmap
          • Vl-portdecl
          • Vl-taskdecl
          • Vl-design
          • Vl-interface
          • Vl-plainarglist->exprs
          • Vl-taskdecllist->names
          • Vl-fundecllist->names
          • Vl-package
          • Vl-port
          • Vl-udp
          • Vl-paramdecl
          • Vl-genelement
          • Vl-cycledelayrange
          • Vl-namedarg
          • Vl-sort-blockitems-aux
          • Vl-distitem
          • Vl-gatedelay
          • Vl-repetition
          • Vl-typedef
          • Vl-range
          • Vl-gatestrength
          • Vl-program
          • Vl-config
          • Vl-always
          • Vl-datatype-update-dims
          • Vl-import
          • Vl-enumbasetype
          • Vl-repeateventcontrol
          • Vl-paramargs
          • Vl-initial
          • Vl-eventcontrol
          • Vl-udpsymbol-p
          • Vl-maybe-range
          • Vl-maybe-nettypename
          • Vl-maybe-gatestrength
          • Vl-maybe-gatedelay
          • Vl-maybe-delayoreventcontrol
          • Vl-alias
          • Maybe-string-fix
          • Vl-maybe-packeddimension
          • Vl-fwdtypedef
          • Vl-evatom
          • Vl-packeddimension-p
          • Vl-maybe-udpsymbol
          • Vl-maybe-module
          • Vl-maybe-direction
          • Vl-maybe-datatype
          • Vl-maybe-cstrength
          • Vl-direction-p
          • Vl-arguments
          • Vl-maybe-design
          • Vl-udpline
          • Vl-exprdist
          • Vl-context1
          • Vl-genvar
          • Vl-enumitem
          • Vl-datatype-update-udims
          • Vl-datatype-update-pdims
          • Vl-modelement
          • Vl-udpedge
          • Vl-delaycontrol
          • Vl-context
          • Vl-sort-blockitems
          • Vl-distweighttype-p
          • Vl-ctxelement->loc
          • Vl-blockitem
          • Vl-vardecllist
          • Vl-module->ifports
          • Vl-modelement->loc
          • Vl-ctxelement
          • Vl-coretypename-p
          • Vl-packeddimensionlist
          • Vl-modelementlist->genelements
          • Vl-gatetype-p
          • Vl-paramdecllist
          • Vl-lifetime-p
          • Vl-datatype->udims
          • Vl-datatype->pdims
          • Vl-timeunit-p
          • Vl-repetitiontype-p
          • Vl-port->name
          • Vl-importlist
          • Vl-genelement->loc
          • Vl-delayoreventcontrol
          • Vl-cstrength-p
          • Statements
            • Vl-stmt
              • Vl-assignstmt
              • Vl-stmt-p
              • Vl-blockstmt
              • Vl-forstmt
              • Vl-casestmt
                • Case-statement-problems
                  • Make-vl-casestmt
                  • Vl-casestmt->casetype
                  • Vl-casestmt->caselist
                  • Vl-casestmt->test
                  • Vl-casestmt->default
                  • Vl-casestmt->check
                  • Vl-casestmt->atts
                  • Change-vl-casestmt
                • Vl-stmt-case
                • Vl-ifstmt
                • Vl-waitstmt
                • Vl-repeatstmt
                • Vl-eventtriggerstmt
                • Vl-whilestmt
                • Vl-timingstmt
                • Vl-enablestmt
                • Vl-deassignstmt
                • Vl-disablestmt
                • Vl-stmt-equiv
                • Vl-foreverstmt
                • Vl-stmt-kind
                • Vl-nullstmt
                • Vl-returnstmt
                • Vl-stmt-fix
                • Vl-stmt-count
              • Vl-stmtlist
              • Vl-caselist
            • Vl-udpentry-p
            • Vl-packeddimension-fix
            • Vl-nettypename-p
            • Vl-portdecllist
            • Vl-port->loc
            • Vl-enumbasekind-fix
            • Vl-arguments->args
            • Vl-taskdecllist
            • Vl-portlist
            • Vl-importpart-p
            • Vl-importpart-fix
            • Vl-fundecllist
            • Vl-blockstmt-p
            • Vl-assignlist
            • Vl-alwaystype-p
            • Vl-typedeflist
            • Vl-syntaxversion-p
            • Vl-randomqualifier-p
            • Vl-modinstlist
            • Vl-gateinstlist
            • Vl-blockitemlist
            • Vl-udptable
            • Vl-udplist
            • Vl-udpentrylist
            • Vl-programlist
            • Vl-paramvaluelist
            • Vl-packagelist
            • Vl-namedparamvaluelist
            • Vl-namedarglist
            • Vl-modulelist
            • Vl-modportlist
            • Vl-modport-portlist
            • Vl-interfacelist
            • Vl-initiallist
            • Vl-genvarlist
            • Vl-fwdtypedeflist
            • Vl-evatomlist
            • Vl-enumitemlist
            • Vl-distlist
            • Vl-configlist
            • Vl-alwayslist
            • Vl-aliaslist
            • Vl-regularportlist
            • Vl-rangelist-list
            • Vl-rangelist
            • Vl-paramdecllist-list
            • Vl-modelementlist
            • Vl-maybe-range-list
            • Vl-interfaceportlist
            • Vl-argumentlist
            • Data-types
          • Getting-started
          • Utilities
          • Loader
          • Transforms
          • Lint
          • Mlib
          • Server
          • Kit
          • Printer
          • Esim-vl
          • Well-formedness
        • Sv
        • Fgl
        • Vwsim
        • Vl
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Vl-casestmt
    • Caseelim

    Case-statement-problems

    The official behavior of case, casez and casex is problematic with respect to X and Z values.

    Generally speaking, Verilog's behavioral modeling constructs are rife with problems when it comes to the handling of unknown and high-impedence values. Even the basic if statement treats X values as false, which is deeply troubling—if we don't know what some value is, we certainly should not simply assume it is false.

    Verilog's case, casex, and casez statements have especially bad behavior with regards to X and Z values.

    For basic case statements, each match is compared against the test expression using case-equality === instead of ordinary equality ==. This allows you to match precisely against X and Z, which can easily lead to an improper, non-conservative treatment of X.

    The fancier casez and casex statements are especially badly behaved. At first glance these statements seem pretty convenient. For instance, in casez you are told that you can use Z or (equivalently) ? as a pattern-matching character. You might look at a code fragment like this:

    casez (inst)
      5'b00001: out = a + b;
      5'b0001?: out = a - b;
      5'b001??: out = a & b;
      5'b01???; out = a | b;
      default:  out = 16'hXXXX;
    endcase

    And think—wow, that looks nice. You might expect that the second pattern here, 5'b0001?, will match:

    • 00010
    • 00011
    • 0001X
    • 0001Z

    And you're right. Unfortunately, what you probably did not expect, is that this pattern will also match many other values, like:

    • Z0010
    • ZZ010
    • ZZ0Z0
    • ZZZZZ

    And so on. This is because Z values are treated as wildcards not only in your pattern, but also in the data itself, which is terrible and makes no sense at all.

    The casex statement is even worse. Here, any X or Z values in the data will match anything you've written in your pattern. So, for instance,

    casex (inst)
      5'b00001: out = GOOD;
      default:  out = BAD;
    endcase

    Will, quite unexpectedly, produce GOOD for instructions such as XXXXX, ZZZZZ, and so on.