• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
      • Transforms
      • Lint
        • Vl-lintconfig-p
        • Lucid
        • Skip-detection
        • Vl-lintresult-p
        • Lint-warning-suppression
        • Condcheck
        • Selfassigns
        • Leftright-check
        • Dupeinst-check
        • Oddexpr-check
          • Vl-modulelist-oddexpr-check
          • *vl-odd-binops-table*
          • Vl-warn-odd-binary-expression-main
          • Vl-expr-probable-selfsize
          • Vl-odd-binop-class
          • Vl-module-oddexpr-check
          • Vl-oddexpr-check
          • Vl-exprctxalist-oddexpr-check
          • Vl-design-oddexpr-check
          • Vl-warn-odd-binary-expression
          • Vl-pp-oddexpr-details
          • *fake-modelement*
        • Remove-toohard
        • Qmarksize-check
        • Portcheck
        • Duplicate-detect
        • Vl-print-certain-warnings
        • Duperhs-check
        • *vl-lint-help*
        • Lint-stmt-rewrite
        • Drop-missing-submodules
        • Check-case
        • Drop-user-submodules
        • Check-namespace
        • Vl-lint
      • Mlib
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Oddexpr-check

*vl-odd-binops-table*

The actual intelligence behind the oddexpr check.

This is the main table that controls whether we warn about certain combinations of binary operators. If you want to NOT issue a warning about a particular combination of operators, then just leave it out of the table.

The keys in the table have the form (outer-class . inner-class). For details about these classes see vl-odd-binop-class. Loosely speaking, a key like (:shift-class . :plus-class) matches expressions of the following forms:

1. (a + b) << c
2. a << (b + c)

Whereas a key like (:plus-class . :shift-class) would match expressions of the following forms:

1. (a << b) + c
2. a + (b << c)

In other words, the inner-op is the "sub" operation, and the outer-op is the "top" operation.

Note that we never have keys where the outer-op has a higher precedence than the inner operation, such as (:plus-class . :shift-class). Why not?

Because of the precedence rules, a << b + c gets parsed as a << (b + c). In other words, the only reason we'd ever get an expression that matches (:plus-class . :shift-class) is that the user explicitly put in their own parens around the shift operator. If they've done that, then they are explicitly saying what precedence they want, and there's no chance they are going to be surprised by Verilog's precedence rules. This same reasoning holds for any combination of operators where the outer op is higher precedence than the inner op.

NOTE see the source code for this table for additional comments giving motivation for these actions, etc.

Definition: *vl-odd-binops-table*

(defconst *vl-odd-binops-table*
  '(((:shift-class . :plus-class)
     . :check-precedence)
    ((:bitand-class . :plus-class)
     . :check-precedence)
    ((:xor-class . :plus-class)
     . :check-precedence)
    ((:bitor-class . :plus-class)
     . :check-precedence)
    ((:logand-class . :plus-class)
     . :check-type)
    ((:logor-class . :plus-class)
     . :check-type)
    ((:plus-class . :minus-class)
     . :check-precedence-plusminus)
    ((:shift-class . :minus-class)
     . :check-precedence)
    ((:bitand-class . :minus-class)
     . :check-precedence)
    ((:xor-class . :minus-class)
     . :check-precedence)
    ((:bitor-class . :minus-class)
     . :check-precedence)
    ((:logand-class . :minus-class)
     . :check-type)
    ((:logor-class . :minus-class)
     . :check-type)
    ((:shift-class . :shift-class)
     . :check-precedence)
    ((:bitand-class . :shift-class)
     . :check-precedence)
    ((:xor-class . :shift-class)
     . :check-precedence)
    ((:bitor-class . :shift-class)
     . :check-precedence)
    ((:logand-class . :shift-class)
     . :check-type)
    ((:logor-class . :shift-class)
     . :check-type)
    ((:rel-class . :rel-class)
     . :check-type)
    ((:cmp-class . :rel-class)
     . :check-type)
    ((:bitand-class . :rel-class)
     . :check-type-unless-topargs-boolean)
    ((:xor-class . :rel-class)
     . :check-type)
    ((:bitor-class . :rel-class)
     . :check-type-unless-topargs-boolean)
    ((:cmp-class . :cmp-class)
     . :check-type)
    ((:bitand-class . :cmp-class)
     . :check-type-unless-topargs-boolean)
    ((:xor-class . :cmp-class)
     . :check-type)
    ((:bitor-class . :cmp-class)
     . :check-type-unless-topargs-boolean)
    ((:xor-class . :bitand-class)
     . :check-precedence)
    ((:logand-class . :bitand-class)
     . :check-type-unless-topargs-boolean)
    ((:logor-class . :bitand-class)
     . :check-type-unless-topargs-boolean)
    ((:logand-class . :xor-class)
     . :check-type)
    ((:logor-class . :xor-class)
     . :check-type)
    ((:logand-class . :bitor-class)
     . :check-type-unless-topargs-boolean)
    ((:logor-class . :bitor-class)
     . :check-type-unless-topargs-boolean)
    ((:logor-class . :logand-class)
     . :check-precedence)))

