• 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
        • Expression-sizing
        • Occform
        • Oprewrite
        • Expand-functions
        • Delayredux
        • Unparameterization
        • Caseelim
          • Vl-casezx-stmt-elim
          • Vl-casezx-matchexpr
          • Vl-modulelist-caseelim
          • Vl-casezx-match-any-expr
          • Vl-casestmt-elim
          • Vl-casestmt-size-warnings
          • Vl-casezx-elim-aux
          • Vl-stmt-caseelim
          • Case-statement-problems
          • Vl-casestmt-compare-expr
          • Vl-initiallist-caseelim
          • Vl-alwayslist-caseelim
          • Vl-casestmt-elim-aux
          • Vl-initial-caseelim
          • Vl-always-caseelim
          • Vl-casestmt-sizes-agreep
          • Vl-module-caseelim
          • Vl-design-caseelim
        • Split
        • Selresolve
        • Weirdint-elim
        • Vl-delta
        • Replicate-insts
        • Rangeresolve
        • Propagate
        • Clean-selects
        • Clean-params
        • Blankargs
        • Inline-mods
        • Expr-simp
        • Trunc
        • Always-top
        • Gatesplit
        • Gate-elim
        • Expression-optimization
        • Elim-supplies
        • Wildelim
        • Drop-blankports
        • Clean-warnings
        • Addinstnames
        • Custom-transform-hooks
        • Annotate
        • Latchcode
        • Elim-unused-vars
        • Problem-modules
      • Lint
      • Mlib
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Caseelim

Vl-casestmt-elim

Rewrite an ordinary case statement into if statements.

Signature

(vl-casestmt-elim check test caselist default atts ctx warnings) 
  → 
(mv warnings new-stmt)

Arguments

check — The kind of checking to do, if any.
    Guard (vl-casecheck-p check).

test — The test expression, should be sized.
    Guard (vl-expr-p test).

caselist — The cases, should be sized.
    Guard (vl-caselist-p caselist).

default — The body for the default case.
    Guard (vl-stmt-p default).

atts — Any attributes on the whole case statement.
    Guard (vl-atts-p atts).

ctx — Context for warnings.
    Guard (vl-modelement-p ctx).

warnings — Ordinary warnings accumulator.
    Guard (vl-warninglist-p warnings).

Returns

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

new-stmt — Type (vl-stmt-p new-stmt).

Definitions and Theorems

Function: vl-casestmt-elim

