• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
        • Svex-stvs
        • Svex-decomposition-methodology
        • Sv-versus-esim
        • Svex-decomp
        • Svex-compose-dfs
        • Svex-compilation
        • Moddb
        • Svmods
          • Address
          • Wire
          • Module
          • Lhs
            • Lhs.lisp
              • Lhs-vars-normorderedp
              • Lhs-norm
              • Lhatom-normorderedp
              • Lhs-normp
              • Svex-lhsrewrite-aux
              • Lhs-concat
              • Lhs-check-masks
              • Lhrange-combine
              • Svexarr-vars-aux
              • Assigns-check-masks
              • Svex->lhs-range
              • Svex-lhs-preproc-blkrev
              • Svarlist-boundedp-badguy
              • Driverlist-rest-after-strength
              • Aliases-normorderedp
              • Lhs-rsh
              • Lhs-cons
              • Svarlist-boundedp
              • Lhs-bitproj
              • Lhs-vars
              • Driver
              • Svex-override
              • Make-simple-lhs
              • Lhssvex-range-p
              • Lhs-override
              • Lhs-first-aux
              • Lhrange-combinable-dec
              • Lhrange-bitproj
              • Lhatom
              • Driverlist-values-of-strength
              • Lhs-rest-aux
              • Lhs-rest
              • Aliases-normorderedp-aux
              • Svexarr-vars
              • Lhsarr-to-svexarr
              • Svexarr-vars-witness-aux
              • Lhbit
                • Lhbit-case
                  • Lhbit-fix
                  • Lhbit-equiv
                  • Lhbit-var
                  • Lhbit-p
                  • Lhbit-z
                  • Lhbit-kind
                • Svex-lhsrewrite
                • Svar-boundedp
                • Lhs-decomp-aux
                • Svex->lhs-bound
                • Aliases-vars-aux
                • Svexarr
                • Svexarr-vars-witness
                • Svar-set-index
                • Lhsarr
                • Lhs-override-vars
                • Lhatom-eval-zero
                • Lhatom-bitproj
                • Lhrange-nextbit
                • Lhrange-combinable
                • Driverlist->svex
                • Svexlist-resolve
                • Lhs->svex-zero
                • Lhs-overridelist-vars
                • Lhs-overridelist-keys
                • Lhbit-eval
                • Driverlist-vars
                • Assigns-vars
                • Svex-int
                • Lhssvex-bounded-p
                • Lhslist-vars
                • Lhs-decomp
                • Lhatom-vars
                • Svar-map-vars
                • Lhssvex-unbounded-p
                • Lhspairs-vars
                • Lhs-width
                • Aliases-vars
                • Lhs-first
                • Svar-index
                • Assigns
                • Svar-indexedp
                • Lhspairs
                • Svex-overridelist
                • Lhslist
                • Lhs-overridelist
                • Driverlist
                • Svex-lhs-preproc
                • Svexarr-fix
                • Lhsarr-fix
              • Lhs-p
              • Lhs-fix
              • Lhrange
              • Lhs-eval-zx
              • Lhs-equiv
              • Lhs-eval
              • Lhs->svex
            • Path
            • Svar-add-namespace
            • Design
            • Modinst
            • Lhs-add-namespace
            • Modalist
            • Path-add-namespace
            • Modname->submodnames
            • Name
            • Constraintlist-addr-p
            • Svex-alist-addr-p
            • Svar-map-addr-p
            • Lhspairs-addr-p
            • Modname
            • Assigns-addr-p
            • Lhs-addr-p
            • Lhatom-addr-p
            • Modhier-list-measure
            • Attributes
            • Modhier-measure
            • Modhier-list-measure-aux
            • Modhier-loopfreelist-p
            • Modhier-loopfree-p
          • Svstmt
          • Sv-tutorial
          • Expressions
          • Symbolic-test-vector
          • Vl-to-svex
        • Fgl
        • Vwsim
        • Vl
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Lhbit

    Lhbit-case

    Case macro for the different kinds of lhbit structures.

    This is an fty sum-type case macro, typically introduced by defflexsum or deftagsum. It allows you to safely check the type of a lhbit structure, or to split into cases based on its type.

    Short Form

    In its short form, lhbit-case allows you to safely check the type of a lhbit structure. For example:

    (lhbit-case x :z)

    is essentially just a safer alternative to writing:

    (equal (lhbit-kind x) :z)

    Why is using lhbit-case safer? When we directly inspect the kind with equal, there is no static checking being done to ensure that, e.g., :z is a valid kind of lhbit structure. That means there is nothing to save you if, later, you change the kind keyword for this type from :z to something else. It also means you get no help if you just make a typo when writing the :z symbol. Over the course of developing VL, we found that such issues were very frequent sources of errors!

    Long Form

    In its longer form, lhbit-case allows you to split into cases based on the kind of structure you are looking at. A typical example would be:

    (lhbit-case x
      :z ...
      :var ...)

    It is also possible to consolidate ``uninteresting'' cases using :otherwise.

    For convenience, the case macro automatically binds the fields of x for you, as appropriate for each case. That is, in the :z case, you can use defprod-style foo.bar style accessors for x without having to explicitly add a z b* binder.