• 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-stmt-elim

Rewrite an casez or casex statement into if statements.

Signature

(vl-casezx-stmt-elim type check 
                     test cases default atts ctx warnings ss) 
 
  → 
(mv warnings new-stmt)

Arguments

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

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).

cases — The cases for the case statement, should be sized.
    Guard (vl-caselist-p cases).

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).

ss — NOTE: Not currently used.
    Guard (vl-scopestack-p ss).

Returns

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

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

Definitions and Theorems

Function: vl-casezx-stmt-elim

(defun vl-casezx-stmt-elim
       (type check
             test cases default atts ctx warnings ss)
 (declare (xargs :guard (and (vl-casetype-p type)
                             (vl-casecheck-p check)
                             (vl-expr-p test)
                             (vl-caselist-p cases)
                             (vl-stmt-p default)
                             (vl-atts-p atts)
                             (vl-modelement-p ctx)
                             (vl-warninglist-p warnings)
                             (vl-scopestack-p ss))))
 (declare (xargs :guard (member type '(:vl-casez :vl-casex))))
 (let ((__function__ 'vl-casezx-stmt-elim))
  (declare (ignorable __function__))
  (b*
   ((type (vl-casetype-fix type))
    (check (vl-casecheck-fix check))
    (test (vl-expr-fix test))
    (ctx (vl-modelement-fix ctx))
    (?ss (vl-scopestack-fix ss))
    (warnings (vl-warninglist-fix warnings))
    (new-warnings (vl-casestmt-size-warnings test cases ctx))
    (new-warnings
     (if (and (vl-expr-welltyped-p test)
              (posp (vl-expr->finalwidth test))
              (eq (vl-expr->finaltype test)
                  :vl-unsigned))
         new-warnings
      (warn
       :type :vl-casezx-fail
       :msg
       "~a0: can't handle ~s1 statement because ~
                                   the test expression ~a2 is either signed, ~
                                   unsized, or of size 0."
       :args (list ctx
                   (if (eq type :vl-casex) "casex" "casez")
                   test)
       :acc new-warnings)))
    ((when new-warnings)
     (mv (append-without-guard new-warnings warnings)
         (make-vl-casestmt :casetype type
                           :check check
                           :test test
                           :caselist cases
                           :default default
                           :atts atts)))
    (warnings
     (if check
      (warn
       :type :vl-casezx-check
       :msg
       "~a0: we don't yet implement priority, unique, or ~
                         unique0 checking for casez/x statements.  We will ~
                         treat this as an ordinary casez/x statement."
       :args (list (vl-modelement-fix ctx)))
      warnings))
    ((mv warnings new-stmt)
     (vl-casezx-elim-aux type test cases default ctx warnings))
    ((unless new-stmt)
     (b*
      ((warnings
        (warn
         :type :vl-casezx-unsafe-conversion
         :msg
         "~a0: ~s1 statement is not supported, so we ~
                                   are processing it as a regular case ~
                                   statement, which may be unsound."
         :args (list ctx
                     (if (eq type :vl-casex)
                         "casex"
                       "casez")))))
      (vl-casestmt-elim check
                        test cases default atts ctx warnings))))
   (mv warnings new-stmt))))

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

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

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

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

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

(defthm vl-casezx-stmt-elim-of-vl-casetype-fix-type
  (equal
       (vl-casezx-stmt-elim (vl-casetype-fix type)
                            check
                            test cases default atts ctx warnings ss)
       (vl-casezx-stmt-elim type check test
                            cases default atts ctx warnings ss)))

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

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

Theorem: vl-casezx-stmt-elim-of-vl-casecheck-fix-check

(defthm vl-casezx-stmt-elim-of-vl-casecheck-fix-check
  (equal
       (vl-casezx-stmt-elim type (vl-casecheck-fix check)
                            test cases default atts ctx warnings ss)
       (vl-casezx-stmt-elim type check test
                            cases default atts ctx warnings ss)))

Theorem: vl-casezx-stmt-elim-vl-casecheck-equiv-congruence-on-check

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

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

(defthm vl-casezx-stmt-elim-of-vl-expr-fix-test
  (equal (vl-casezx-stmt-elim type check (vl-expr-fix test)
                              cases default atts ctx warnings ss)
         (vl-casezx-stmt-elim type check test
                              cases default atts ctx warnings ss)))

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

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

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

(defthm vl-casezx-stmt-elim-of-vl-caselist-fix-cases
 (equal (vl-casezx-stmt-elim type check test (vl-caselist-fix cases)
                             default atts ctx warnings ss)
        (vl-casezx-stmt-elim type check test
                             cases default atts ctx warnings ss)))

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

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

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

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

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

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

Theorem: vl-casezx-stmt-elim-of-vl-atts-fix-atts

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

Theorem: vl-casezx-stmt-elim-vl-atts-equiv-congruence-on-atts

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

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

(defthm vl-casezx-stmt-elim-of-vl-modelement-fix-ctx
  (equal (vl-casezx-stmt-elim type check test cases
                              default atts (vl-modelement-fix ctx)
                              warnings ss)
         (vl-casezx-stmt-elim type check test
                              cases default atts ctx warnings ss)))

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

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

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

(defthm vl-casezx-stmt-elim-of-vl-warninglist-fix-warnings
  (equal (vl-casezx-stmt-elim type check test cases default
                              atts ctx (vl-warninglist-fix warnings)
                              ss)
         (vl-casezx-stmt-elim type check test
                              cases default atts ctx warnings ss)))

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

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

Theorem: vl-casezx-stmt-elim-of-vl-scopestack-fix-ss

(defthm vl-casezx-stmt-elim-of-vl-scopestack-fix-ss
  (equal (vl-casezx-stmt-elim type check test cases default atts
                              ctx warnings (vl-scopestack-fix ss))
         (vl-casezx-stmt-elim type check test
                              cases default atts ctx warnings ss)))

Theorem: vl-casezx-stmt-elim-vl-scopestack-equiv-congruence-on-ss

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