• 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-key-fix
                • Sd-key-equiv
                • Make-sd-key
                • Sd-key->index
                • Change-sd-key
                • Sd-key->pat
                • Sd-key->orig
                • Sd-key-p
              • 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
  • Skip-detection

Sd-key

Keys are derived from wire names and are the basis of our skip detection.

This is a product type introduced by defprod.

Fields
pat — stringp
The same as the wire name except that some embedded number (perhaps spanning many digits) may have been replaced by a * character.
index — maybe-natp
The parsed value of the number that has been replaced, or nil if no replacement was made.
orig — stringp
The original wire name. This is somewhat unnecessary since it can be recovered by just replacing * in pat with the characters for index, but we thought it was convenient to keep around

The idea of keys is to cause related signals to have the same pattern. For instance, bcWCB0Ent_P and bcWCB1Ent_P will both give rise to the pattern bcWCB*Ent_P.

Because a particular wire name might include many numbers, we may generate a list of keys for a single wire. For instance, for bcL2RB1NoRtry_P we will generate one key with the pattern bcL*RB1NoRtry_P and another with the pattern bcL2RB*NoRtry_P. We had previously considered using a list of indices, but found it easier to just generate multiple keys, each with a single index.

Subtopics

Sd-key-fix
Fixing function for sd-key structures.
Sd-key-equiv
Basic equivalence relation for sd-key structures.
Make-sd-key
Basic constructor macro for sd-key structures.
Sd-key->index
Get the index field from a sd-key.
Change-sd-key
Modifying constructor for sd-key structures.
Sd-key->pat
Get the pat field from a sd-key.
Sd-key->orig
Get the orig field from a sd-key.
Sd-key-p
Recognizer for sd-key structures.