• 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
        • Lint
          • Vl-lintconfig-p
          • Lucid
          • Skip-detection
          • Vl-lintresult-p
          • Lint-warning-suppression
          • Condcheck
            • Vl-modulelist-condcheck
            • Vl-condcheck-fix
            • Vl-expr-condcheck
            • Vl-condcheck-negate
            • Vl-module-condcheck
            • Vl-exprctxalist-condcheck
            • Vl-design-condcheck
          • Selfassigns
          • Leftright-check
          • Dupeinst-check
          • Oddexpr-check
          • 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
  • Lint

Condcheck

Check for ?:-expressions with strange conditions.

This is a heuristic for generating warnings. We look for things like the following, except that we target the ?: operator instead of if statements.

if A { ... }
else if B { ... }
else if A { ... }   // already checked A above, so this is unreachable
else if C { ... }
else ...

And also things like:

if A { ... }
else if B { ... }
else if !A { ... }   // already checked A above, so this is just true
else if C { ... }
else ...

And for if (constant) {...}.

All of this could be adapted to if statements too, but we target the ?: operator because we care a lot less about procedural code (like test benches) than we do about the actual hardware modules. Note that the qmarksize-check can also be used for some additional checking on ?: operators, but it tries to identify a different class of problems.

Since this is just a heuristic and it is completely unrelated to soundness, we feel justified in doing a couple of seemingly unsound things. In particular, we basically ignore widths of test expressions and treat ! and ~ as equivalent. We also treat ^ as != and ~^ as ==. This is completely wrong in general, but it makes sense if you assume that the tests are all going to be one-bit wide.

This check has no prerequisites and can in principle be run at any time. But it is probably best to run it very early before throwing things out, and it should probably be run before oprewrite, which screws around with conditional expressions, and also before things like expression splitting which would get rid of the nested branches.

Subtopics

Vl-modulelist-condcheck
(vl-modulelist-condcheck x) maps vl-module-condcheck across a list.
Vl-condcheck-fix
Canonicalize an test expression for condcheck.
Vl-expr-condcheck
Look for strange conditions throughout an expression.
Vl-condcheck-negate
Smartly negate a canonicalized expression.
Vl-module-condcheck
(vl-module-condcheck x) carries our our condcheck on all the expressions in a module, and adds any resulting warnings to the module.
Vl-exprctxalist-condcheck
(vl-exprctxalist-condcheck x) extends vl-expr-condcheck across an vl-exprctxalist-p.
Vl-design-condcheck