• 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
            • Sd-problem-p
            • Sd-keylist-find-skipped
            • Sd-keylist->indicies
            • Sd-key-p
            • Sd-patalist-compare
            • Sd-analyze-ctxexprs
            • Sd-problemlist-p
            • Sd-patalist-p
            • Sd-keygen
            • Sd-patalist
            • Sd-keylist-p
            • Sd-analyze-modulelist
            • Sd-analyze-module-aux
            • Sd-analyze-module
            • Sd-pp-problem-long
            • Sd-analyze-modulelist-aux
            • Sd-problem-score
            • Sd-pp-problem-header
            • Sd-analyze-design
            • Sd-problem->
            • Sd-pp-problem-brief
            • Sd-pp-problemlist-long
            • Sd-pp-problemlist-brief
            • Sd-natlist-linear-increments-p
            • Sd-keylist-linear-increments-p
          • Vl-lintresult-p
          • Lint-warning-suppression
          • 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

Skip-detection

We try to detect missing signals from expressions.

Related wires often have similar names, e.g., in one module we found wires with names like bcL2RB0NoRtry_P, bcL2RB1NoRtry_P, and so on, up to bcL2RB7NoRtry_P. Such signals might sometimes be combined later on, e.g., we later found:

assign bcL2NoRtry_P = bcL2RB7NoRtry_P | bcL2RB6NoRtry_P
                    | bcL2RB5NoRtry_P | bcL2RB4NoRtry_P
                    | bcL2RB3NoRtry_P | bcL2RB2NoRtry_P
                    | bcL2RB1NoRtry_P | bcL2RB0NoRtry_P;

Skip detection pertains to expressions like the above. In short, it would be pretty odd if bcL2RB4NoRtry_P been omitted ("skipped") in the above expression, or if say bcL2RB3NoRtry_P occurred more than once. We try to detect such situations.

Note that some expressions might involve more than one group of these kind of signals. For instance, we found:

assign bcNxtWCBEntSrc_P =
   bcDataSrcLd_P ? ({3{bcWCB0DBSYQual_P}} & bcWCB0Ent_P)
                 | ({3{bcWCB1DBSYQual_P}} & bcWCB1Ent_P)
                 | ({3{bcWCB2DBSYQual_P}} & bcWCB2Ent_P)
                 | ({3{bcWCB3DBSYQual_P}} & bcWCB3Ent_P)
                 | ({3{bcWCB4DBSYQual_P}} & bcWCB4Ent_P)
                 | ({3{bcWCB5DBSYQual_P}} & bcWCB5Ent_P)
                 : bcWCBEntSrc_P;

We try to also detect skipped signals in these kinds of expressions.

Subtopics

Sd-problem-p
An alleged problem noticed by skip detection.
Sd-keylist-find-skipped
Perform skip-detection for a single pattern within an expression.
Sd-keylist->indicies
(sd-keylist->indicies x) maps sd-key->index across a list.
Sd-key-p
Keys are derived from wire names and are the basis of our skip detection.
Sd-patalist-compare
Perform skip-detection for a single expression.
Sd-analyze-ctxexprs
Perform skip-detection for a list of expressions.
Sd-problemlist-p
(sd-problemlist-p x) recognizes lists where every element satisfies sd-problem-p.
Sd-patalist-p
(sd-patalist-p x) recognizes alists that bind strings to sd-keylist-ps.
Sd-keygen
(sd-keygen x acc) derives a list of sd-key-ps from x, a wire name, and accumulates them into acc.
Sd-patalist
(sd-patalist x) separates a sd-keylist-p by their patterns, producing a sd-patalist-p.
Sd-keylist-p
(sd-keylist-p x) recognizes lists where every element satisfies sd-key-p.
Sd-analyze-modulelist
Perform skip-detection on a module list.
Sd-analyze-module-aux
Collect all the problems.
Sd-analyze-module
Perform skip-detection on a module.
Sd-pp-problem-long
Sd-analyze-modulelist-aux
Sd-problem-score
Sd-pp-problem-header
Sd-analyze-design
Top level skip-detection for a design.
Sd-problem->
Basic ordering on skip-detect problems.
Sd-pp-problem-brief
Sd-pp-problemlist-long
Sd-pp-problemlist-brief
Sd-natlist-linear-increments-p
Sd-keylist-linear-increments-p