(defun vl-casestmt-elim
       (check test caselist default atts ctx warnings)
 (declare (xargs :guard (and (vl-casecheck-p check)
                             (vl-expr-p test)
                             (vl-caselist-p caselist)
                             (vl-stmt-p default)
                             (vl-atts-p atts)
                             (vl-modelement-p ctx)
                             (vl-warninglist-p warnings))))
 (let ((__function__ 'vl-casestmt-elim))
  (declare (ignorable __function__))
  (b*
   ((warnings (vl-warninglist-fix warnings))
    (new-warnings (vl-casestmt-size-warnings test caselist ctx))
    (check (vl-casecheck-fix check))
    ((when new-warnings)
     (mv (append new-warnings warnings)
         (make-vl-casestmt :casetype nil
                           :check check
                           :test test
                           :caselist caselist
                           :default default
                           :atts atts)))
    (warnings
     (if check
      (warn
       :type :vl-case-check
       :msg
       "~a0: we don't yet implement priority, unique, or ~
                         unique0 checking for case statements.  We will ~
                         treat this as an ordinary case statement."
       :args (list (vl-modelement-fix ctx)))
      (ok))))
   (mv warnings
       (vl-casestmt-elim-aux test caselist default)))))

Theorem: vl-warninglist-p-of-vl-casestmt-elim.warnings

(defthm vl-warninglist-p-of-vl-casestmt-elim.warnings
  (b* (((mv ?warnings ?new-stmt)
        (vl-casestmt-elim check test
                          caselist default atts ctx warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-stmt-p-of-vl-casestmt-elim.new-stmt

(defthm vl-stmt-p-of-vl-casestmt-elim.new-stmt
  (b* (((mv ?warnings ?new-stmt)
        (vl-casestmt-elim check test
                          caselist default atts ctx warnings)))
    (vl-stmt-p new-stmt))
  :rule-classes :rewrite)

Theorem: vl-casestmt-elim-of-vl-casecheck-fix-check

(defthm vl-casestmt-elim-of-vl-casecheck-fix-check
  (equal (vl-casestmt-elim (vl-casecheck-fix check)
                           test caselist default atts ctx warnings)
         (vl-casestmt-elim check test
                           caselist default atts ctx warnings)))

Theorem: vl-casestmt-elim-vl-casecheck-equiv-congruence-on-check

(defthm vl-casestmt-elim-vl-casecheck-equiv-congruence-on-check
 (implies
   (vl-casecheck-equiv check check-equiv)
   (equal (vl-casestmt-elim check
                            test caselist default atts ctx warnings)
          (vl-casestmt-elim check-equiv test
                            caselist default atts ctx warnings)))
 :rule-classes :congruence)

Theorem: vl-casestmt-elim-of-vl-expr-fix-test

(defthm vl-casestmt-elim-of-vl-expr-fix-test
  (equal (vl-casestmt-elim check (vl-expr-fix test)
                           caselist default atts ctx warnings)
         (vl-casestmt-elim check test
                           caselist default atts ctx warnings)))

Theorem: vl-casestmt-elim-vl-expr-equiv-congruence-on-test

(defthm vl-casestmt-elim-vl-expr-equiv-congruence-on-test
 (implies
   (vl-expr-equiv test test-equiv)
   (equal (vl-casestmt-elim check
                            test caselist default atts ctx warnings)
          (vl-casestmt-elim check test-equiv
                            caselist default atts ctx warnings)))
 :rule-classes :congruence)

Theorem: vl-casestmt-elim-of-vl-caselist-fix-caselist

(defthm vl-casestmt-elim-of-vl-caselist-fix-caselist
  (equal (vl-casestmt-elim check test (vl-caselist-fix caselist)
                           default atts ctx warnings)
         (vl-casestmt-elim check test
                           caselist default atts ctx warnings)))

Theorem: vl-casestmt-elim-vl-caselist-equiv-congruence-on-caselist

(defthm vl-casestmt-elim-vl-caselist-equiv-congruence-on-caselist
 (implies
   (vl-caselist-equiv caselist caselist-equiv)
   (equal (vl-casestmt-elim check
                            test caselist default atts ctx warnings)
          (vl-casestmt-elim check test caselist-equiv
                            default atts ctx warnings)))
 :rule-classes :congruence)

Theorem: vl-casestmt-elim-of-vl-stmt-fix-default

(defthm vl-casestmt-elim-of-vl-stmt-fix-default
  (equal (vl-casestmt-elim check
                           test caselist (vl-stmt-fix default)
                           atts ctx warnings)
         (vl-casestmt-elim check test
                           caselist default atts ctx warnings)))

Theorem: vl-casestmt-elim-vl-stmt-equiv-congruence-on-default

(defthm vl-casestmt-elim-vl-stmt-equiv-congruence-on-default
 (implies
   (vl-stmt-equiv default default-equiv)
   (equal (vl-casestmt-elim check
                            test caselist default atts ctx warnings)
          (vl-casestmt-elim check test caselist
                            default-equiv atts ctx warnings)))
 :rule-classes :congruence)

Theorem: vl-casestmt-elim-of-vl-atts-fix-atts

(defthm vl-casestmt-elim-of-vl-atts-fix-atts
  (equal (vl-casestmt-elim check
                           test caselist default (vl-atts-fix atts)
                           ctx warnings)
         (vl-casestmt-elim check test
                           caselist default atts ctx warnings)))

Theorem: vl-casestmt-elim-vl-atts-equiv-congruence-on-atts

(defthm vl-casestmt-elim-vl-atts-equiv-congruence-on-atts
 (implies
   (vl-atts-equiv atts atts-equiv)
   (equal (vl-casestmt-elim check
                            test caselist default atts ctx warnings)
          (vl-casestmt-elim check test caselist
                            default atts-equiv ctx warnings)))
 :rule-classes :congruence)

Theorem: vl-casestmt-elim-of-vl-modelement-fix-ctx

(defthm vl-casestmt-elim-of-vl-modelement-fix-ctx
  (equal (vl-casestmt-elim check test caselist
                           default atts (vl-modelement-fix ctx)
                           warnings)
         (vl-casestmt-elim check test
                           caselist default atts ctx warnings)))

Theorem: vl-casestmt-elim-vl-modelement-equiv-congruence-on-ctx

(defthm vl-casestmt-elim-vl-modelement-equiv-congruence-on-ctx
 (implies
   (vl-modelement-equiv ctx ctx-equiv)
   (equal (vl-casestmt-elim check
                            test caselist default atts ctx warnings)
          (vl-casestmt-elim check test caselist
                            default atts ctx-equiv warnings)))
 :rule-classes :congruence)

Theorem: vl-casestmt-elim-of-vl-warninglist-fix-warnings

(defthm vl-casestmt-elim-of-vl-warninglist-fix-warnings
  (equal (vl-casestmt-elim check test caselist default
                           atts ctx (vl-warninglist-fix warnings))
         (vl-casestmt-elim check test
                           caselist default atts ctx warnings)))

Theorem: vl-casestmt-elim-vl-warninglist-equiv-congruence-on-warnings

(defthm vl-casestmt-elim-vl-warninglist-equiv-congruence-on-warnings
 (implies
   (vl-warninglist-equiv warnings warnings-equiv)
   (equal (vl-casestmt-elim check
                            test caselist default atts ctx warnings)
          (vl-casestmt-elim check test caselist
                            default atts ctx warnings-equiv)))
 :rule-classes :congruence)