• 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-p
            • Vl-lucidstate-fix
            • Vl-lucidval
            • Vl-lucidocc
            • Vl-lucidkey
            • Vl-lucidstate-equiv
            • Make-vl-lucidstate
            • Vl-lucidstate->warnings
            • Vl-lucidstate->generatesp
            • Vl-luciddb-count
            • Vl-lucidstate->paramsp
            • Change-vl-lucidstate
            • Vl-lucidstate->db
            • Vl-lucidocc->ctx
            • Vl-lucidocc->ss
            • Vl-luciddb
              • Vl-luciddb-p
              • Vl-luciddb-fix
              • Vl-luciddb-equiv
            • Vl-lucidocclist
            • Vl-lucidkeylist
          • 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

• Vl-lucidstate

Vl-luciddb

The main lucid database. Binds keys (scopestack/item pairs) to information about how they have been used.

This is an ordinary fty::defalist.

Subtopics

Vl-luciddb-p

Recognizer for vl-luciddb.

Vl-luciddb-fix

(vl-luciddb-fix x) is an ACL2::fty alist fixing function that follows the fix-keys strategy.

Vl-luciddb-equiv

Basic equivalence relation for vl-luciddb structures.