• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
      • Fgl
      • Vwsim
      • Vl
        • Syntax
        • Loader
        • Warnings
        • Getting-started
        • Utilities
        • Printer
        • Kit
          • Vl-lint
            • Vl-lintconfig-p
            • Condcheck
            • Lint-warning-suppression
            • Lucid
            • Lvaluecheck
            • Vl-interfacelist-alwaysstyle
            • Truncation-warnings
            • Vl-modulelist-alwaysstyle
            • Skip-detection
              • Vl-ctxexprlist->exprs
              • Sd-keylist->indicies
              • Sd-keylist-find-skipped
              • Sd-problem
              • Sd-key
              • Sd-patalist-compare
              • Sd-analyze-ctxexprs
              • Sd-keygen
              • Make-sd-patalist
              • Sd-analyze-modulelist
              • Sd-analyze-module-aux
              • Sd-analyze-module
              • Sd-pp-problem-long
              • Sd-problem-score
              • Sd-pp-problem-header
              • Sd-analyze-modulelist-aux
              • Sd-analyze-design
              • Sd-problem->
              • Sd-patalist
              • Sd-problemlist
              • Sd-pp-problem-brief
              • Sd-keylist
              • Sd-pp-problemlist-long
              • Sd-pp-problemlist-brief
              • Sd-natlist-linear-increments-p
              • Sd-keylist-linear-increments-p
            • Vl-lint-report
            • Vl-lintresult
            • Vl::vl-design-sv-use-set
            • Oddexpr-check
            • Leftright-check
            • Duplicate-detect
            • Selfassigns
            • *vl-lint-help*
            • Arith-compare-check
            • Dupeinst-check
            • Qmarksize-check
            • Lint-whole-file-suppression
            • Run-vl-lint-main
            • Logicassign
            • Run-vl-lint
            • Vl-print-certain-warnings
            • Duperhs-check
            • Vl-lint-top
            • Sd-filter-problems
            • Vl-modulelist-add-svbad-warnings
            • Vl-module-add-svbad-warnings
            • Check-case
            • Vl-lint-extra-actions
            • Drop-lint-stubs
            • Vl-lint-print-warnings
            • Drop-user-submodules
            • Check-namespace
            • Vl-lintconfig-loadconfig
            • Vl-lint-design->svex-modalist-wrapper
            • Vl-delete-sd-problems-for-modnames-aux
            • Vl-collect-new-names-from-orignames
            • Vl-lint-print-all-warnings
            • Vl-design-remove-unnecessary-modules
            • Vl-delete-sd-problems-for-modnames
            • Vl-always-check-style
            • Vl-vardecllist-svbad-warnings
            • Vl-vardecl-svbad-warnings
            • Vl-reportcard-remove-suppressed
            • Vl-reportcard-keep-suppressed
            • Vl-alwayslist-check-style
            • Vl-remove-nameless-descriptions
            • Vl-lint-apply-quiet
            • Vl-warninglist-remove-suppressed
            • Vl-warninglist-keep-suppressed
            • Vl-print-eliminated-descs
            • Vl-module-alwaysstyle
            • Vl-jp-reportcard-aux
            • Vl-interface-alwaysstyle
            • Vl-design-alwaysstyle
            • Vl-jp-description-locations
            • Vl-jp-reportcard
            • Vl-pp-stringlist-lines
            • Vl-jp-design-locations
            • Vl-datatype-svbad-p
            • Unpacked-range-check
            • Sd-problem-major-p
            • Vl-alwaysstyle
          • Vl-server
          • Vl-gather
          • Vl-zip
          • Vl-main
          • Split-plusargs
          • Vl-shell
          • Vl-json
        • Mlib
        • Transforms
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Vl-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

Vl-ctxexprlist->exprs
(vl-ctxexprlist->exprs x) maps vl-ctxexpr->expr across a list.
Sd-keylist->indicies
(sd-keylist->indicies x) maps sd-key->index across a list.
Sd-keylist-find-skipped
Perform skip-detection for a single pattern within an expression.
Sd-problem
An alleged problem noticed by skip detection.
Sd-key
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-keygen
(sd-keygen x acc) derives a list of sd-key-ps from x, a wire name, and accumulates them into acc.
Make-sd-patalist
(make-sd-patalist x) separates a sd-keylist-p by their patterns, producing a sd-patalist-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-problem-score
Sd-pp-problem-header
Sd-analyze-modulelist-aux
Sd-analyze-design
Top level skip-detection for a design.
Sd-problem->
Basic ordering on skip-detect problems.
Sd-patalist
An alist mapping stringp to sd-keylist-p.
Sd-problemlist
A list of sd-problem-p objects.
Sd-pp-problem-brief
Sd-keylist
A list of sd-key-p objects.
Sd-pp-problemlist-long
Sd-pp-problemlist-brief
Sd-natlist-linear-increments-p
Sd-keylist-linear-increments-p