• 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-casezx-matchexpr

Creates, e.g., the expression (data & 4'b1100) === 4'b1000 for handling casez(data) ... 4'b10??: ... endcase.

Signature

(vl-casezx-matchexpr type test match-expr ctx warnings) 
  → 
(mv warnings expr?)

Arguments

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

test — E.g., for casex(data) ..., data.
    Guard (vl-expr-p test).

match-expr — E.g., 4'b10??, the expression to match; usually a weird integer with some wildcard bits.
    Guard (vl-expr-p match-expr).

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

expr? — On failure nil, otherwise an expression that checks whether we have a match, i.e., (data & 4'b1100) === 4'b1000.
    Type (iff (vl-expr-p expr?) expr?).

Definitions and Theorems

Function: vl-casezx-matchexpr

(defun vl-casezx-matchexpr (type test match-expr ctx warnings)
 (declare (xargs :guard (and (vl-casetype-p type)
                             (vl-expr-p test)
                             (vl-expr-p match-expr)
                             (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))
                             (eq (vl-expr->finaltype test)
                                 :vl-unsigned))))
 (let ((__function__ 'vl-casezx-matchexpr))
  (declare (ignorable __function__))
  (b*
   ((type (vl-casetype-fix type))
    (ctx (vl-modelement-fix ctx))
    (match-expr (vl-expr-fix match-expr))
    ((unless (and (vl-expr-welltyped-p match-expr)
                  (posp (vl-expr->finalwidth match-expr))))
     (mv
      (warn
       :type :vl-casezx-fail
       :msg
       "~a0: can't handle ~s1 statement; match expression ~a2 ~
                        is too complex or incorrectly sized."
       :args (list ctx
                   (if (eq type :vl-casex) "casex" "casez")
                   match-expr))
      nil))
    ((mv ok match-bits)
     (vl-intliteral-msb-bits match-expr))
    ((unless ok)
     (mv
      (warn
       :type :vl-casezx-fail
       :msg
       "~a0: can't handle ~s1 statement; match expression ~a2 ~
                        is too complex.  (We only support integer literals ~
                        here.)"
       :args (list ctx
                   (if (eq type :vl-casex) "casex" "casez")
                   match-expr))
      nil))
    (finalwidth (max (vl-expr->finalwidth match-expr)
                     (vl-expr->finalwidth test)))
    (finaltype (if (and (eq (vl-expr->finaltype match-expr)
                            :vl-signed)
                        (eq (vl-expr->finaltype test)
                            :vl-signed))
                   :vl-signed
                 :vl-unsigned))
    (ext-match-bits
         (append (repeat (- finalwidth
                            (vl-expr->finalwidth match-expr))
                         (if (eq finaltype :vl-signed)
                             (car match-bits)
                           :vl-0val))
                 match-bits))
    (cm-value (if (eq type :vl-casez)
                  (vl-msb-bits-to-z-care-mask ext-match-bits 0)
                (vl-msb-bits-to-zx-care-mask ext-match-bits 0)))
    (cm-guts (make-vl-constint :value cm-value
                               :origwidth finalwidth
                               :origtype finaltype))
    (cm-expr (make-vl-atom :guts cm-guts
                           :finalwidth finalwidth
                           :finaltype finaltype))
    (zap-bits (if (eq type :vl-casez)
                  (vl-msb-bits-zap-dontcares-z ext-match-bits)
                (vl-msb-bits-zap-dontcares-zx ext-match-bits)))
    (zap-expr (vl-msb-bits-to-intliteral zap-bits finaltype))
    (test-width (vl-expr->finalwidth test))
    (test-ext
     (if
      (< test-width finalwidth)
      (make-vl-nonatom
       :op :vl-concat
       :args
       (list
         (make-vl-atom
              :guts
              (make-vl-constint :origwidth (- finalwidth test-width)
                                :origtype :vl-unsigned
                                :value 0)
              :finalwidth (- finalwidth test-width)
              :finaltype :vl-unsigned)
         test)
       :finalwidth finalwidth
       :finaltype finaltype)
      test))
    (if-test
     (make-vl-nonatom
          :op :vl-binary-ceq
          :args (list (make-vl-nonatom :op :vl-binary-bitand
                                       :args (list test-ext cm-expr)
                                       :finalwidth finalwidth
                                       :finaltype finaltype)
                      zap-expr)
          :finalwidth 1
          :finaltype :vl-unsigned)))
   (mv (ok) if-test))))

Theorem: vl-warninglist-p-of-vl-casezx-matchexpr.warnings

(defthm vl-warninglist-p-of-vl-casezx-matchexpr.warnings
  (b* (((mv ?warnings ?expr?)
        (vl-casezx-matchexpr type test match-expr ctx warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-casezx-matchexpr.expr?

(defthm return-type-of-vl-casezx-matchexpr.expr?
  (b* (((mv ?warnings ?expr?)
        (vl-casezx-matchexpr type test match-expr ctx warnings)))
    (iff (vl-expr-p expr?) expr?))
  :rule-classes :rewrite)

Theorem: vl-expr->finalwidth-of-vl-casezx-matchexpr

(defthm vl-expr->finalwidth-of-vl-casezx-matchexpr
  (b* (((mv ?warnings ?expr?)
        (vl-casezx-matchexpr type test match-expr ctx warnings)))
    (implies expr?
             (equal (vl-expr->finalwidth expr?) 1)))
  :rule-classes :rewrite)

Theorem: vl-expr->finaltype-of-vl-casezx-matchexpr

(defthm vl-expr->finaltype-of-vl-casezx-matchexpr
  (b* (((mv ?warnings ?expr?)
        (vl-casezx-matchexpr type test match-expr ctx warnings)))
    (implies expr?
             (equal (vl-expr->finaltype expr?)
                    :vl-unsigned)))
  :rule-classes :rewrite)

Theorem: vl-expr-welltyped-p-of-vl-casezx-matchexpr

(defthm vl-expr-welltyped-p-of-vl-casezx-matchexpr
 (implies
     (and (vl-expr-welltyped-p test)
          (posp (vl-expr->finalwidth test))
          (equal (vl-expr->finaltype test)
                 :vl-unsigned))
     (b* (((mv & result)
           (vl-casezx-matchexpr type test match-expr ctx warnings)))
       (implies result (vl-expr-welltyped-p result)))))

Theorem: vl-casezx-matchexpr-of-vl-casetype-fix-type

(defthm vl-casezx-matchexpr-of-vl-casetype-fix-type
  (equal (vl-casezx-matchexpr (vl-casetype-fix type)
                              test match-expr ctx warnings)
         (vl-casezx-matchexpr type test match-expr ctx warnings)))

Theorem: vl-casezx-matchexpr-vl-casetype-equiv-congruence-on-type

(defthm vl-casezx-matchexpr-vl-casetype-equiv-congruence-on-type
 (implies
      (vl-casetype-equiv type type-equiv)
      (equal (vl-casezx-matchexpr type test match-expr ctx warnings)
             (vl-casezx-matchexpr type-equiv
                                  test match-expr ctx warnings)))
 :rule-classes :congruence)

Theorem: vl-casezx-matchexpr-of-vl-expr-fix-test

(defthm vl-casezx-matchexpr-of-vl-expr-fix-test
  (equal (vl-casezx-matchexpr type (vl-expr-fix test)
                              match-expr ctx warnings)
         (vl-casezx-matchexpr type test match-expr ctx warnings)))

Theorem: vl-casezx-matchexpr-vl-expr-equiv-congruence-on-test

(defthm vl-casezx-matchexpr-vl-expr-equiv-congruence-on-test
 (implies
   (vl-expr-equiv test test-equiv)
   (equal (vl-casezx-matchexpr type test match-expr ctx warnings)
          (vl-casezx-matchexpr type
                               test-equiv match-expr ctx warnings)))
 :rule-classes :congruence)

Theorem: vl-casezx-matchexpr-of-vl-expr-fix-match-expr

(defthm vl-casezx-matchexpr-of-vl-expr-fix-match-expr
  (equal (vl-casezx-matchexpr type test (vl-expr-fix match-expr)
                              ctx warnings)
         (vl-casezx-matchexpr type test match-expr ctx warnings)))

Theorem: vl-casezx-matchexpr-vl-expr-equiv-congruence-on-match-expr

(defthm vl-casezx-matchexpr-vl-expr-equiv-congruence-on-match-expr
 (implies
   (vl-expr-equiv match-expr match-expr-equiv)
   (equal (vl-casezx-matchexpr type test match-expr ctx warnings)
          (vl-casezx-matchexpr type
                               test match-expr-equiv ctx warnings)))
 :rule-classes :congruence)

Theorem: vl-casezx-matchexpr-of-vl-modelement-fix-ctx

(defthm vl-casezx-matchexpr-of-vl-modelement-fix-ctx
 (equal (vl-casezx-matchexpr type
                             test match-expr (vl-modelement-fix ctx)
                             warnings)
        (vl-casezx-matchexpr type test match-expr ctx warnings)))

Theorem: vl-casezx-matchexpr-vl-modelement-equiv-congruence-on-ctx

(defthm vl-casezx-matchexpr-vl-modelement-equiv-congruence-on-ctx
 (implies
   (vl-modelement-equiv ctx ctx-equiv)
   (equal (vl-casezx-matchexpr type test match-expr ctx warnings)
          (vl-casezx-matchexpr type
                               test match-expr ctx-equiv warnings)))
 :rule-classes :congruence)

Theorem: vl-casezx-matchexpr-of-vl-warninglist-fix-warnings

(defthm vl-casezx-matchexpr-of-vl-warninglist-fix-warnings
  (equal (vl-casezx-matchexpr type test match-expr
                              ctx (vl-warninglist-fix warnings))
         (vl-casezx-matchexpr type test match-expr ctx warnings)))

Theorem: vl-casezx-matchexpr-vl-warninglist-equiv-congruence-on-warnings

(defthm
    vl-casezx-matchexpr-vl-warninglist-equiv-congruence-on-warnings
 (implies
   (vl-warninglist-equiv warnings warnings-equiv)
   (equal (vl-casezx-matchexpr type test match-expr ctx warnings)
          (vl-casezx-matchexpr type
                               test match-expr ctx warnings-equiv)))
 :rule-classes :congruence)