Definition: *vl-odd-binops-table*

(defconst *vl-odd-binops-table*
  '(((:shift-class . :plus-class)
     . :check-precedence)
    ((:bitand-class . :plus-class)
     . :check-precedence)
    ((:xor-class . :plus-class)
     . :check-precedence)
    ((:bitor-class . :plus-class)
     . :check-precedence)
    ((:logand-class . :plus-class)
     . :check-type)
    ((:logor-class . :plus-class)
     . :check-type)
    ((:plus-class . :minus-class)
     . :check-precedence-plusminus)
    ((:shift-class . :minus-class)
     . :check-precedence)
    ((:bitand-class . :minus-class)
     . :check-precedence)
    ((:xor-class . :minus-class)
     . :check-precedence)
    ((:bitor-class . :minus-class)
     . :check-precedence)
    ((:logand-class . :minus-class)
     . :check-type)
    ((:logor-class . :minus-class)
     . :check-type)
    ((:shift-class . :shift-class)
     . :check-precedence)
    ((:bitand-class . :shift-class)
     . :check-precedence)
    ((:xor-class . :shift-class)
     . :check-precedence)
    ((:bitor-class . :shift-class)
     . :check-precedence)
    ((:logand-class . :shift-class)
     . :check-type)
    ((:logor-class . :shift-class)
     . :check-type)
    ((:rel-class . :rel-class)
     . :check-type)
    ((:cmp-class . :rel-class)
     . :check-type)
    ((:bitand-class . :rel-class)
     . :check-type-unless-topargs-boolean)
    ((:xor-class . :rel-class)
     . :check-type)
    ((:bitor-class . :rel-class)
     . :check-type-unless-topargs-boolean)
    ((:cmp-class . :cmp-class)
     . :check-type)
    ((:bitand-class . :cmp-class)
     . :check-type-unless-topargs-boolean)
    ((:xor-class . :cmp-class)
     . :check-type)
    ((:bitor-class . :cmp-class)
     . :check-type-unless-topargs-boolean)
    ((:xor-class . :bitand-class)
     . :check-precedence)
    ((:logand-class . :bitand-class)
     . :check-type-unless-topargs-boolean)
    ((:logor-class . :bitand-class)
     . :check-type-unless-topargs-boolean)
    ((:logand-class . :xor-class)
     . :check-type)
    ((:logor-class . :xor-class)
     . :check-type)
    ((:logand-class . :bitor-class)
     . :check-type-unless-topargs-boolean)
    ((:logor-class . :bitor-class)
     . :check-type-unless-topargs-boolean)
    ((:logor-class . :logand-class)
     . :check-precedence)))