• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
      • Svex-stvs
      • Svex-decomposition-methodology
      • Sv-versus-esim
      • Svex-decomp
      • Svex-compose-dfs
      • Svex-compilation
      • Moddb
      • Svmods
      • Svstmt
      • Sv-tutorial
      • Expressions
      • Symbolic-test-vector
      • Vl-to-svex
        • Vl-to-sv
        • Vl-design->sv-design
          • Vl-simpconfig
          • Vl-hierarchy-sv-translation
          • Vl-expr-svex-translation
          • Vl-design->svex-modalist
          • Vl-svstmt
            • Vl-svstmt.lisp
              • Vl-casestmt-violation-conds
              • Vl-caselist-none/multiple
              • Vl-elaborated-expr-consteval
              • Vl-always->svex
              • Vl-caseexprs->svex-test
              • Vl-always->svex-checks
              • Vl-implicitvalueparam-final-type
              • Vl-assignstmt->svstmts
              • Vl-fundecl-to-svex
              • Vl-evatomlist-delay-substitution
              • Vl-consteval
              • Vl-alwayslist->svex
              • Vl-index-expr-svex/size/type
              • Vl-vardecllist->svstmts
              • Sv::svex-alist->assigns
              • Vl-case-conservative-test-expr
              • Vl-evatomlist->svex
              • Vl-case-xcond-wrapper
              • Sv::constraintlist-maybe-rewrite-fixpoint
              • Vl-always-apply-trigger-to-updates
              • Vl-initiallist-size-warnings
              • Vl-initial-size-warnings
              • Vl-finallist-size-warnings
              • Vl-always->svex-latch-warnings
              • Vl-final-size-warnings
              • Sv::svarlist-masked-x-subst
              • Sv::svar->lhs-by-mask
              • Svstmt-config
              • Sv::svex-alist-unset-nonblocking
              • Sv::svar->lhs-by-size
              • Combine-mask-alists
              • Sv::svarlist-delay-subst
              • Vttree-constraints-to-svstmts
              • Sv::4vmask-alist-unset-nonblocking
              • Sv::svarlist-remove-delays
              • Vl-caselist->caseexprs
              • Vl-evatomlist-has-edge
        • Vl-to-sv-main
        • Vl-simplify-sv
        • Vl-user-paramsettings->unparam-names
        • Vl-user-paramsettings->modnames
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Vl-svstmt.lisp

Vl-caselist-none/multiple

Signature

(vl-caselist-none/multiple x size test casetype casekey ss scopes) 
  → 
(mv vttree nonematch multimatch)

Arguments

x — Guard (vl-caselist-p x).

size — Guard (natp size).

test — Guard (sv::svex-p test).

casetype — Guard (vl-casetype-p casetype).

casekey — Guard (vl-casekey-p casekey).

ss — Guard (vl-scopestack-p ss).

scopes — Guard (vl-elabscopes-p scopes).

Returns

vttree — Type (and (vttree-p vttree) (sv::svarlist-addr-p (sv::constraintlist-vars (vttree->constraints vttree)))) .

nonematch — Expression (whose value is a bit) signifying that none of the cases match.
    Type (sv::svex-p nonematch).

multimatch — Expression (whose value is a bit) signifying that more than 1 case matches.
    Type (sv::svex-p multimatch).

Definitions and Theorems

Function: vl-caselist-none/multiple

