• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • 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
        • Fgl
        • Vwsim
        • Vl
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Lucid

    Vl-lucid-pp-multibits

    Signature
    (vl-lucid-pp-multibits badbits occs &key (ps 'ps)) → ps
    Arguments
    badbits — The set of multiply driven bits.
        Guard (setp badbits).
    occs — Occs which may or may not drive these bits.
        Guard (vl-lucidocclist-p occs).

    Definitions and Theorems

    Function: vl-lucid-pp-multibits-fn

    (defun vl-lucid-pp-multibits-fn (badbits occs ps)
     (declare (xargs :stobjs (ps)))
     (declare (xargs :guard (and (setp badbits)
                                 (vl-lucidocclist-p occs))))
     (declare
          (xargs :guard (and (nat-listp badbits)
                             (vl-lucid-all-slices-p occs)
                             (vl-lucid-all-slices-resolved-p occs))))
     (let ((__function__ 'vl-lucid-pp-multibits))
      (declare (ignorable __function__))
      (b* (((when (atom occs)) ps)
           (occbits (vl-lucid-resolved-slice->bits (car occs)))
           (overlap (intersect occbits badbits))
           ((unless overlap)
            (vl-lucid-pp-multibits badbits (cdr occs))))
       (vl-ps-seq (vl-indent 4)
                  (if (vl-plural-p overlap)
                      (vl-print " - Bits ")
                    (vl-print " - Bit "))
                  (vl-lucid-pp-bits overlap)
                  (vl-print ": ")
                  (vl-pp-ctxelement-summary
                       (vl-context1->elem (vl-lucidocc->ctx (car occs)))
                       :withloc t)
                  (vl-println "")
                  (vl-lucid-pp-multibits badbits (cdr occs))))))

    Theorem: vl-lucid-pp-multibits-fn-of-vl-lucidocclist-fix-occs

    (defthm vl-lucid-pp-multibits-fn-of-vl-lucidocclist-fix-occs
     (equal (vl-lucid-pp-multibits-fn badbits (vl-lucidocclist-fix occs)
                                      ps)
            (vl-lucid-pp-multibits-fn badbits occs ps)))

    Theorem: vl-lucid-pp-multibits-fn-vl-lucidocclist-equiv-congruence-on-occs

    (defthm
      vl-lucid-pp-multibits-fn-vl-lucidocclist-equiv-congruence-on-occs
      (implies (vl-lucidocclist-equiv occs occs-equiv)
               (equal (vl-lucid-pp-multibits-fn badbits occs ps)
                      (vl-lucid-pp-multibits-fn badbits occs-equiv ps)))
      :rule-classes :congruence)