• 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-problem
              • Make-sd-problem
              • Change-sd-problem
              • Make-honsed-sd-problem
              • Honsed-sd-problem
              • Sd-problem->type
              • Sd-problem->priority
              • Sd-problem->key
              • Sd-problem->groupsize
              • Sd-problem->ctx
            • 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
  • Skip-detection

Sd-problem-p

An alleged problem noticed by skip detection.

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

  • type — What kind of problem this is. At the moment the type is always :skipped and means that we think some wire is suspiciously skipped. But we imagine that we could add other kinds of analysis that look, e.g., for wires that are oddly duplicated, etc., and hence have other types.
        Invariant (symbolp type).
  • priority — A heuristic score that we give to problems to indicate how likely they are to be a real problem. For instance, we assign extra priority to a sequence of wires like foo1, foo2, foo4, foo5 because the skipped wire is in the middle. We also might assign extra priority if one of the other wires is duplicated.
        Invariant (natp priority).
  • groupsize — Says how many wires had this same pattern. We generally think that the larger the group size is, the more likely the problem is to be legitimate.
        Invariant (natp groupsize).
  • key — The sd-key-p for the missing wire.
        Invariant (sd-key-p key).
  • ctx — Says where this problem originates.
        Invariant (vl-context1-p ctx).

Source link: sd-problem-p

Subtopics

Sd-problem
Raw constructor for sd-problem-p structures.
Make-sd-problem
Constructor macro for sd-problem-p structures.
Change-sd-problem
A copying macro that lets you create new sd-problem-p structures, based on existing structures.
Make-honsed-sd-problem
Constructor macro for honsed sd-problem-p structures.
Honsed-sd-problem
Raw constructor for honsed sd-problem-p structures.
Sd-problem->type
Access the type field of a sd-problem-p structure.
Sd-problem->priority
Access the priority field of a sd-problem-p structure.
Sd-problem->key
Access the key field of a sd-problem-p structure.
Sd-problem->groupsize
Access the groupsize field of a sd-problem-p structure.
Sd-problem->ctx
Access the ctx field of a sd-problem-p structure.