(defun vl-caselist-none/multiple
       (x size test casetype casekey ss scopes)
 (declare (xargs :guard (and (vl-caselist-p x)
                             (natp size)
                             (sv::svex-p test)
                             (vl-casetype-p casetype)
                             (vl-casekey-p casekey)
                             (vl-scopestack-p ss)
                             (vl-elabscopes-p scopes))))
 (let ((__function__ 'vl-caselist-none/multiple))
  (declare (ignorable __function__))
  (b* ((x (vl-caselist-fix x))
       ((when (atom x)) (mv nil 1 0))
       (tests (caar x))
       ((mv vttree none-rest multi-rest)
        (vl-caselist-none/multiple
             (cdr x)
             size test casetype casekey ss scopes))
       ((vmv vttree svtest)
        (vl-caseexprs->svex-test
             tests
             test size casetype casekey ss scopes)))
   (mv
     vttree
     (sv::svcall sv::bitand
                 (sv::svcall sv::bitnot svtest)
                 none-rest)
     (sv::svcall
          sv::bitor
          (sv::svcall
               sv::bitand svtest
               (sv::svex-zerox 1 (sv::svcall sv::bitnot none-rest)))
          multi-rest)))))

Theorem: return-type-of-vl-caselist-none/multiple.vttree

(defthm return-type-of-vl-caselist-none/multiple.vttree
 (b* (((mv ?vttree ?nonematch ?multimatch)
       (vl-caselist-none/multiple
            x
            size test casetype casekey ss scopes)))
  (and
      (vttree-p vttree)
      (sv::svarlist-addr-p
           (sv::constraintlist-vars (vttree->constraints vttree)))))
 :rule-classes :rewrite)

Theorem: svex-p-of-vl-caselist-none/multiple.nonematch

(defthm svex-p-of-vl-caselist-none/multiple.nonematch
  (b* (((mv ?vttree ?nonematch ?multimatch)
        (vl-caselist-none/multiple
             x
             size test casetype casekey ss scopes)))
    (sv::svex-p nonematch))
  :rule-classes :rewrite)

Theorem: svex-p-of-vl-caselist-none/multiple.multimatch

(defthm svex-p-of-vl-caselist-none/multiple.multimatch
  (b* (((mv ?vttree ?nonematch ?multimatch)
        (vl-caselist-none/multiple
             x
             size test casetype casekey ss scopes)))
    (sv::svex-p multimatch))
  :rule-classes :rewrite)

Theorem: svex-addr-p-of-vl-caselist-none/multiple

(defthm svex-addr-p-of-vl-caselist-none/multiple
 (b* (((mv ?vttree ?nonematch ?multimatch)
       (vl-caselist-none/multiple
            x
            size test casetype casekey ss scopes)))
  (implies (sv::svarlist-addr-p (sv::svex-vars test))
           (and (sv::svarlist-addr-p (sv::svex-vars nonematch))
                (sv::svarlist-addr-p (sv::svex-vars multimatch))))))

Theorem: vl-caselist-none/multiple-of-vl-caselist-fix-x

(defthm vl-caselist-none/multiple-of-vl-caselist-fix-x
 (equal
  (vl-caselist-none/multiple (vl-caselist-fix x)
                             size test casetype casekey ss scopes)
  (vl-caselist-none/multiple x
                             size test casetype casekey ss scopes)))

Theorem: vl-caselist-none/multiple-vl-caselist-equiv-congruence-on-x

(defthm vl-caselist-none/multiple-vl-caselist-equiv-congruence-on-x
  (implies (vl-caselist-equiv x x-equiv)
           (equal (vl-caselist-none/multiple
                       x size test casetype casekey ss scopes)
                  (vl-caselist-none/multiple
                       x-equiv
                       size test casetype casekey ss scopes)))
  :rule-classes :congruence)

Theorem: vl-caselist-none/multiple-of-nfix-size

(defthm vl-caselist-none/multiple-of-nfix-size
 (equal
  (vl-caselist-none/multiple x (nfix size)
                             test casetype casekey ss scopes)
  (vl-caselist-none/multiple x
                             size test casetype casekey ss scopes)))

Theorem: vl-caselist-none/multiple-nat-equiv-congruence-on-size

(defthm vl-caselist-none/multiple-nat-equiv-congruence-on-size
 (implies
  (acl2::nat-equiv size size-equiv)
  (equal
       (vl-caselist-none/multiple
            x size test casetype casekey ss scopes)
       (vl-caselist-none/multiple x size-equiv
                                  test casetype casekey ss scopes)))
 :rule-classes :congruence)

Theorem: vl-caselist-none/multiple-of-svex-fix-test

(defthm vl-caselist-none/multiple-of-svex-fix-test
 (equal
  (vl-caselist-none/multiple x size (sv::svex-fix test)
                             casetype casekey ss scopes)
  (vl-caselist-none/multiple x
                             size test casetype casekey ss scopes)))

Theorem: vl-caselist-none/multiple-svex-equiv-congruence-on-test

(defthm vl-caselist-none/multiple-svex-equiv-congruence-on-test
  (implies (sv::svex-equiv test test-equiv)
           (equal (vl-caselist-none/multiple
                       x size test casetype casekey ss scopes)
                  (vl-caselist-none/multiple
                       x size
                       test-equiv casetype casekey ss scopes)))
  :rule-classes :congruence)

Theorem: vl-caselist-none/multiple-of-vl-casetype-fix-casetype

(defthm vl-caselist-none/multiple-of-vl-casetype-fix-casetype
 (equal
  (vl-caselist-none/multiple x size test (vl-casetype-fix casetype)
                             casekey ss scopes)
  (vl-caselist-none/multiple x
                             size test casetype casekey ss scopes)))

Theorem: vl-caselist-none/multiple-vl-casetype-equiv-congruence-on-casetype

(defthm
 vl-caselist-none/multiple-vl-casetype-equiv-congruence-on-casetype
 (implies (vl-casetype-equiv casetype casetype-equiv)
          (equal (vl-caselist-none/multiple
                      x size test casetype casekey ss scopes)
                 (vl-caselist-none/multiple
                      x size
                      test casetype-equiv casekey ss scopes)))
 :rule-classes :congruence)

Theorem: vl-caselist-none/multiple-of-vl-casekey-fix-casekey

(defthm vl-caselist-none/multiple-of-vl-casekey-fix-casekey
 (equal
  (vl-caselist-none/multiple x size
                             test casetype (vl-casekey-fix casekey)
                             ss scopes)
  (vl-caselist-none/multiple x
                             size test casetype casekey ss scopes)))

Theorem: vl-caselist-none/multiple-vl-casekey-equiv-congruence-on-casekey

(defthm
   vl-caselist-none/multiple-vl-casekey-equiv-congruence-on-casekey
  (implies (vl-casekey-equiv casekey casekey-equiv)
           (equal (vl-caselist-none/multiple
                       x size test casetype casekey ss scopes)
                  (vl-caselist-none/multiple
                       x size
                       test casetype casekey-equiv ss scopes)))
  :rule-classes :congruence)

Theorem: vl-caselist-none/multiple-of-vl-scopestack-fix-ss

(defthm vl-caselist-none/multiple-of-vl-scopestack-fix-ss
 (equal
  (vl-caselist-none/multiple x size test
                             casetype casekey (vl-scopestack-fix ss)
                             scopes)
  (vl-caselist-none/multiple x
                             size test casetype casekey ss scopes)))

Theorem: vl-caselist-none/multiple-vl-scopestack-equiv-congruence-on-ss

(defthm
     vl-caselist-none/multiple-vl-scopestack-equiv-congruence-on-ss
  (implies (vl-scopestack-equiv ss ss-equiv)
           (equal (vl-caselist-none/multiple
                       x size test casetype casekey ss scopes)
                  (vl-caselist-none/multiple
                       x size
                       test casetype casekey ss-equiv scopes)))
  :rule-classes :congruence)

Theorem: vl-caselist-none/multiple-of-vl-elabscopes-fix-scopes

(defthm vl-caselist-none/multiple-of-vl-elabscopes-fix-scopes
 (equal
  (vl-caselist-none/multiple x size test casetype
                             casekey ss (vl-elabscopes-fix scopes))
  (vl-caselist-none/multiple x
                             size test casetype casekey ss scopes)))

Theorem: vl-caselist-none/multiple-vl-elabscopes-equiv-congruence-on-scopes

(defthm
 vl-caselist-none/multiple-vl-elabscopes-equiv-congruence-on-scopes
 (implies (vl-elabscopes-equiv scopes scopes-equiv)
          (equal (vl-caselist-none/multiple
                      x size test casetype casekey ss scopes)
                 (vl-caselist-none/multiple
                      x size
                      test casetype casekey ss scopes-equiv)))
 :rule-classes :congruence)