• 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
          • Vl-lucidstate
          • Vl-lucidstate-init
          • Vl-lucid-dissect-pair
          • Vl-hidslice-mark
          • Vl-lucid-dissect-var-main
          • Vl-lucid-multidrive-detect
          • Vl-lucid-filter-merges
          • Vl-hidsolo-mark
          • Vl-maybe-delayoreventcontrol-lucidcheck
          • Vl-maybe-packeddimension-lucidcheck
          • Vl-delayoreventcontrol-lucidcheck
          • Vl-repeateventcontrol-lucidcheck
          • Vl-packeddimensionlist-lucidcheck
          • Vl-namedparamvaluelist-lucidcheck
          • Vl-hidtrace-mark-interfaces
          • Vl-hidstep-mark-interfaces
          • Vl-maybe-paramvalue-lucidcheck
          • Vl-paramvaluelist-lucidcheck
          • Vl-packeddimension-lucidcheck
          • Vl-namedparamvalue-lucidcheck
          • Vl-maybe-gatedelay-lucidcheck
          • Vl-rhsatom-lucidcheck
          • Vl-plainarglist-lucidcheck
          • Vl-namedarglist-lucidcheck
          • Vl-lucidstate-mark
          • Vl-lucid-mark-simple
          • Vl-eventcontrol-lucidcheck
          • Vl-enumitemlist-lucidcheck
          • Vl-enumbasetype-lucidcheck
          • Vl-enumbasekind-lucidcheck
          • Vl-delaycontrol-lucidcheck
          • Vl-plainarg-lucidcheck
          • Vl-paramvalue-lucidcheck
          • Vl-paramargs-lucidcheck
          • Vl-maybe-rhsexpr-lucidcheck
          • Vl-maybe-range-lucidcheck
          • Vl-gatedelay-lucidcheck
          • Vl-evatomlist-lucidcheck
          • Vl-arguments-lucidcheck
          • Vl-rangelist-lucidcheck
          • Vl-namedarg-lucidcheck
          • Vl-enumitem-lucidcheck
          • Vl-custom-suppress-multidrive-p
          • Vl-evatom-lucidcheck
          • Vl-range-lucidcheck
          • Vl-pps-lucidstate
          • Vl-lucid-valid-bits-for-datatype
          • Vl-lucidocclist-drop-bad-modinsts
          • Vl-paramdecl-lucidcheck
          • Vl-lucid-dissect-database
          • Vl-interfaceportlist-lucidcheck
          • Vl-interfaceport-lucidcheck
          • Vl-taskdecllist-lucidcheck
          • Vl-taskdecl-lucidcheck
          • Vl-portdecllist-lucidcheck
          • Vl-paramdecllist-lucidcheck
          • Vl-interfacelist-lucidcheck
          • Vl-gateinstlist-lucidcheck
          • Vl-fundecl-lucidcheck
          • Vl-design-lucidcheck-main
          • Vl-vardecllist-lucidcheck
          • Vl-vardecl-lucidcheck
          • Vl-typedeflist-lucidcheck
          • Vl-portdecl-lucidcheck
          • Vl-packagelist-lucidcheck
          • Vl-package-lucidcheck
          • Vl-modulelist-lucidcheck
          • Vl-modinstlist-lucidcheck
          • Vl-modinst-lucidcheck
          • Vl-interface-lucidcheck
          • Vl-initiallist-lucidcheck
          • Vl-gateinst-lucidcheck
          • Vl-fundecllist-lucidcheck
          • Vl-assignlist-lucidcheck
          • Vl-alwayslist-lucidcheck
          • Vl-typedef-lucidcheck
          • Vl-initial-lucidcheck
          • Vl-design-lucid
          • Vl-assign-lucidcheck
          • Vl-module-lucidcheck
          • Vl-always-lucidcheck
          • Vl-lucidocclist-drop-foreign-writes
          • Vl-lucid-valid-bits-for-decl
          • Vl-custom-suppress-multidrive-p-default
          • Vl-lucidmergealist-count
          • Vl-lucid-scopestack-subscope-p
          • Vl-lucid-collect-solo-occs
          • Vl-lucid-collect-resolved-slices
          • Vl-lucid-pp-multibits
          • Vl-lucid-ctx
          • Vl-lucidocclist-drop-initials
          • Vl-lucidocclist-drop-generates
          • Vl-lucid-slices-append-bits
          • Vl-lucid-first-solo-occ
          • Vl-lucid-do-merges1
          • Vl-lucid-do-merges
          • Vl-lucidocclist-remove-tails
          • Vl-lucid-some-solo-occp
          • Vl-lucid-resolved-slices->bits
          • Vl-lucid-resolved-slice->bits
          • Vl-scopestack-top-level-name
          • Vl-normalize-scopestack
          • Vl-lucid-resolved-slice-p
          • Vl-lucid-all-slices-resolved-p
          • Vl-lucid-range->bits
          • Vl-lucid-plainarglist-nicely-resolved-p
          • Vl-lucid-multidrive-summary
          • Vl-pp-lucid-multidrive-summary
          • Vl-lucid-dissect
          • Vl-lucid-all-slices-p
          • Vl-lucidocclist-some-transistory-p
          • Vl-lucidocc-transistory-p
          • Vl-lucid-plainarg-nicely-resolved-p
          • Vl-inside-true-generate-p
          • Vl-lucid-z-gateinst-p
          • Vl-lucid-modinst-nicely-resolved-p
          • Vl-inside-interface-p
          • Vl-inside-blockscope-p
          • Vl-lucid-z-expr-p
          • Vl-lucid-z-assign-p
          • Vl-lucidmergealist
          • Vl-lucid-summarize-bits
          • Vl-pp-merged-index-list
          • Vl-pp-merged-index
          • Vl-lucid-pp-bits
          • Vl-fast-range-p
        • Skip-detection
        • 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
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Lucid

