• 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-key
              • Make-sd-key
              • Change-sd-key
              • Make-honsed-sd-key
              • Honsed-sd-key
              • Sd-key->index
              • Sd-key->pat
              • Sd-key->orig
            • 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
  • Skip-detection

Sd-key-p

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

(sd-key-p x) is a defaggregate of the following fields.

  • pat — The same as the wire name except that some embedded number (perhaps spanning many digits) may have been replaced by a * character.
        Invariant (stringp pat).
  • index — The parsed value of the number that has been replaced, or nil if no replacement was made.
        Invariant (maybe-natp index).
  • orig — 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.
        Invariant (stringp orig).

Source link: sd-key-p

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
Raw constructor for sd-key-p structures.
Make-sd-key
Constructor macro for sd-key-p structures.
Change-sd-key
A copying macro that lets you create new sd-key-p structures, based on existing structures.
Make-honsed-sd-key
Constructor macro for honsed sd-key-p structures.
Honsed-sd-key
Raw constructor for honsed sd-key-p structures.
Sd-key->index
Access the index field of a sd-key-p structure.
Sd-key->pat
Access the pat field of a sd-key-p structure.
Sd-key->orig
Access the orig field of a sd-key-p structure.