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

Signature

(vl-casezx-elim-aux type test cases default ctx warnings) 
  → 
(mv warnings new-stmt?)

Arguments

type — Kind of case statement.
    Guard (vl-casetype-p type).

test — E.g., for casex(data) ..., the msb-first bits of data.
    Guard (vl-expr-p test).

cases — Compatibly sized cases.
    Guard (vl-caselist-p cases).

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

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 (equal (vl-stmt-p new-stmt?) (if new-stmt? t nil)).

Definitions and Theorems

Function: vl-casezx-elim-aux

(defun vl-casezx-elim-aux (type test cases default ctx warnings)
 (declare (xargs :guard (and (vl-casetype-p type)
                             (vl-expr-p test)
                             (vl-caselist-p cases)
                             (vl-stmt-p default)
                             (vl-modelement-p ctx)
                             (vl-warninglist-p warnings))))
 (declare (xargs :guard (and (member type '(:vl-casez :vl-casex))
                             (vl-expr-welltyped-p test)
                             (posp (vl-expr->finalwidth test))
                             (equal (vl-expr->finaltype test)
                                    :vl-unsigned))))
 (let ((__function__ 'vl-casezx-elim-aux))
  (declare (ignorable __function__))
  (b*
   ((cases (vl-caselist-fix cases))
    (default (vl-stmt-fix default))
    ((when (atom cases)) (mv (ok) default))
    ((cons match-exprs1 body1) (car cases))
    ((mv warnings match-expr)
     (vl-casezx-match-any-expr type test match-exprs1 ctx warnings))
    ((unless match-expr) (mv warnings nil))
    ((mv warnings rest-stmt)
     (vl-casezx-elim-aux type test (cdr cases)
                         default ctx warnings))
    ((unless rest-stmt) (mv warnings nil))
    (new-stmt (make-vl-ifstmt :condition match-expr
                              :truebranch body1
                              :falsebranch rest-stmt)))
   (mv warnings new-stmt))))

Theorem: vl-warninglist-p-of-vl-casezx-elim-aux.warnings

(defthm vl-warninglist-p-of-vl-casezx-elim-aux.warnings
  (b* (((mv ?warnings ?new-stmt?)
        (vl-casezx-elim-aux type test cases default ctx warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-casezx-elim-aux.new-stmt?

(defthm return-type-of-vl-casezx-elim-aux.new-stmt?
  (b* (((mv ?warnings ?new-stmt?)
        (vl-casezx-elim-aux type test cases default ctx warnings)))
    (equal (vl-stmt-p new-stmt?)
           (if new-stmt? t nil)))
  :rule-classes :rewrite)

Theorem: vl-casezx-elim-aux-of-vl-casetype-fix-type

(defthm vl-casezx-elim-aux-of-vl-casetype-fix-type
  (equal (vl-casezx-elim-aux (vl-casetype-fix type)
                             test cases default ctx warnings)
         (vl-casezx-elim-aux type test cases default ctx warnings)))

Theorem: vl-casezx-elim-aux-vl-casetype-equiv-congruence-on-type

(defthm vl-casezx-elim-aux-vl-casetype-equiv-congruence-on-type
 (implies
    (vl-casetype-equiv type type-equiv)
    (equal (vl-casezx-elim-aux type test cases default ctx warnings)
           (vl-casezx-elim-aux type-equiv
                               test cases default ctx warnings)))
 :rule-classes :congruence)

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

(defthm vl-casezx-elim-aux-of-vl-expr-fix-test
  (equal (vl-casezx-elim-aux type (vl-expr-fix test)
                             cases default ctx warnings)
         (vl-casezx-elim-aux type test cases default ctx warnings)))

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

(defthm vl-casezx-elim-aux-vl-expr-equiv-congruence-on-test
 (implies
   (vl-expr-equiv test test-equiv)
   (equal
        (vl-casezx-elim-aux type test cases default ctx warnings)
        (vl-casezx-elim-aux type
                            test-equiv cases default ctx warnings)))
 :rule-classes :congruence)

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

(defthm vl-casezx-elim-aux-of-vl-caselist-fix-cases
  (equal (vl-casezx-elim-aux type test (vl-caselist-fix cases)
                             default ctx warnings)
         (vl-casezx-elim-aux type test cases default ctx warnings)))

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

(defthm vl-casezx-elim-aux-vl-caselist-equiv-congruence-on-cases
 (implies
   (vl-caselist-equiv cases cases-equiv)
   (equal
        (vl-casezx-elim-aux type test cases default ctx warnings)
        (vl-casezx-elim-aux type
                            test cases-equiv default ctx warnings)))
 :rule-classes :congruence)

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

(defthm vl-casezx-elim-aux-of-vl-stmt-fix-default
  (equal (vl-casezx-elim-aux type test cases (vl-stmt-fix default)
                             ctx warnings)
         (vl-casezx-elim-aux type test cases default ctx warnings)))

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

(defthm vl-casezx-elim-aux-vl-stmt-equiv-congruence-on-default
 (implies
   (vl-stmt-equiv default default-equiv)
   (equal
        (vl-casezx-elim-aux type test cases default ctx warnings)
        (vl-casezx-elim-aux type
                            test cases default-equiv ctx warnings)))
 :rule-classes :congruence)

Theorem: vl-casezx-elim-aux-of-vl-modelement-fix-ctx

(defthm vl-casezx-elim-aux-of-vl-modelement-fix-ctx
  (equal (vl-casezx-elim-aux type test
                             cases default (vl-modelement-fix ctx)
                             warnings)
         (vl-casezx-elim-aux type test cases default ctx warnings)))

Theorem: vl-casezx-elim-aux-vl-modelement-equiv-congruence-on-ctx

(defthm vl-casezx-elim-aux-vl-modelement-equiv-congruence-on-ctx
 (implies
   (vl-modelement-equiv ctx ctx-equiv)
   (equal
        (vl-casezx-elim-aux type test cases default ctx warnings)
        (vl-casezx-elim-aux type
                            test cases default ctx-equiv warnings)))
 :rule-classes :congruence)

Theorem: vl-casezx-elim-aux-of-vl-warninglist-fix-warnings

(defthm vl-casezx-elim-aux-of-vl-warninglist-fix-warnings
  (equal (vl-casezx-elim-aux type test cases default
                             ctx (vl-warninglist-fix warnings))
         (vl-casezx-elim-aux type test cases default ctx warnings)))

Theorem: vl-casezx-elim-aux-vl-warninglist-equiv-congruence-on-warnings

(defthm
     vl-casezx-elim-aux-vl-warninglist-equiv-congruence-on-warnings
 (implies
   (vl-warninglist-equiv warnings warnings-equiv)
   (equal
        (vl-casezx-elim-aux type test cases default ctx warnings)
        (vl-casezx-elim-aux type
                            test cases default ctx warnings-equiv)))
 :rule-classes :congruence)