Vl-lucid-dissect-var-main

Signature

(vl-lucid-dissect-var-main ss item used set genp) → warnings

Arguments

ss — Guard (vl-scopestack-p ss).

item — Guard (or (vl-paramdecl-p item) (vl-vardecl-p item)).

used — Guard (vl-lucidocclist-p used).

set — Guard (vl-lucidocclist-p set).

genp — Guard (booleanp genp).

Returns

warnings — Type (vl-warninglist-p warnings).

Definitions and Theorems

Function: vl-lucid-dissect-var-main

(defun vl-lucid-dissect-var-main (ss item used set genp)
 (declare (xargs :guard (and (vl-scopestack-p ss)
                             (or (vl-paramdecl-p item)
                                 (vl-vardecl-p item))
                             (vl-lucidocclist-p used)
                             (vl-lucidocclist-p set)
                             (booleanp genp))))
 (let ((__function__ 'vl-lucid-dissect-var-main))
  (declare (ignorable __function__))
  (b*
   ((used (vl-lucidocclist-fix used))
    (set (vl-lucidocclist-fix set))
    (name (if (eq (tag item) :vl-vardecl)
              (vl-vardecl->name item)
            (vl-paramdecl->name item)))
    (warnings (vl-lucid-multidrive-detect ss item set genp))
    ((when (and (atom used) (atom set)))
     (warn :type :vl-lucid-spurious
           :msg "~w0 is never used or set anywhere. (~s1)"
           :args (list name
                       (with-local-ps (vl-pp-scopestack-path ss)))))
    (used-solop (vl-lucid-some-solo-occp used))
    (set-solop (vl-lucid-some-solo-occp set))
    ((when (and used-solop set-solop))
     warnings)
    ((mv simplep valid-bits)
     (vl-lucid-valid-bits-for-decl item ss))
    (warnings
     (b*
      (((when (atom used))
        (warn
           :type :vl-lucid-unused
           :msg "~w0 is set but is never used. (~s1)"
           :args (list name
                       (with-local-ps (vl-pp-scopestack-path ss)))))
       ((when used-solop) warnings)
       ((unless (and simplep (vl-lucid-all-slices-p used)
                     (vl-lucid-all-slices-resolved-p used)))
        warnings)
       (used-bits (vl-lucid-resolved-slices->bits used))
       (unused-bits (difference valid-bits used-bits))
       ((unless unused-bits) warnings))
      (warn
          :type :vl-lucid-unused
          :msg "~w0 has some bits that are never used: ~s1. (~s2)"
          :args (list name
                      (vl-lucid-summarize-bits unused-bits)
                      (with-local-ps (vl-pp-scopestack-path ss))))))
    (warnings
     (b*
      (((when (atom set))
        (warn
           :type :vl-lucid-unset
           :msg "~w0 is used but is never initialized. (~s1)"
           :args (list name
                       (with-local-ps (vl-pp-scopestack-path ss)))))
       ((when set-solop) warnings)
       ((unless (and simplep (vl-lucid-all-slices-p set)
                     (vl-lucid-all-slices-resolved-p set)))
        warnings)
       (set-bits (vl-lucid-resolved-slices->bits set))
       (unset-bits (difference valid-bits set-bits))
       ((unless unset-bits) warnings))
      (warn
         :type :vl-lucid-unset
         :msg "~w0 has some bits that are never set: ~s1. (~s2)"
         :args (list name
                     (vl-lucid-summarize-bits unset-bits)
                     (with-local-ps (vl-pp-scopestack-path ss)))))))
   warnings)))

Theorem: vl-warninglist-p-of-vl-lucid-dissect-var-main

(defthm vl-warninglist-p-of-vl-lucid-dissect-var-main
  (b* ((warnings (vl-lucid-dissect-var-main ss item used set genp)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-lucid-dissect-var-main-of-vl-scopestack-fix-ss

(defthm vl-lucid-dissect-var-main-of-vl-scopestack-fix-ss
  (equal (vl-lucid-dissect-var-main (vl-scopestack-fix ss)
                                    item used set genp)
         (vl-lucid-dissect-var-main ss item used set genp)))

Theorem: vl-lucid-dissect-var-main-vl-scopestack-equiv-congruence-on-ss

(defthm
     vl-lucid-dissect-var-main-vl-scopestack-equiv-congruence-on-ss
 (implies
    (vl-scopestack-equiv ss ss-equiv)
    (equal (vl-lucid-dissect-var-main ss item used set genp)
           (vl-lucid-dissect-var-main ss-equiv item used set genp)))
 :rule-classes :congruence)

Theorem: vl-lucid-dissect-var-main-of-vl-lucidocclist-fix-used

(defthm vl-lucid-dissect-var-main-of-vl-lucidocclist-fix-used
  (equal
       (vl-lucid-dissect-var-main ss item (vl-lucidocclist-fix used)
                                  set genp)
       (vl-lucid-dissect-var-main ss item used set genp)))

Theorem: vl-lucid-dissect-var-main-vl-lucidocclist-equiv-congruence-on-used

(defthm
 vl-lucid-dissect-var-main-vl-lucidocclist-equiv-congruence-on-used
 (implies
    (vl-lucidocclist-equiv used used-equiv)
    (equal (vl-lucid-dissect-var-main ss item used set genp)
           (vl-lucid-dissect-var-main ss item used-equiv set genp)))
 :rule-classes :congruence)

Theorem: vl-lucid-dissect-var-main-of-vl-lucidocclist-fix-set

(defthm vl-lucid-dissect-var-main-of-vl-lucidocclist-fix-set
 (equal
   (vl-lucid-dissect-var-main ss item used (vl-lucidocclist-fix set)
                              genp)
   (vl-lucid-dissect-var-main ss item used set genp)))

Theorem: vl-lucid-dissect-var-main-vl-lucidocclist-equiv-congruence-on-set

(defthm
  vl-lucid-dissect-var-main-vl-lucidocclist-equiv-congruence-on-set
 (implies
    (vl-lucidocclist-equiv set set-equiv)
    (equal (vl-lucid-dissect-var-main ss item used set genp)
           (vl-lucid-dissect-var-main ss item used set-equiv genp)))
 :rule-classes :congruence)

Theorem: vl-lucid-dissect-var-main-of-bool-fix-genp

(defthm vl-lucid-dissect-var-main-of-bool-fix-genp
 (equal
  (vl-lucid-dissect-var-main ss item used set (acl2::bool-fix genp))
  (vl-lucid-dissect-var-main ss item used set genp)))

Theorem: vl-lucid-dissect-var-main-iff-congruence-on-genp

(defthm vl-lucid-dissect-var-main-iff-congruence-on-genp
 (implies
    (iff genp genp-equiv)
    (equal (vl-lucid-dissect-var-main ss item used set genp)
           (vl-lucid-dissect-var-main ss item used set genp-equiv)))
 :rule-classes :congruence)