• 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
        • Svstmt
          • Svstmt-case
            • Svstmt-while
            • Svstmt-p
            • Svstmt-if
            • Svstmt-equiv
            • Svstmt-xcond
            • Svstmt-scope
            • Svstmt-assign
            • Svstmt-compile
            • Svstmt-constraints
            • Svstmt-jump
            • Svstmtlist
            • Svstmt-kind
            • Svstmt.lisp
            • Svstmt-fix
            • Svstmt-count
          • Sv-tutorial
          • Expressions
          • Symbolic-test-vector
          • Vl-to-svex
        • Fgl
        • Vwsim
        • Vl
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Svstmt

    Svstmt-case

    Case macro for the different kinds of svstmt 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 svstmt structure, or to split into cases based on its type.

    Short Form

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

    (svstmt-case x :assign)

    is essentially just a safer alternative to writing:

    (equal (svstmt-kind x) :assign)

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

    Long Form

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

    (svstmt-case x
      :assign ...
      :if ...
      :xcond ...
      :while ...
      :constraints ...
      :scope ...
      :jump ...)

    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 :assign case, you can use defprod-style foo.bar style accessors for x without having to explicitly add a assign b* binder.