• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • 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-aux

Signature

(vl-casestmt-elim-aux test cases default) → new-stmt

Arguments

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

cases — The match expressions and bodies.
    Guard (vl-caselist-p cases).

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

Returns

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

Definitions and Theorems

Function: vl-casestmt-elim-aux

(defun vl-casestmt-elim-aux (test cases default)
  (declare (xargs :guard (and (vl-expr-p test)
                              (vl-caselist-p cases)
                              (vl-stmt-p default))))
  (declare
       (xargs :guard (and (vl-expr->finaltype test)
                          (posp (vl-expr->finalwidth test))
                          (vl-casestmt-sizes-agreep test cases))))
  (let ((__function__ 'vl-casestmt-elim-aux))
    (declare (ignorable __function__))
    (b* ((cases (vl-caselist-fix cases))
         ((when (atom cases))
          (vl-stmt-fix default))
         ((cons match-exprs1 body1) (car cases)))
      (make-vl-ifstmt
           :condition (vl-casestmt-compare-expr test match-exprs1)
           :truebranch body1
           :falsebranch (vl-casestmt-elim-aux test (cdr cases)
                                              default)))))

Theorem: vl-stmt-p-of-vl-casestmt-elim-aux

(defthm vl-stmt-p-of-vl-casestmt-elim-aux
  (b* ((new-stmt (vl-casestmt-elim-aux test cases default)))
    (vl-stmt-p new-stmt))
  :rule-classes :rewrite)

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

(defthm vl-casestmt-elim-aux-of-vl-expr-fix-test
  (equal (vl-casestmt-elim-aux (vl-expr-fix test)
                               cases default)
         (vl-casestmt-elim-aux test cases default)))

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

(defthm vl-casestmt-elim-aux-vl-expr-equiv-congruence-on-test
  (implies (vl-expr-equiv test test-equiv)
           (equal (vl-casestmt-elim-aux test cases default)
                  (vl-casestmt-elim-aux test-equiv cases default)))
  :rule-classes :congruence)

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

(defthm vl-casestmt-elim-aux-of-vl-caselist-fix-cases
  (equal (vl-casestmt-elim-aux test (vl-caselist-fix cases)
                               default)
         (vl-casestmt-elim-aux test cases default)))

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

(defthm vl-casestmt-elim-aux-vl-caselist-equiv-congruence-on-cases
  (implies (vl-caselist-equiv cases cases-equiv)
           (equal (vl-casestmt-elim-aux test cases default)
                  (vl-casestmt-elim-aux test cases-equiv default)))
  :rule-classes :congruence)

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

(defthm vl-casestmt-elim-aux-of-vl-stmt-fix-default
  (equal (vl-casestmt-elim-aux test cases (vl-stmt-fix default))
         (vl-casestmt-elim-aux test cases default)))

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

(defthm vl-casestmt-elim-aux-vl-stmt-equiv-congruence-on-default
  (implies (vl-stmt-equiv default default-equiv)
           (equal (vl-casestmt-elim-aux test cases default)
                  (vl-casestmt-elim-aux test cases default-equiv)))
  :rule-classes :congruence)